Conformal和formality做形式验证svf文件问题

@@@12 · 发表于 2022-8-11 17:39:21

您需要登录才可以下载或查看，没有账号？注册

x

formality要读入一个svf文件，那conformal需要读入什么文件帮助LEC呢？
试了用DC生成一个vsdc文件，但读进去并没有解决问题，一个可能是读的指令不对，又或者还需要发送什么指令来进行设置？

jake · 发表于 2022-8-11 21:57:39

Conformal可以读入Genus写出的fv目录下的文件，帮助LEC

@@@12 · 发表于 2022-8-12 09:24:03

jake 发表于 2022-8-11 21:57
Conformal可以读入Genus写出的fv目录下的文件，帮助LEC

Genus是cadence的综合工具吧，读入DC的文件不可以吗，是一定要用同家工具吗，Genus没用过

jake · 发表于 2022-8-12 09:39:05

@@@12 发表于 2022-8-11 19:24
Genus是cadence的综合工具吧，读入DC的文件不可以吗，是一定要用同家工具吗，Genus没用过
...

SVF是binary格式，不公开，conformal读不了。
S家工具比较恶心，经常这样搞。

jake · 发表于 2022-8-12 09:42:24

conformal是可以读VSDC的
READ SETUP INFORMATION <file> -TYPE <type>
SETUP> read setup information myblock.vsdc -type vsdc

@@@12 · 发表于 2022-8-12 14:46:11

本帖最后由 @@@12 于 2022-8-12 14:47 编辑

jake 发表于 2022-8-12 09:42
conformal是可以读VSDC的
READ SETUP INFORMATION -TYPE
SETUP> read setup information myblock.vsdc -t ...

我就是用这条指令读了vsdc文件，read setup information .../.vsdc -type vsdc -revised -report -verbos
但对比结果出来有很多不等，我分析了几个，发现是优化导致的，读入vsdc貌似没有什么效果，还是我缺少了什么设置呢？

@@@12 · 发表于 2022-8-18 17:06:06

无效读入vsdc，感觉没读进去，要怎么才让软件识别到优化信息

lzxqaq · 发表于 2022-9-22 17:13:35

我只在vsdc文件看到 DC 命名规则引起的重命名信息，并没有其他优化的信息。楼主最后是怎么解决的？

@@@12 · 发表于 2022-11-12 15:11:41

lzxqaq 发表于 2022-9-22 17:13
我只在vsdc文件看到 DC 命名规则引起的重命名信息，并没有其他优化的信息。楼主最后是怎么解决的？ ...

没有解决，还是得用formality做

温柔阴影 · 发表于 2022-12-21 10:09:34

formality 读入svf会吐出svf明文，conformal 应该可以用

[求助] Conformal和formality做形式验证svf文件问题