求助，cadence LEC做形式验证，用时好长？

西边的鸵鸟

第一次接触形式化验证，使用cadence的LEC（服务器上没有formality），运行了1个晚上了，到现在还没有结束？这是为什么呢？
还有大神能告诉如何有效的做形式化验证，需要注意什么？第一次做，不懂。
这是我截取的图


谢谢给位前辈！！！！！！

icfbicfb

是rtl vs gate么，需要加载do文件吧，

西边的鸵鸟

回复 2# icfbicfb
是的，gate文件，也就是netlist文件是RTL通过综合工具RC综合后生成的。这个do文件是什么？如何产生呢？求版主告知如，多谢多谢！！！！

icfbicfb

rc 综合的时候产生的

do文件就是类似于svf，帮助pass lec的

设计多大规模

西边的鸵鸟

回复 4# icfbicfb
版主，我现在产生了do文件，在gui界面运行后，就退出了，这是怎么回事？版主你遇到过没？快愁死了。。。。

西边的鸵鸟

回复 4# icfbicfb
这是从RTL到intermediate.v（中间层 ungroup的）的do文件，是不是最后的exit -force，造成的闪退吗？
我试着把他注销了，也不行，还是运行完闪退。
// Generated by Cadence Encounter(R) RTL Compiler RC10.1.306 - v10.10-s357_1
tclmode
set env(RC_VERSION) "RC10.1.306 - v10.10-s357_1"
vpxmode
set dofile abort exit
usage -auto
// tclmode
// set env(CDN_SYNTH_ROOT) /usr/eda/cadence/RC101/tools.lnx86
// vpxmode
tclmode
set ver [lindex [split [lindex [get_version_info] 0] "-"] 0]
if {$ver >= 08.10} {
  vpx set naming style rc
}
vpxmode
set naming rule "%s_reg" -register -golden
set naming rule "%L.%s" "%L[%d].%s" "%s" -instance
set naming rule "%L.%s" "%L[%d].%s" "%s" -variable
set undefined cell black_box -noascend -both
set undriven signal Z -golden

add search path -library ../../tech_files/
read library -statetable -liberty  -both  \

tcb018gbwp7ttc.lib \

tpd018nvtc.lib

add search path -design ../verilog/
read design  -verilog -define SYNTHESIS  -golden -lastmod -noelab \

../verilog/clk_test.v \

../verilog/clk_test1.v \

../verilog/clk1.v \

../verilog/clk2.v

elaborate design -golden -root clk_test

read design -verilog -revised -lastmod -noelab \

intermediate.v

elaborate design -revised -root clk_test

report design data
report black box

uniquify -all -nolib
set flatten model -seq_constant -seq_constant_x_to 0
set flatten model -nodff_to_dlat_zero -nodff_to_dlat_feedback
// set parallel option -threads 4 -license xl
set analyze option -auto

set system mode lec
analyze datapath -module -verbose
usage
analyze datapath -verbose
// report mapped points
report unmapped points -summary
report unmapped points -extra -unreachable -notmapped
add compared points -all
// report compared points
compare
usage
// report compare data
report compare data -class nonequivalent -class abort -class notcompared
report verification -verbose
report statistics
tclmode
puts "No of compare points = [get_compare_points -count]"
puts "No of diff points    = [get_compare_points -diff -count]"
puts "No of abort points   = [get_compare_points -abort -count]"
puts "No of unknown points = [get_compare_points -unknown -count]"
if {[get_compare_points -count] == 0} {
    puts "---------------------------------"
    puts "ERROR: No compare points detected"
    puts "---------------------------------"
}
if {[get_compare_points -diff -count] > 0} {
    puts "------------------------------------"
    puts "ERROR: Different Key Points detected"
    puts "------------------------------------"
#     foreach i [get_compare_points -diff] {
#         vpx report test vector [get_keypoint $i]
#         puts "     ----------------------------"
#     }
}
if {[get_compare_points -abort -count] > 0} {
    puts "-----------------------------"
    puts "ERROR: Abort Points detected "
    puts "-----------------------------"
}
if {[get_compare_points -unknown -count] > 0} {
    puts "----------------------------------"
    puts "ERROR: Unknown Key Points detected"
    puts "----------------------------------"
}
vpxmode
exit -force

icfbicfb

不清楚，再研究下吧

西边的鸵鸟

回复 7# icfbicfb
恩，好，我再看看，麻烦版主了

didiaolanse

我也是刚刚接触这个，希望多交流，我也遇到过闪退，我把你代码第五行的set dofile abort exit，里面exit注释掉就可以了，不闪退了

stliutao

回复 5# 西边的鸵鸟


    到退出的时候已经运行完了