Conformal ® LEC Logic Equivalence Checker是Cadence旗下的一款软件。最近我在项目中有用到这款工具完成VHDL和Verilog语言的逻辑一致性验证。网上关于这款工具使用方式的教程比较少,所以我花了很多时间去查阅官方的用户手册。在这篇文章里,我将给大家一步步介绍一下如何用这款工具完成逻辑一致性比较并消除所有的不一致关键点。针对大家很可能遇到的常见问题,我还会尽量列出所知的解决办法。
首先上一个参考脚本
[source lang="Tcl"]
vpxmode
reset
add notranslate modules a b c d
set naming rule -instance "%s" "%s_%d" "%s"
set naming rule -variable "%s" "%s" "%s"
set naming rule -mdportflatten -mdport_bitblast
set naming rule -parameter ""
set naming rule -instance_array "%s_%d"
set naming rule -enable_unnamed_blk_naming
add search path /some_path/some_dir
read design -golden -sensitive -norangeconstraint -continuousassignment bidirectional -nokeep_unreach -nosupply -lastmod -noelab \
-systemverilog -mapfile some_lib1 \
/some_path/some_dir/some_file1.v \
/some_path/some_dir/some_file2.v \
\
-systemverilog -mapfile some_lib2 \
/some_path/some_dir/some_file3.v \
/some_path/some_dir/some_file4.v \
\
read design -golden -continuousassignment bidirectional -norangeconstraint -nokeep_unreach -lastmod -noelab \
-vhdl 93 -mapfile some_lib1 \
/some_path/some_dir/some_file1.vhdl \
/some_path/some_dir/some_file2.vhdl \
\
-vhdl 93 -mapfile some_lib2 \
/some_path/some_dir/some_file3.vhdl \
/some_path/some_dir/some_file4.vhdl \
\
elaborate design -golden -root top_module_name
checkpoint a.ckpt -replace
add search path /some_path/some_dir
read design -revised -sensitive -norangeconstraint -continuousassignment bidirectional -nokeep_unreach -nosupply -lastmod -noelab \
-systemverilog -mapfile some_lib1 \
/some_path/some_dir/some_file1.v \
/some_path/some_dir/some_file2.v \
\
-systemverilog -mapfile some_lib2 \
/some_path/some_dir/some_file3.v \
/some_path/some_dir/some_file4.v \
\
read design -revised -continuousassignment bidirectional -norangeconstraint -nokeep_unreach -lastmod -noelab \
-vhdl 93 -mapfile some_lib1 \
/some_path/some_dir/some_file1.vhdl \
/some_path/some_dir/some_file2.vhdl \
\
-vhdl 93 -mapfile some_lib2 \
/some_path/some_dir/some_file3.vhdl \
/some_path/some_dir/some_file4.vhdl \
\
elaborate design -revised -root top_module_name
checkpoint b.ckpt -replace
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 analyze option -auto
set system mode lec
read mapped points some_map_file.map
analyze dc -remove_range_constraint
analyze datapath -module -verbose
usage
analyze datapath -verbose
report unmapped points -summary
report unmapped points -extra -unreachable -notmapped
add compared points -all
compare
checkpoint c.ckpt -replace
usage
report compare data -class nonequivalent -class abort -class notcompared
report verification -verbose
report statistics
vpxmode
[/source]
以下是重映射文件
[source lang="Tcl"]
add mapped points some_hierachy/some_module1 some_hierachy/some_module2 -type BBOX BBOX
add mapped points some_hierachy/some_module1 some_hierachy/some_module2 -input_pin module1_pin_name module2_pin_name -replace_pin_mapping -type BBOX BBOX
[/source]
以下是命令行
[source lang="bash"]
lec -Dofile i.do -Gui -LOGfile lec.log -XL
[/source]