formality

socsd

刚开始接触formality，写了一个脚本用来匹配RTL代码和综合后的网表，出现的不匹配点非常多，不知道是自己写的脚本有问题还是综合的时候出现问题。想要哪位大侠提供一个正确的formality脚本，参考一下setup的设置。谢谢

zh123456789

同求啊

wodeqinshi

不太清楚

lixunwangsan

推荐用LEC

zfx253

Fm.tcl
  set VNET_LIST(r)        /disk2/user/epon/epon/STA/back-anno/0530/top_0530.v
  set VNET_LIST(i)        /disk2/user/epon/epon/STA/back-anno/0601/ECO_0530_3_Route.vg
  set TOP               top
  set DATE                [ sh date +%m%d%y ]
  set SESSION           FM_${TOP}_${DATE}
  
  sh rm -rf   ${SESSION}.run
  sh mkdir -p ${SESSION}.run
  
  source ./FM_setup.tcl
  source ./slow_lib.tcl
  
  read_verilog -container r -libname WORK $VNET_LIST(r)
  set_top r:/WORK/${TOP}
  
  read_verilog -container i -libname WORK $VNET_LIST(i)
  set_top i:/WORK/${TOP}
  
  match
  
  report_unmatched_points > ${SESSION}.run/report_unmatched_points.rpt
  report_matched_points   > ${SESSION}.run/report_matched_points.rpt
  
  set result [verify r:/WORK/${TOP} i:/WORK/${TOP}]
  
  report_failing > ${SESSION}.run/report_failing.rpt
  report_passing > ${SESSION}.run/report_passing.rpt
  report_aborted > ${SESSION}.run/report_aborted.rpt
  
  if { $result == 1 } {
          exit
  } else {
          start_gui
  }
  
Fm_setup.tcl
set sh_new_variable_message           "false"         ; # default = "true"
  set hdlin_auto_top                    "false"         ; # default = "false"
  set hdlin_unresolved_modules          "black_box"     ; # default = "error"
  set verification_failing_point_limit  999             ; # default = 20


slow_lib.tcl
set search_path {

        /disk2/user/epon/epon/LIB/synopsys/SC
        /disk2/user/epon/epon/LIB/synopsys/IO
        /disk2/user/epon/epon/LIB/synopsys/MEM
        }

  foreach path $search_path {
    foreach file [ glob -nocomplain $path/*.db ] {
       if { ( [ regexp {_ss\.db$} $file ] == 1 ) || ( [ regexp {_worst\.db$} $file ] == 1 )} {
           read_db $file
          }
        }
      }

运行的时候，首先在fm.tcl中把文件名改好，
然后直接输入 fm_shell –f fm.tcl 就可以了。当然我们也可以把这三个文件合成一个文件，进行处理。

vampire0078

谢谢楼上的

kafeijiatang198

谢谢！

icfbicfb

多谢分享！！！

formal 无论是synopsys的 formality还是 cadence 的lec， 都很简单的，
就几步：
1）read  lib/db
2) read reference netlist ( like RTL ) ,  golden one
3) read implementation netlist , gate level , revised one
3) match , verify , lec mode
4) report results

但是formal里面最难就是rtl 比gate了，  gate对gate很容易过，
比如综合后的和pr后的，  上面这个脚本做gate对gate肯定够了，

你可以先比较下gate对gate，
RTL 对gate 要debug下，有的不是formal脚本的问题

对了，你读了 svf么，dc输出的 , 能帮助formal过的

set_svf   default.svf

icfbicfb

scanreorder以后，要把 test_mode ,test_se tie到0上， formal才能过

也就是忽略scanreorder对 scanchain 顺序造成的影响

tigerajs

回复 5# zfx253
请教下report_unmatched_points有一堆不匹配的数据，但是report_failing的时候没有问题，是不是以后者为准