formality问题求助！！！

pigolo

各位大侠，小弟用formality的时候遇到了点问题，请帮忙看看，谢谢。

issue1：Dc综合的时候将一些常量寄存器砍掉了，并且将相关信息写入svf，但是fm在吃svf的时候将这些guide指令给reject了。
fm后续认定rtl中这些寄存器为unmatched的， 并且这些寄存器影响了后面一些逻辑，导致verify fail。rtl逻辑代码如下：

wire [9:0] a;     
reg [9:0] a_d1;     
reg [9:0] a_d2;     
reg [9:0] a_d3;     
reg [9:0] a_d4;     
reg [9:0] a_d5;     

assign a = 10'b0;

always @（posedge clk）
     begin
              a_d1 <= a;
              a_d2 <= a_d1;
              a_d3 <= a_d2;
              a_d4 <= a_d3;
              a_d5 <= a_d4;
    end
   
     DC在综合时将a_d1直接砍掉，在综合a_d2时，先是将a_d2[1]~a_d2[9]同a_d2[0] merge了一下，然后又将a_d2[0]，砍掉。
     后面的a_d3~a_d5直接砍掉。这些信息在svf中都是有记录的。但是fm在吃svf的时候将a_d2[1]~a_d2[9]等于0的guide指令给rejected了，
    a_d2[0]等于0的却accepted了。后续的a_d3[0]~a_d5[0]等于0都accepted，其他bit都rejected。从rtl上看这些寄存器最后应该能推断出
    应该都是0，是很明显的。为什DC综合的时候，处理a_d2~a_d5，不像a_d1那样直接砍掉，怎么会有a_d2的merge这事出现呢。并且fm也恰恰是
   在这个位置开始不认识后面的几个变量，吃svf的时候说这些变量不能被推断出=0，从而将svf中令其等于0的那些指令都给rejected了。
   由于这些变量后面用在了一些比较点里面，所以最后的verify fail了。当在fm的脚本中将这些变量都人为设置成0，从新跑fm verify 就成功了。
   请问各位大侠这是怎么回事，谢谢

issu2： fm在吃rtl的时候，将某些寄存器推断出是DFF，将某些寄存器推断是是LAT， 从rtl代码上来看（是项目中的其他的代码，不是我上一个问题中
    举例的代码）这些寄存器应该都是时序逻辑的纯粹的寄存器，应该就是DFF，LAT应该只会出现在组合逻辑分支条件不完整的地方才对。 我想知道fm推断一个寄存器是DFF还是LAT，是根据什么方式推断的。

pigolo

在线等，请各位大侠出手相助，谢谢

sdlyyuxi

回复 2# pigolo


   会不会是你的formality环境setup的有问题，我综合了你的module, 并吃了svf，没有rejected；
   最后passed；
   我的svf中没有rejected； constant的

  

1. module eetop (//input
   
2.                 clk,
   
3.                 //output
   
4.                 temp
   
5.                 );
   
6. input clk;
   
7. //input  [9:0] a;   
   
8. output [9:0] temp;   
   
9. reg [9:0] a_d1;     
   
10. reg [9:0] a_d2;     
    
11. reg [9:0] a_d3;     
    
12. reg [9:0] a_d4;     
    
13. reg [9:0] a_d5;     
    
14. 
    
15. wire [9:0] a = 10'b0;
    
16. assign temp = (a_d1|a_d2|a_d3|a_d4|a_d5);
    
17. always @(posedge clk)
    
18.      begin
    
19.               a_d1 <= a;
    
20.               a_d2 <= a_d1;
    
21.               a_d3 <= a_d2;
    
22.               a_d4 <= a_d3;
    
23.               a_d5 <= a_d4;
    
24.     end
    
25. endmodule
    

复制代码

pigolo

回复 3# sdlyyuxi


    这块代码是位于设计中较低层次的逻辑。fm的setup我只设置了跟scan相关的，就是将test_en = 0； 其他好像不需要什么setup的东西，
   芯片的顶层接口不是i2c就是模拟的，还有几个gpio

sdlyyuxi

回复 4# pigolo


    report_svf_operation -status rejected -command reg_constant
看一下为啥rejected

pigolo

我又综合了一版代码，上版是不带ICG和DFT，这一版将ICG插了进去，发现不报这个问题了，并且verify也过了，真是奇了怪了

sdlyyuxi

回复 6# pigolo


    从我这边看，svf的顺序是，a_d1[0] ~a_d1[9] 是直接有相关的guide_reg_constant command；
    而对于a_d2, 就像你说的，是先把a_d2[1]~a_d2[9] merge 到a_d2[0]; 然后再将a_d2[0] guide 为constant 0；
    逻辑上，看起来也没啥问题；
    工具的行为是：接受这些guide command之前，会preverify；
    以a_d2来说，svf里面记录顺序是先guide merge，后guide reg constant；
    你看看这样修改一下svf是否可行: 把guide reg constant 放到guide merge 前面，用这个新的svf再跑一下你failed的session;

pigolo

好， 我去试试。谢谢

494693243

回复 8# pigolo


   楼主你的问题实验出的结果怎样啊因为我也遇到了svf 被rejected 的情况，完完全全不知道咋搞的

leadway1314

你这样写有什么用呢