使用formality形式验证出现非常多的failing points

homelander

小弟最近在做形式验证的工作，用到的是DC+formality。但是在formality中，在导入了svf文件的前提下verify一步依然出现了非常多的failing points。请求各位大佬指点12

ilmkduse

看到failing的时候，其实你是不知道到底这个是由于工具没认对，还是真的发生了不一致。
一般debug的话会看下输入-输出结果这些，确认是不是真的出错了。如果出错了就找综合的问题。没错的话看下是不是formality的哪些设置问题。
单纯看一个结果存在failing其实没法debug的。

另外你这里有大量的unverified，未比较的点，得看看是不是命名对应或者是什么丢了导致的。

ilmkduse

单纯看到failing只知道是没跑通。它可以是flow设置不对，也可能是真的有不一致。得检查具体情况才知道了。

可能还在建flow的阶段吧？有大量的unverified，不知道是特地不比还是由于设置不对导致的。
如果是的话，可以先找下设置，是不是命名匹配规则之类的和你综合后的结果没对上，它就根本没比/比错了。也可能是svf文件不对？

yuanpin318

先看有没有unmatched point.

如果没有的话，选择cone size最小的看看pattern window。你这么多failing Point多数是testmode和supply的constant没有set。

homelander

   

ilmkduse 发表于 2025-11-14 16:22
单纯看到failing只知道是没跑通。它可以是flow设置不对，也可能是真的有不一致。得检查具体情况才知道了。
...

感谢回复。这个问题大概是因为我写dc脚本的时候，在compile之前写了个set_svf xxx.svf，然后就把这个svf文件导入了。这样生成的svf文件跟dc默认生成的default.svf似乎是不一样的，小弟导入后者再重复相同的步骤就succeeded了。

homelander

   

yuanpin318 发表于 2025-11-14 17:36
先看有没有unmatched point.

如果没有的话，选择cone size最小的看看pattern window。你这么多failing Poi ...

感谢回复。这个问题大概是因为我写dc脚本的时候，在compile之前写了个set_svf xxx.svf，然后就把这个svf文件导入了。这样生成的svf文件跟dc默认生成的default.svf似乎是不一样的，小弟导入后者再重复相同的步骤就succeeded了。