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

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

谢谢给位前辈！

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

是的，gate文件，也就是netlist文件是RTL通过综合工具RC综合后生成的。这个do文件是什么?如何产生呢?求小编告知如，多谢多谢！

rc 综合的时候产生的
do文件就是类似于svf，帮助pass lec的
设计多大规模

小编，我现在产生了do文件，在gui界面运行后，就退出了，这是怎么回事?小编你遇到过没?快愁死了。

这是从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

不清楚，再研究下吧

恩，好，我再看看，麻烦小编了

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

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

做multi-threading,效果很明晰