形式验证遇到的问题

孤月飞星 · 发表于 2012-11-19 09:48:58

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

x

做数字模块的形式验证是通过的，但是加上模拟IP之后再做形式验证就出现问题，请问该从什么地方入手分析解决。

cnasic@163.com · 发表于 2012-11-19 11:32:13

set_black_box

lemondavid · 发表于 2012-11-19 18:56:21

我也试下

孤月飞星 · 发表于 2012-11-20 08:47:20

这个用了，但是也不起作用，后来已经解决了，方法是将所有的SVF文件都添加进去。用的是buttom to up的综合方式，最开始做形式验证只将最上层的SVF添加了，现在将子模块的SVF以及顶层的SVF添加进去就可以通过形式验证了。

llongice9 · 发表于 2012-11-20 11:33:10

形式验证的本质是什么啊

sunhui_asic · 发表于 2013-6-27 22:23:04

看看。。。

fengzhepianzhou · 发表于 2013-7-2 22:08:49

本质？就是保证网表和rtl的一致，不一致的原因可以有：
1、版图或者手动插入buffer的时候插入反相器，
2、用candence的综合工具，然后用synopsis的lec工具有可能不一致
3、dc优化过程出现bug，比如我就遇见dc综合后出现多驱动的现象，这个代码里面是没有的，lec可以找出

[求助] 形式验证遇到的问题