急求，Formality吃了svf后的unmatch问题

zaqi

各位大神，不吝赐教啊！！！

1、环境：DC 2016 2018均试过，FM为2016

2、背景：A、B两个项目，A中有个小harden名为C，B和C都比对过了，只有A有大量unmatch

3、现象：A的DC生成了svf，Formality吃了该svf，依然有大量unmatch。分析发现，这些unmatch点均为DC中被merge掉了，但是Formality没吃到merge信息，认为这些cell还存在

4、其他：（1）查看了DC生成的网表，这些cell确实被merge掉了
               （2）dc.log里没有这些merge信息
               （3）Formality生成的svf.txt中也没有这些cell的merge信息（不是rejected，而是压根没有）

现在不确定merge信息是Formality吃.svf二进制文件时丢失了，还是DC压根就没写入，请问有没有大神遇到过类似问题，现在卡住了，不知道如何往下debug。

各位大神，不吝赐教啊！！！

13129969857

DC是不是analyze&elaborate(也可以是read的过程) 的过程没有被svf记录？这个过程不记录会导致这一类问题。

zaqi

13129969857 发表于 2020-12-2 16:20
DC是不是analyze&elaborate(也可以是read的过程) 的过程没有被svf记录？这个过程不记录会导致这一类问题。 ...

    您说这个倒是没有考虑过，有这个可能。
  那么请问如何保证这个过程被记录呢？现在set_svf已经是写在最前面了，光有这句话能保证吗？

13129969857

zaqi 发表于 2020-12-2 18:51
您说这个倒是没有考虑过，有这个可能。
  那么请问如何保证这个过程被记录呢？现在set_svf已经是写在 ...

是的，set_svf写在最前面就可以了。

zaqi

追加调试进度：
    现在单拎出某一个不到1000行代码的.v，居然都比对不过。
    该module内有一个[10:0]的reg，第[9] bit实际用不到。
    根据各种输出报告，该bit的cell在DC compile前还存在，compile后就没了，看不到remove。

    Formality无论吃不吃svf，都是这一bit的cell unmatch，因为它认为在ref中该cell还存在，但是在imp中找不到

    DC版本2016 2018  Formality版本2016 2017，4种排列组合都尝试了，现象一致。
   
    现在定位，Formality与DC对那一bit的处理策略明显不一样，但是在svf中又看不到那一bit的remove，不知该如何是好了。

    ps:这只是为了debug的手段，实际工程庞大，有大量类似问题，所以不可能通过修改代码或者单独用语句去处理那一个寄存器的方法来规避问题。

    各位大神显显神通，救救小弟啊！！！

13129969857

看看编译脚本？formality的问题之前也是很头疼，一般来说，只要流程规范，formality有时候是会出现unmatch的，但是verify会过。

独孤败天999

不用太纠结unmatch，看下log里面是VERIFYED SUCCESSED还是FAILED，或者可以start_gui看下

junma8862

1、首先确认formality是否fail；
2、如果fail，看是否是unmatch 导致；如果是的话就比较麻烦，建议首先确认综合和formality两边读取代码的方式是否一致，尤其是宏定义顺序、传参等影响；如果不是可以进入第三步
3、如果success或者非unmatch 导致fail，需要设计分析unmatch原因，看是否对功能无影响；确认完毕即可。
unmatch对于大设计来说是很正常的，不过你说的merge的问题，还没有遇到过，希望解决之后share一下原因。

l13787908861

路过学习，很实用，谢谢分享

l13787908861

路过学习，很实用，谢谢分享