formality 问题 求助

gbsid

有这样一个设计,reg3的异步置位和异步复位（SN，RN）分别直接来自于reg1和reg2(异步置位和异步复位不能同时有效，所以SN和RN不能同时为0)。Formality在解析RTL的时候自动在reg1和reg2——也就是reg3的SN和RN端添加了逻辑，保证SN和RN不能出现同时为0的情况（我看Formality的逻辑图是这样的）。但是在综合后的网表中，并没有这种处理，也就是说reg3的SN和RN是直接来自于reg1和reg2。这样reg1和reg2就会出现同时为0的情况，从而导致formality验证结果是错误的。其实reg1和reg2在电路里面已经通过置位和复位作了处理，保证不会同时输出0。

不知有什么方法可以让formality通过这种验证。

我的想法是不让reg1和reg2的Q端产生同时输出0的向量，但是存在01,10,11这三个向量

看了formality的user guide，里面有讲实用create_constraint_type创建约束，实用set_constraint施加用户创建的约束的情况，但不知道怎么做。特此请教。

有更好的办法更好。

icfbicfb

用综合的svf啊 ，

dc的svf导入 fm就行了，不用这么细节，

gbsid

回复 2# icfbicfb


首先，感谢你的回答   我已经读入了svf但是还是有问题,并且从formality的图形界面上可以看到增加的逻辑；但是在综合的网表上确不存在这些逻辑，就像上图，直接来自于前级寄存器。

鬼舞十七

确实是这个问题，之前遇到过，FM解析RTL，在reg3的RN和SN前会做互斥，但DC不会

gbsid

回复 4# 鬼舞十七


   hello，最后你们是怎么做的呢？

鬼舞十七

回复 5# gbsid


   没解决，报告里面列出来。实际不会有问题。
其实，有用到DFFSR的地方，我们在rtl-code的时候自己就做了互斥的，RN=a SN=~(a&(~b)),但FM会在这后面再自己加互斥，总之，只要有DFFSR的地方，它都自己加，逻辑化简后也就这个意思。应该是有个地方能约束FM不加，但没找到。