formality verify failed 求助

刮痧永不嫌多 · 发表于 2025-2-27 15:57:45

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

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

x

小白求助
领导给了一份usart的rtl代码，其中有个spi模式，我修改了该模式，领导让我测试除了spi模式外，其他模式是否受到影响，我进行formality形式验证，ref是修改前的rtl代码，impl是修改后的rtl代码，两个代码都将spi模式关闭了，不会跑spi的功能，match都match上了，但是verify failed。然后我就单独测试子模块中哪里失败了，发现是receiver.v会verify failed。然后我又突发奇想，将ref和impl都设置成修改前的receiver.v的rtl代码，结果还是verify failed。请问为什么ref和impl是同一个rtl代码，verify 会 failed？

望大佬们解答，谢谢！

刮痧永不嫌多 · 发表于 2025-2-27 16:24:41

formality通过了，之前的形式验证我加了svf文件和db文件，而rtl和rtl对比似乎不需要这两个文件，不加这两个文件就通过了，小白还是想知道为什么，求大佬们解答

2596784844 · 发表于 2025-2-27 17:35:34

svf里面有综合时候优化以及rename的guide，只对ref生效，出现fail很正常

刮痧永不嫌多 · 发表于 2025-2-28 09:28:45

2596784844 发表于 2025-2-27 17:35
svf里面有综合时候优化以及rename的guide，只对ref生效，出现fail很正常

感谢大佬解惑

[求助] formality verify failed 求助

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

浏览过的版块

站长推荐 /2