在线咨询
eetop公众号 创芯大讲堂 创芯人才网
切换到宽版

EETOP 创芯网论坛 (原名:电子顶级开发网)

手机号码,快捷登录

手机号码,快捷登录

找回密码

  登录   注册  

快捷导航
搜帖子
查看: 7403|回复: 10

[求助] formality问题求助!!!

[复制链接]
发表于 2018-1-5 10:38:07 | 显示全部楼层 |阅读模式

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

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

x
各位大侠,小弟用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,是根据什么方式推断的。
 楼主| 发表于 2018-1-5 11:15:35 | 显示全部楼层
在线等,请各位大侠出手相助,谢谢
发表于 2018-1-5 14:46:33 | 显示全部楼层
回复 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. wire [9:0] a = 10'b0;
  15. assign temp = (a_d1|a_d2|a_d3|a_d4|a_d5);
  16. always @(posedge clk)
  17.      begin
  18.               a_d1 <= a;
  19.               a_d2 <= a_d1;
  20.               a_d3 <= a_d2;
  21.               a_d4 <= a_d3;
  22.               a_d5 <= a_d4;
  23.     end
  24. endmodule


复制代码
 楼主| 发表于 2018-1-5 15:10:16 | 显示全部楼层
回复 3# sdlyyuxi


    这块代码是位于设计中较低层次的逻辑。fm的setup我只设置了跟scan相关的,就是将test_en = 0; 其他好像不需要什么setup的东西,
   芯片的顶层接口不是i2c就是模拟的,还有几个gpio
发表于 2018-1-5 15:29:16 | 显示全部楼层
回复 4# pigolo


    report_svf_operation -status rejected -command reg_constant
看一下为啥rejected
 楼主| 发表于 2018-1-5 15:36:47 | 显示全部楼层
我又综合了一版代码,上版是不带ICG和DFT,这一版将ICG插了进去,发现不报这个问题了,并且verify也过了,真是奇了怪了
发表于 2018-1-5 16:34:21 | 显示全部楼层
回复 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;
 楼主| 发表于 2018-1-5 16:47:31 | 显示全部楼层
好, 我去试试。谢谢
发表于 2018-7-6 16:31:08 | 显示全部楼层
回复 8# pigolo


   楼主你的问题实验出的结果怎样啊因为我也遇到了svf 被rejected 的情况,完完全全不知道咋搞的
发表于 2018-7-15 21:44:48 | 显示全部楼层
你这样写有什么用呢
您需要登录后才可以回帖 登录 | 注册

本版积分规则

关闭

站长推荐 上一条 /2 下一条


小黑屋| 手机版| 关于我们| 联系我们| 在线咨询| 隐私声明| EETOP 创芯网
( 京ICP备:10050787号 京公网安备:11010502037710 )

GMT+8, 2024-11-22 11:41 , Processed in 0.020457 second(s), 7 queries , Gzip On, Redis On.

eetop公众号 创芯大讲堂 创芯人才网
快速回复 返回顶部 返回列表