相关阅读
Formality
https://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.2014.3001.5482
Formality存在两个重要的概念：参考设计/实现设计和顶层设计，本文就将对此进行详细阐述。参考设计/实现设计是中两个重要的全局概念，在使用verify命令时，默认是对它们两者之中的比较点进行验证；而顶层设计则是属于一个容器的局部概念，每个容器只能拥有一个顶层设计，且确定之后就无法更改。
顶层设计
使用set_top命令可以将容器中某一个设计设置为顶层设计并进行展开(Elaborate)或者说链接(Link)时，Formality会在容器范围内解析引用并构建层次结构（只会对与顶层设计相关的设计进行解析），此后可以使用report_hierarchy命令报告层次中任意设计的结构。如果这个容器是默认容器r，则顶层设计还会被自动设置为参考设计；如果这个容器是默认容器i，则顶层设计还会被自动设置为实现设计。
参考设计/实现设计
使用set_reference_design命令将已设置顶层设计的容器中的某个设计设置为参考设计（要求必须在顶层设计的层次结构中），设置完成后用变量$ref表示；使用set_implementation_design命令将已设置顶层设计的容器中的某个设计设置为参考设计（要求必须在顶层设计的层次结构中），设置完成后用变量$ref表示。
虽然参考设计/实现设计常常不需要显式指定，它们在使用set_top命令指定默认容器r和i的顶层设计时就自动设置了，但会有一些特殊情况，比如层次化验证(hierarchical verification)过程中就是从下到上将层次结构中的各个设计设置为参考设计/实现设计依次进行验证，并在高层次验证时将低层次设置为黑盒来进行验证。
使用write_hierarchical_verification_script命令即可生成一个用于层次验证的脚本，该脚本应该在之前的验证基础上执行，下面是一个层次验证脚本的例子。
###
### Formality (R) hierarchical verification script: /home/zhangchen/Desktop/test1/hier.tcl
###
### Reference design: r:/WORK/TopModule
### Implementation design: i:/WORK/TopModule
### Generated Fri Jan 17 00:32:42 2025
###
global ref
global impl
global verification_constant_prop_mode
global signature_analysis_match_blackbox_input
global signature_analysis_match_blackbox_output
global signature_analysis_match_primary_input
global signature_analysis_match_primary_output
global verification_status
global fm_tmp_result_count
global fm_hier_result_array
redirect /home/zhangchen/Desktop/test1/fm_hier.log {echo "**************************************************************************************************"}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {echo "Results of hierarchical verification script: /home/zhangchen/Desktop/test1/hier.tcl"}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {echo "**************************************************************************************************"}
setup
if [info exists verification_constant_prop_mode] {
set fm_write_hier_saved_vars(verification_constant_prop_mode) $verification_constant_prop_mode
}
set verification_constant_prop_mode none
if [info exists signature_analysis_match_blackbox_input] {
set fm_write_hier_saved_vars(signature_analysis_match_blackbox_input) $signature_analysis_match_blackbox_input
}
set signature_analysis_match_blackbox_input false
if [info exists signature_analysis_match_blackbox_output] {
set fm_write_hier_saved_vars(signature_analysis_match_blackbox_output) $signature_analysis_match_blackbox_output
}
set signature_analysis_match_blackbox_output false
if [info exists signature_analysis_match_primary_input] {
set fm_write_hier_saved_vars(signature_analysis_match_primary_input) $signature_analysis_match_primary_input
}
set signature_analysis_match_primary_input false
if [info exists signature_analysis_match_primary_output] {
set fm_write_hier_saved_vars(signature_analysis_match_primary_output) $signature_analysis_match_primary_output
}
set signature_analysis_match_primary_output false
if [info exists fm_hier_result_array] {
unset fm_hier_result_array
}
set fm_hier_result_count 0
set fm_tmp_result_count 0
set fm_session_files_saved 0
set fm_save_file_limit 1
set fm_save_time_limit 0
proc get_verification_status {ref_inst imp_inst} {
global fm_tmp_result_count
global fm_hier_result_array
for {set i 0} {$i < $fm_tmp_result_count} {incr i} {
if [expr (![string compare [lindex $fm_hier_result_array([expr $i + 1]) 0] $ref_inst])] {
if [expr (![string compare [lindex $fm_hier_result_array([expr $i + 1]) 1] $imp_inst])] {
return [lindex $fm_hier_result_array([expr $i + 1]) 2]
}
}
}
return UNKNOWN
}
###
### Verifying instances:
### Ref: r:/WORK/TopModule/a1/c1
### Imp: i:/WORK/TopModule/a1/c1
###
set_reference_design r:/WORK/C_0
set_implementation_design i:/WORK/C_0
set_user_match -type port $impl/out[3] $ref/out[3]
set_user_match -type port $impl/out[2] $ref/out[2]
set_user_match -type port $impl/out[1] $ref/out[1]
set_user_match -type port $impl/out[0] $ref/out[0]
set_user_match -type port $impl/op_select $ref/op_select
set_user_match -type port $impl/input_a[3] $ref/input_a[3]
set_user_match -type port $impl/input_a[2] $ref/input_a[2]
set_user_match -type port $impl/input_a[1] $ref/input_a[1]
set_user_match -type port $impl/input_a[0] $ref/input_a[0]
set_user_match -type port $impl/input_b[3] $ref/input_b[3]
set_user_match -type port $impl/input_b[2] $ref/input_b[2]
set_user_match -type port $impl/input_b[1] $ref/input_b[1]
set_user_match -type port $impl/input_b[0] $ref/input_b[0]
set_user_match -type port $impl/clk $ref/clk
set_user_match -type port $impl/reset $ref/reset
set_constant -type port $ref/op_select 0
set_constant -type port $impl/op_select 0
set fm_begin_cputime [cputime]
verify
set fm_end_cputime [cputime]
set fm_this_verification_cputime [expr $fm_end_cputime - $fm_begin_cputime]
set fm_cumulative_memory [expr [memory] / 1000]
set fm_tmp_result_count [expr $fm_tmp_result_count + 1]
set fm_hier_result_array($fm_tmp_result_count) [list {r:/WORK/TopModule/a1/c1} {i:/WORK/TopModule/a1/c1} $verification_status]
set fm_failure_comment ""
if [expr (![string compare $verification_status "FAILED"])] {
set fm_failure_comment " (may be resolved in the parent level verification)"
}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " "}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format "Verification %s%s:" $verification_status $fm_failure_comment}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Ref: %s (instance of %s)" {r:/WORK/TopModule/a1/c1} $ref}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Imp: %s (instance of %s)" {i:/WORK/TopModule/a1/c1} $impl}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " %s, %4.0fMB (cumulative), %7.2fsec (incremental)" [date] $fm_cumulative_memory $fm_this_verification_cputime}
if [expr (![string compare $verification_status "INCONCLUSIVE"]) && \
($fm_session_files_saved < $fm_save_file_limit) && \
($fm_this_verification_cputime >= $fm_save_time_limit)] {
save_session -replace /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
lappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Session file: /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss"}
set fm_session_files_saved [expr $fm_session_files_saved + 1]
}
setup
remove_user_match -type port $impl/out[3]
remove_user_match -type port $impl/out[2]
remove_user_match -type port $impl/out[1]
remove_user_match -type port $impl/out[0]
remove_user_match -type port $impl/op_select
remove_user_match -type port $impl/input_a[3]
remove_user_match -type port $impl/input_a[2]
remove_user_match -type port $impl/input_a[1]
remove_user_match -type port $impl/input_a[0]
remove_user_match -type port $impl/input_b[3]
remove_user_match -type port $impl/input_b[2]
remove_user_match -type port $impl/input_b[1]
remove_user_match -type port $impl/input_b[0]
remove_user_match -type port $impl/clk
remove_user_match -type port $impl/reset
remove_constant -type port $ref/op_select
remove_constant -type port $impl/op_select
###
### Verifying instances:
### Ref: r:/WORK/TopModule/a1/c2
### Imp: i:/WORK/TopModule/a1/c2
###
set_reference_design r:/WORK/C_5
set_implementation_design i:/WORK/C_5
set_user_match -type port $impl/out[3] $ref/out[3]
set_user_match -type port $impl/out[2] $ref/out[2]
set_user_match -type port $impl/out[1] $ref/out[1]
set_user_match -type port $impl/out[0] $ref/out[0]
set_user_match -type port $impl/op_select $ref/op_select
set_user_match -type port $impl/input_a[3] $ref/input_a[3]
set_user_match -type port $impl/input_a[2] $ref/input_a[2]
set_user_match -type port $impl/input_a[1] $ref/input_a[1]
set_user_match -type port $impl/input_a[0] $ref/input_a[0]
set_user_match -type port $impl/input_b[3] $ref/input_b[3]
set_user_match -type port $impl/input_b[2] $ref/input_b[2]
set_user_match -type port $impl/input_b[1] $ref/input_b[1]
set_user_match -type port $impl/input_b[0] $ref/input_b[0]
set_user_match -type port $impl/clk $ref/clk
set_user_match -type port $impl/reset $ref/reset
set_constant -type port $ref/op_select 1
set_constant -type port $impl/op_select 1
set fm_begin_cputime [cputime]
verify
set fm_end_cputime [cputime]
set fm_this_verification_cputime [expr $fm_end_cputime - $fm_begin_cputime]
set fm_cumulative_memory [expr [memory] / 1000]
set fm_tmp_result_count [expr $fm_tmp_result_count + 1]
set fm_hier_result_array($fm_tmp_result_count) [list {r:/WORK/TopModule/a1/c2} {i:/WORK/TopModule/a1/c2} $verification_status]
set fm_failure_comment ""
if [expr (![string compare $verification_status "FAILED"])] {
set fm_failure_comment " (may be resolved in the parent level verification)"
}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " "}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format "Verification %s%s:" $verification_status $fm_failure_comment}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Ref: %s (instance of %s)" {r:/WORK/TopModule/a1/c2} $ref}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Imp: %s (instance of %s)" {i:/WORK/TopModule/a1/c2} $impl}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " %s, %4.0fMB (cumulative), %7.2fsec (incremental)" [date] $fm_cumulative_memory $fm_this_verification_cputime}
if [expr (![string compare $verification_status "INCONCLUSIVE"]) && \
($fm_session_files_saved < $fm_save_file_limit) && \
($fm_this_verification_cputime >= $fm_save_time_limit)] {
save_session -replace /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
lappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Session file: /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss"}
set fm_session_files_saved [expr $fm_session_files_saved + 1]
}
setup
remove_user_match -type port $impl/out[3]
remove_user_match -type port $impl/out[2]
remove_user_match -type port $impl/out[1]
remove_user_match -type port $impl/out[0]
remove_user_match -type port $impl/op_select
remove_user_match -type port $impl/input_a[3]
remove_user_match -type port $impl/input_a[2]
remove_user_match -type port $impl/input_a[1]
remove_user_match -type port $impl/input_a[0]
remove_user_match -type port $impl/input_b[3]
remove_user_match -type port $impl/input_b[2]
remove_user_match -type port $impl/input_b[1]
remove_user_match -type port $impl/input_b[0]
remove_user_match -type port $impl/clk
remove_user_match -type port $impl/reset
remove_constant -type port $ref/op_select
remove_constant -type port $impl/op_select
###
### Verifying instances:
### Ref: r:/WORK/TopModule/a1
### Imp: i:/WORK/TopModule/a1
###
set_reference_design r:/WORK/A_0
set_implementation_design i:/WORK/A_0
set at_least_one_black_box 0
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a1/c1} {i:/WORK/TopModule/a1/c1}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
set_black_box $ref/c1
set_black_box $impl/c1
set at_least_one_black_box 1
set_user_match -type cell $impl/c1 $ref/c1
set_user_match -type pin $impl/c1/out[3] $ref/c1/out[3]
set_user_match -type pin $impl/c1/out[2] $ref/c1/out[2]
set_user_match -type pin $impl/c1/out[1] $ref/c1/out[1]
set_user_match -type pin $impl/c1/out[0] $ref/c1/out[0]
set_user_match -type pin $impl/c1/op_select $ref/c1/op_select
set_user_match -type pin $impl/c1/input_a[3] $ref/c1/input_a[3]
set_user_match -type pin $impl/c1/input_a[2] $ref/c1/input_a[2]
set_user_match -type pin $impl/c1/input_a[1] $ref/c1/input_a[1]
set_user_match -type pin $impl/c1/input_a[0] $ref/c1/input_a[0]
set_user_match -type pin $impl/c1/input_b[3] $ref/c1/input_b[3]
set_user_match -type pin $impl/c1/input_b[2] $ref/c1/input_b[2]
set_user_match -type pin $impl/c1/input_b[1] $ref/c1/input_b[1]
set_user_match -type pin $impl/c1/input_b[0] $ref/c1/input_b[0]
set_user_match -type pin $impl/c1/clk $ref/c1/clk
set_user_match -type pin $impl/c1/reset $ref/c1/reset
}
if [expr true] {
}
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
# The following matched pin(s) are constant,
# therefore need not be verified at this level.
set_dont_verify_points -type pin $ref/c1/op_select
# The following matched pin(s) are constant,
# therefore need not be verified at this level.
set_dont_verify_points -type pin $impl/c1/op_select
}
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a1/c2} {i:/WORK/TopModule/a1/c2}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
set_black_box $ref/c2
set_black_box $impl/c2
set at_least_one_black_box 1
set_user_match -type cell $impl/c2 $ref/c2
set_user_match -type pin $impl/c2/out[3] $ref/c2/out[3]
set_user_match -type pin $impl/c2/out[2] $ref/c2/out[2]
set_user_match -type pin $impl/c2/out[1] $ref/c2/out[1]
set_user_match -type pin $impl/c2/out[0] $ref/c2/out[0]
set_user_match -type pin $impl/c2/op_select $ref/c2/op_select
set_user_match -type pin $impl/c2/input_a[3] $ref/c2/input_a[3]
set_user_match -type pin $impl/c2/input_a[2] $ref/c2/input_a[2]
set_user_match -type pin $impl/c2/input_a[1] $ref/c2/input_a[1]
set_user_match -type pin $impl/c2/input_a[0] $ref/c2/input_a[0]
set_user_match -type pin $impl/c2/input_b[3] $ref/c2/input_b[3]
set_user_match -type pin $impl/c2/input_b[2] $ref/c2/input_b[2]
set_user_match -type pin $impl/c2/input_b[1] $ref/c2/input_b[1]
set_user_match -type pin $impl/c2/input_b[0] $ref/c2/input_b[0]
set_user_match -type pin $impl/c2/clk $ref/c2/clk
set_user_match -type pin $impl/c2/reset $ref/c2/reset
}
if [expr true] {
}
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
# The following matched pin(s) are constant,
# therefore need not be verified at this level.
set_dont_verify_points -type pin $ref/c2/op_select
# The following matched pin(s) are constant,
# therefore need not be verified at this level.
set_dont_verify_points -type pin $impl/c2/op_select
}
set_user_match -type port $impl/out[3] $ref/out[3]
set_user_match -type port $impl/out[2] $ref/out[2]
set_user_match -type port $impl/out[1] $ref/out[1]
set_user_match -type port $impl/out[0] $ref/out[0]
set_user_match -type port $impl/input_a[3] $ref/input_a[3]
set_user_match -type port $impl/input_a[2] $ref/input_a[2]
set_user_match -type port $impl/input_a[1] $ref/input_a[1]
set_user_match -type port $impl/input_a[0] $ref/input_a[0]
set_user_match -type port $impl/input_b[3] $ref/input_b[3]
set_user_match -type port $impl/input_b[2] $ref/input_b[2]
set_user_match -type port $impl/input_b[1] $ref/input_b[1]
set_user_match -type port $impl/input_b[0] $ref/input_b[0]
set_user_match -type port $impl/clk $ref/clk
set_user_match -type port $impl/reset $ref/reset
set_dont_match -type port $ref/c_out_1[3]
set_dont_match -type port $ref/c_out_1[2]
set_dont_match -type port $ref/c_out_1[1]
set_dont_match -type port $ref/c_out_1[0]
set_dont_match -type port $ref/c_out_2[3]
set_dont_match -type port $ref/c_out_2[2]
set_dont_match -type port $ref/c_out_2[1]
set_dont_match -type port $ref/c_out_2[0]
set_dont_match -type port $impl/c_out_1[3]
set_dont_match -type port $impl/c_out_1[2]
set_dont_match -type port $impl/c_out_1[1]
set_dont_match -type port $impl/c_out_1[0]
set_dont_match -type port $impl/c_out_2[3]
set_dont_match -type port $impl/c_out_2[2]
set_dont_match -type port $impl/c_out_2[1]
set_dont_match -type port $impl/c_out_2[0]
# The following unmatched port(s) will cause verification failure at higher level if used there,
# therefore need not cause verification failure at this level.
set_dont_verify_points -type port $ref/c_out_1[3]
set_dont_verify_points -type port $ref/c_out_1[2]
set_dont_verify_points -type port $ref/c_out_1[1]
set_dont_verify_points -type port $ref/c_out_1[0]
set_dont_verify_points -type port $ref/c_out_2[3]
set_dont_verify_points -type port $ref/c_out_2[2]
set_dont_verify_points -type port $ref/c_out_2[1]
set_dont_verify_points -type port $ref/c_out_2[0]
# The following unmatched port(s) will cause verification failure at higher level if used there,
# therefore need not cause verification failure at this level.
set_dont_verify_points -type port $impl/c_out_1[3]
set_dont_verify_points -type port $impl/c_out_1[2]
set_dont_verify_points -type port $impl/c_out_1[1]
set_dont_verify_points -type port $impl/c_out_1[0]
set_dont_verify_points -type port $impl/c_out_2[3]
set_dont_verify_points -type port $impl/c_out_2[2]
set_dont_verify_points -type port $impl/c_out_2[1]
set_dont_verify_points -type port $impl/c_out_2[0]
set fm_begin_cputime [cputime]
verify
if [expr ($at_least_one_black_box) && \
(![string compare $verification_status "FAILED"])] {
setup
set at_least_one_black_box 0
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a1/c1} {i:/WORK/TopModule/a1/c1}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/c1
remove_black_box $impl/c1
remove_user_match -type cell $impl/c1
remove_user_match -type pin $impl/c1/out[3]
remove_user_match -type pin $impl/c1/out[2]
remove_user_match -type pin $impl/c1/out[1]
remove_user_match -type pin $impl/c1/out[0]
remove_user_match -type pin $impl/c1/op_select
remove_user_match -type pin $impl/c1/input_a[3]
remove_user_match -type pin $impl/c1/input_a[2]
remove_user_match -type pin $impl/c1/input_a[1]
remove_user_match -type pin $impl/c1/input_a[0]
remove_user_match -type pin $impl/c1/input_b[3]
remove_user_match -type pin $impl/c1/input_b[2]
remove_user_match -type pin $impl/c1/input_b[1]
remove_user_match -type pin $impl/c1/input_b[0]
remove_user_match -type pin $impl/c1/clk
remove_user_match -type pin $impl/c1/reset
remove_dont_verify_points -type pin $ref/c1/op_select
remove_dont_verify_points -type pin $impl/c1/op_select
}
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a1/c2} {i:/WORK/TopModule/a1/c2}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/c2
remove_black_box $impl/c2
remove_user_match -type cell $impl/c2
remove_user_match -type pin $impl/c2/out[3]
remove_user_match -type pin $impl/c2/out[2]
remove_user_match -type pin $impl/c2/out[1]
remove_user_match -type pin $impl/c2/out[0]
remove_user_match -type pin $impl/c2/op_select
remove_user_match -type pin $impl/c2/input_a[3]
remove_user_match -type pin $impl/c2/input_a[2]
remove_user_match -type pin $impl/c2/input_a[1]
remove_user_match -type pin $impl/c2/input_a[0]
remove_user_match -type pin $impl/c2/input_b[3]
remove_user_match -type pin $impl/c2/input_b[2]
remove_user_match -type pin $impl/c2/input_b[1]
remove_user_match -type pin $impl/c2/input_b[0]
remove_user_match -type pin $impl/c2/clk
remove_user_match -type pin $impl/c2/reset
remove_dont_verify_points -type pin $ref/c2/op_select
remove_dont_verify_points -type pin $impl/c2/op_select
}
verify
}
set fm_end_cputime [cputime]
set fm_this_verification_cputime [expr $fm_end_cputime - $fm_begin_cputime]
set fm_cumulative_memory [expr [memory] / 1000]
set fm_tmp_result_count [expr $fm_tmp_result_count + 1]
set fm_hier_result_array($fm_tmp_result_count) [list {r:/WORK/TopModule/a1} {i:/WORK/TopModule/a1} $verification_status]
set fm_failure_comment ""
if [expr (![string compare $verification_status "FAILED"])] {
set fm_failure_comment " (may be resolved in the parent level verification)"
}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " "}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format "Verification %s%s:" $verification_status $fm_failure_comment}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Ref: %s (instance of %s)" {r:/WORK/TopModule/a1} $ref}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Imp: %s (instance of %s)" {i:/WORK/TopModule/a1} $impl}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " %s, %4.0fMB (cumulative), %7.2fsec (incremental)" [date] $fm_cumulative_memory $fm_this_verification_cputime}
if [expr (![string compare $verification_status "INCONCLUSIVE"]) && \
($fm_session_files_saved < $fm_save_file_limit) && \
($fm_this_verification_cputime >= $fm_save_time_limit)] {
save_session -replace /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
lappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Session file: /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss"}
set fm_session_files_saved [expr $fm_session_files_saved + 1]
}
setup
if [expr ($at_least_one_black_box)] {
set at_least_one_black_box 0
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a1/c1} {i:/WORK/TopModule/a1/c1}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/c1
remove_black_box $impl/c1
remove_user_match -type cell $impl/c1
remove_user_match -type pin $impl/c1/out[3]
remove_user_match -type pin $impl/c1/out[2]
remove_user_match -type pin $impl/c1/out[1]
remove_user_match -type pin $impl/c1/out[0]
remove_user_match -type pin $impl/c1/op_select
remove_user_match -type pin $impl/c1/input_a[3]
remove_user_match -type pin $impl/c1/input_a[2]
remove_user_match -type pin $impl/c1/input_a[1]
remove_user_match -type pin $impl/c1/input_a[0]
remove_user_match -type pin $impl/c1/input_b[3]
remove_user_match -type pin $impl/c1/input_b[2]
remove_user_match -type pin $impl/c1/input_b[1]
remove_user_match -type pin $impl/c1/input_b[0]
remove_user_match -type pin $impl/c1/clk
remove_user_match -type pin $impl/c1/reset
remove_dont_verify_points -type pin $ref/c1/op_select
remove_dont_verify_points -type pin $impl/c1/op_select
}
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a1/c2} {i:/WORK/TopModule/a1/c2}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/c2
remove_black_box $impl/c2
remove_user_match -type cell $impl/c2
remove_user_match -type pin $impl/c2/out[3]
remove_user_match -type pin $impl/c2/out[2]
remove_user_match -type pin $impl/c2/out[1]
remove_user_match -type pin $impl/c2/out[0]
remove_user_match -type pin $impl/c2/op_select
remove_user_match -type pin $impl/c2/input_a[3]
remove_user_match -type pin $impl/c2/input_a[2]
remove_user_match -type pin $impl/c2/input_a[1]
remove_user_match -type pin $impl/c2/input_a[0]
remove_user_match -type pin $impl/c2/input_b[3]
remove_user_match -type pin $impl/c2/input_b[2]
remove_user_match -type pin $impl/c2/input_b[1]
remove_user_match -type pin $impl/c2/input_b[0]
remove_user_match -type pin $impl/c2/clk
remove_user_match -type pin $impl/c2/reset
remove_dont_verify_points -type pin $ref/c2/op_select
remove_dont_verify_points -type pin $impl/c2/op_select
}
}
remove_user_match -type port $impl/out[3]
remove_user_match -type port $impl/out[2]
remove_user_match -type port $impl/out[1]
remove_user_match -type port $impl/out[0]
remove_user_match -type port $impl/input_a[3]
remove_user_match -type port $impl/input_a[2]
remove_user_match -type port $impl/input_a[1]
remove_user_match -type port $impl/input_a[0]
remove_user_match -type port $impl/input_b[3]
remove_user_match -type port $impl/input_b[2]
remove_user_match -type port $impl/input_b[1]
remove_user_match -type port $impl/input_b[0]
remove_user_match -type port $impl/clk
remove_user_match -type port $impl/reset
remove_dont_match -type port $ref/c_out_1[3]
remove_dont_match -type port $ref/c_out_1[2]
remove_dont_match -type port $ref/c_out_1[1]
remove_dont_match -type port $ref/c_out_1[0]
remove_dont_match -type port $ref/c_out_2[3]
remove_dont_match -type port $ref/c_out_2[2]
remove_dont_match -type port $ref/c_out_2[1]
remove_dont_match -type port $ref/c_out_2[0]
remove_dont_match -type port $impl/c_out_1[3]
remove_dont_match -type port $impl/c_out_1[2]
remove_dont_match -type port $impl/c_out_1[1]
remove_dont_match -type port $impl/c_out_1[0]
remove_dont_match -type port $impl/c_out_2[3]
remove_dont_match -type port $impl/c_out_2[2]
remove_dont_match -type port $impl/c_out_2[1]
remove_dont_match -type port $impl/c_out_2[0]
remove_dont_verify_points -type port $ref/c_out_1[3]
remove_dont_verify_points -type port $ref/c_out_1[2]
remove_dont_verify_points -type port $ref/c_out_1[1]
remove_dont_verify_points -type port $ref/c_out_1[0]
remove_dont_verify_points -type port $ref/c_out_2[3]
remove_dont_verify_points -type port $ref/c_out_2[2]
remove_dont_verify_points -type port $ref/c_out_2[1]
remove_dont_verify_points -type port $ref/c_out_2[0]
remove_dont_verify_points -type port $impl/c_out_1[3]
remove_dont_verify_points -type port $impl/c_out_1[2]
remove_dont_verify_points -type port $impl/c_out_1[1]
remove_dont_verify_points -type port $impl/c_out_1[0]
remove_dont_verify_points -type port $impl/c_out_2[3]
remove_dont_verify_points -type port $impl/c_out_2[2]
remove_dont_verify_points -type port $impl/c_out_2[1]
remove_dont_verify_points -type port $impl/c_out_2[0]
###
### Verifying instances:
### Ref: r:/WORK/TopModule/a2/c1
### Imp: i:/WORK/TopModule/a2/c1
###
set_reference_design r:/WORK/C_4
set_implementation_design i:/WORK/C_4
set_user_match -type port $impl/out[3] $ref/out[3]
set_user_match -type port $impl/out[2] $ref/out[2]
set_user_match -type port $impl/out[1] $ref/out[1]
set_user_match -type port $impl/out[0] $ref/out[0]
set_user_match -type port $impl/op_select $ref/op_select
set_user_match -type port $impl/input_a[3] $ref/input_a[3]
set_user_match -type port $impl/input_a[2] $ref/input_a[2]
set_user_match -type port $impl/input_a[1] $ref/input_a[1]
set_user_match -type port $impl/input_a[0] $ref/input_a[0]
set_user_match -type port $impl/input_b[3] $ref/input_b[3]
set_user_match -type port $impl/input_b[2] $ref/input_b[2]
set_user_match -type port $impl/input_b[1] $ref/input_b[1]
set_user_match -type port $impl/input_b[0] $ref/input_b[0]
set_user_match -type port $impl/clk $ref/clk
set_user_match -type port $impl/reset $ref/reset
set_constant -type port $ref/op_select 0
set_constant -type port $impl/op_select 0
set fm_begin_cputime [cputime]
verify
set fm_end_cputime [cputime]
set fm_this_verification_cputime [expr $fm_end_cputime - $fm_begin_cputime]
set fm_cumulative_memory [expr [memory] / 1000]
set fm_tmp_result_count [expr $fm_tmp_result_count + 1]
set fm_hier_result_array($fm_tmp_result_count) [list {r:/WORK/TopModule/a2/c1} {i:/WORK/TopModule/a2/c1} $verification_status]
set fm_failure_comment ""
if [expr (![string compare $verification_status "FAILED"])] {
set fm_failure_comment " (may be resolved in the parent level verification)"
}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " "}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format "Verification %s%s:" $verification_status $fm_failure_comment}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Ref: %s (instance of %s)" {r:/WORK/TopModule/a2/c1} $ref}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Imp: %s (instance of %s)" {i:/WORK/TopModule/a2/c1} $impl}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " %s, %4.0fMB (cumulative), %7.2fsec (incremental)" [date] $fm_cumulative_memory $fm_this_verification_cputime}
if [expr (![string compare $verification_status "INCONCLUSIVE"]) && \
($fm_session_files_saved < $fm_save_file_limit) && \
($fm_this_verification_cputime >= $fm_save_time_limit)] {
save_session -replace /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
lappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Session file: /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss"}
set fm_session_files_saved [expr $fm_session_files_saved + 1]
}
setup
remove_user_match -type port $impl/out[3]
remove_user_match -type port $impl/out[2]
remove_user_match -type port $impl/out[1]
remove_user_match -type port $impl/out[0]
remove_user_match -type port $impl/op_select
remove_user_match -type port $impl/input_a[3]
remove_user_match -type port $impl/input_a[2]
remove_user_match -type port $impl/input_a[1]
remove_user_match -type port $impl/input_a[0]
remove_user_match -type port $impl/input_b[3]
remove_user_match -type port $impl/input_b[2]
remove_user_match -type port $impl/input_b[1]
remove_user_match -type port $impl/input_b[0]
remove_user_match -type port $impl/clk
remove_user_match -type port $impl/reset
remove_constant -type port $ref/op_select
remove_constant -type port $impl/op_select
###
### Verifying instances:
### Ref: r:/WORK/TopModule/a2/c2
### Imp: i:/WORK/TopModule/a2/c2
###
set_reference_design r:/WORK/C_3
set_implementation_design i:/WORK/C_3
set_user_match -type port $impl/out[3] $ref/out[3]
set_user_match -type port $impl/out[2] $ref/out[2]
set_user_match -type port $impl/out[1] $ref/out[1]
set_user_match -type port $impl/out[0] $ref/out[0]
set_user_match -type port $impl/op_select $ref/op_select
set_user_match -type port $impl/input_a[3] $ref/input_a[3]
set_user_match -type port $impl/input_a[2] $ref/input_a[2]
set_user_match -type port $impl/input_a[1] $ref/input_a[1]
set_user_match -type port $impl/input_a[0] $ref/input_a[0]
set_user_match -type port $impl/input_b[3] $ref/input_b[3]
set_user_match -type port $impl/input_b[2] $ref/input_b[2]
set_user_match -type port $impl/input_b[1] $ref/input_b[1]
set_user_match -type port $impl/input_b[0] $ref/input_b[0]
set_user_match -type port $impl/clk $ref/clk
set_user_match -type port $impl/reset $ref/reset
set_constant -type port $ref/op_select 1
set_constant -type port $impl/op_select 1
set fm_begin_cputime [cputime]
verify
set fm_end_cputime [cputime]
set fm_this_verification_cputime [expr $fm_end_cputime - $fm_begin_cputime]
set fm_cumulative_memory [expr [memory] / 1000]
set fm_tmp_result_count [expr $fm_tmp_result_count + 1]
set fm_hier_result_array($fm_tmp_result_count) [list {r:/WORK/TopModule/a2/c2} {i:/WORK/TopModule/a2/c2} $verification_status]
set fm_failure_comment ""
if [expr (![string compare $verification_status "FAILED"])] {
set fm_failure_comment " (may be resolved in the parent level verification)"
}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " "}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format "Verification %s%s:" $verification_status $fm_failure_comment}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Ref: %s (instance of %s)" {r:/WORK/TopModule/a2/c2} $ref}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Imp: %s (instance of %s)" {i:/WORK/TopModule/a2/c2} $impl}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " %s, %4.0fMB (cumulative), %7.2fsec (incremental)" [date] $fm_cumulative_memory $fm_this_verification_cputime}
if [expr (![string compare $verification_status "INCONCLUSIVE"]) && \
($fm_session_files_saved < $fm_save_file_limit) && \
($fm_this_verification_cputime >= $fm_save_time_limit)] {
save_session -replace /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
lappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Session file: /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss"}
set fm_session_files_saved [expr $fm_session_files_saved + 1]
}
setup
remove_user_match -type port $impl/out[3]
remove_user_match -type port $impl/out[2]
remove_user_match -type port $impl/out[1]
remove_user_match -type port $impl/out[0]
remove_user_match -type port $impl/op_select
remove_user_match -type port $impl/input_a[3]
remove_user_match -type port $impl/input_a[2]
remove_user_match -type port $impl/input_a[1]
remove_user_match -type port $impl/input_a[0]
remove_user_match -type port $impl/input_b[3]
remove_user_match -type port $impl/input_b[2]
remove_user_match -type port $impl/input_b[1]
remove_user_match -type port $impl/input_b[0]
remove_user_match -type port $impl/clk
remove_user_match -type port $impl/reset
remove_constant -type port $ref/op_select
remove_constant -type port $impl/op_select
###
### Verifying instances:
### Ref: r:/WORK/TopModule/a2
### Imp: i:/WORK/TopModule/a2
###
set_reference_design r:/WORK/A_2
set_implementation_design i:/WORK/A_2
set at_least_one_black_box 0
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a2/c1} {i:/WORK/TopModule/a2/c1}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
set_black_box $ref/c1
set_black_box $impl/c1
set at_least_one_black_box 1
set_user_match -type cell $impl/c1 $ref/c1
set_user_match -type pin $impl/c1/out[3] $ref/c1/out[3]
set_user_match -type pin $impl/c1/out[2] $ref/c1/out[2]
set_user_match -type pin $impl/c1/out[1] $ref/c1/out[1]
set_user_match -type pin $impl/c1/out[0] $ref/c1/out[0]
set_user_match -type pin $impl/c1/op_select $ref/c1/op_select
set_user_match -type pin $impl/c1/input_a[3] $ref/c1/input_a[3]
set_user_match -type pin $impl/c1/input_a[2] $ref/c1/input_a[2]
set_user_match -type pin $impl/c1/input_a[1] $ref/c1/input_a[1]
set_user_match -type pin $impl/c1/input_a[0] $ref/c1/input_a[0]
set_user_match -type pin $impl/c1/input_b[3] $ref/c1/input_b[3]
set_user_match -type pin $impl/c1/input_b[2] $ref/c1/input_b[2]
set_user_match -type pin $impl/c1/input_b[1] $ref/c1/input_b[1]
set_user_match -type pin $impl/c1/input_b[0] $ref/c1/input_b[0]
set_user_match -type pin $impl/c1/clk $ref/c1/clk
set_user_match -type pin $impl/c1/reset $ref/c1/reset
}
if [expr true] {
}
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
# The following matched pin(s) are constant,
# therefore need not be verified at this level.
set_dont_verify_points -type pin $ref/c1/op_select
# The following matched pin(s) are constant,
# therefore need not be verified at this level.
set_dont_verify_points -type pin $impl/c1/op_select
}
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a2/c2} {i:/WORK/TopModule/a2/c2}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
set_black_box $ref/c2
set_black_box $impl/c2
set at_least_one_black_box 1
set_user_match -type cell $impl/c2 $ref/c2
set_user_match -type pin $impl/c2/out[3] $ref/c2/out[3]
set_user_match -type pin $impl/c2/out[2] $ref/c2/out[2]
set_user_match -type pin $impl/c2/out[1] $ref/c2/out[1]
set_user_match -type pin $impl/c2/out[0] $ref/c2/out[0]
set_user_match -type pin $impl/c2/op_select $ref/c2/op_select
set_user_match -type pin $impl/c2/input_a[3] $ref/c2/input_a[3]
set_user_match -type pin $impl/c2/input_a[2] $ref/c2/input_a[2]
set_user_match -type pin $impl/c2/input_a[1] $ref/c2/input_a[1]
set_user_match -type pin $impl/c2/input_a[0] $ref/c2/input_a[0]
set_user_match -type pin $impl/c2/input_b[3] $ref/c2/input_b[3]
set_user_match -type pin $impl/c2/input_b[2] $ref/c2/input_b[2]
set_user_match -type pin $impl/c2/input_b[1] $ref/c2/input_b[1]
set_user_match -type pin $impl/c2/input_b[0] $ref/c2/input_b[0]
set_user_match -type pin $impl/c2/clk $ref/c2/clk
set_user_match -type pin $impl/c2/reset $ref/c2/reset
}
if [expr true] {
}
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
# The following matched pin(s) are constant,
# therefore need not be verified at this level.
set_dont_verify_points -type pin $ref/c2/op_select
# The following matched pin(s) are constant,
# therefore need not be verified at this level.
set_dont_verify_points -type pin $impl/c2/op_select
}
set_user_match -type port $impl/out[3] $ref/out[3]
set_user_match -type port $impl/out[2] $ref/out[2]
set_user_match -type port $impl/out[1] $ref/out[1]
set_user_match -type port $impl/out[0] $ref/out[0]
set_user_match -type port $impl/input_a[3] $ref/input_a[3]
set_user_match -type port $impl/input_a[2] $ref/input_a[2]
set_user_match -type port $impl/input_a[1] $ref/input_a[1]
set_user_match -type port $impl/input_a[0] $ref/input_a[0]
set_user_match -type port $impl/input_b[3] $ref/input_b[3]
set_user_match -type port $impl/input_b[2] $ref/input_b[2]
set_user_match -type port $impl/input_b[1] $ref/input_b[1]
set_user_match -type port $impl/input_b[0] $ref/input_b[0]
set_user_match -type port $impl/clk $ref/clk
set_user_match -type port $impl/reset $ref/reset
set_dont_match -type port $ref/c_out_1[3]
set_dont_match -type port $ref/c_out_1[2]
set_dont_match -type port $ref/c_out_1[1]
set_dont_match -type port $ref/c_out_1[0]
set_dont_match -type port $ref/c_out_2[3]
set_dont_match -type port $ref/c_out_2[2]
set_dont_match -type port $ref/c_out_2[1]
set_dont_match -type port $ref/c_out_2[0]
set_dont_match -type port $impl/c_out_1[3]
set_dont_match -type port $impl/c_out_1[2]
set_dont_match -type port $impl/c_out_1[1]
set_dont_match -type port $impl/c_out_1[0]
set_dont_match -type port $impl/c_out_2[3]
set_dont_match -type port $impl/c_out_2[2]
set_dont_match -type port $impl/c_out_2[1]
set_dont_match -type port $impl/c_out_2[0]
# The following unmatched port(s) will cause verification failure at higher level if used there,
# therefore need not cause verification failure at this level.
set_dont_verify_points -type port $ref/c_out_1[3]
set_dont_verify_points -type port $ref/c_out_1[2]
set_dont_verify_points -type port $ref/c_out_1[1]
set_dont_verify_points -type port $ref/c_out_1[0]
set_dont_verify_points -type port $ref/c_out_2[3]
set_dont_verify_points -type port $ref/c_out_2[2]
set_dont_verify_points -type port $ref/c_out_2[1]
set_dont_verify_points -type port $ref/c_out_2[0]
# The following unmatched port(s) will cause verification failure at higher level if used there,
# therefore need not cause verification failure at this level.
set_dont_verify_points -type port $impl/c_out_1[3]
set_dont_verify_points -type port $impl/c_out_1[2]
set_dont_verify_points -type port $impl/c_out_1[1]
set_dont_verify_points -type port $impl/c_out_1[0]
set_dont_verify_points -type port $impl/c_out_2[3]
set_dont_verify_points -type port $impl/c_out_2[2]
set_dont_verify_points -type port $impl/c_out_2[1]
set_dont_verify_points -type port $impl/c_out_2[0]
set fm_begin_cputime [cputime]
verify
if [expr ($at_least_one_black_box) && \
(![string compare $verification_status "FAILED"])] {
setup
set at_least_one_black_box 0
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a2/c1} {i:/WORK/TopModule/a2/c1}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/c1
remove_black_box $impl/c1
remove_user_match -type cell $impl/c1
remove_user_match -type pin $impl/c1/out[3]
remove_user_match -type pin $impl/c1/out[2]
remove_user_match -type pin $impl/c1/out[1]
remove_user_match -type pin $impl/c1/out[0]
remove_user_match -type pin $impl/c1/op_select
remove_user_match -type pin $impl/c1/input_a[3]
remove_user_match -type pin $impl/c1/input_a[2]
remove_user_match -type pin $impl/c1/input_a[1]
remove_user_match -type pin $impl/c1/input_a[0]
remove_user_match -type pin $impl/c1/input_b[3]
remove_user_match -type pin $impl/c1/input_b[2]
remove_user_match -type pin $impl/c1/input_b[1]
remove_user_match -type pin $impl/c1/input_b[0]
remove_user_match -type pin $impl/c1/clk
remove_user_match -type pin $impl/c1/reset
remove_dont_verify_points -type pin $ref/c1/op_select
remove_dont_verify_points -type pin $impl/c1/op_select
}
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a2/c2} {i:/WORK/TopModule/a2/c2}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/c2
remove_black_box $impl/c2
remove_user_match -type cell $impl/c2
remove_user_match -type pin $impl/c2/out[3]
remove_user_match -type pin $impl/c2/out[2]
remove_user_match -type pin $impl/c2/out[1]
remove_user_match -type pin $impl/c2/out[0]
remove_user_match -type pin $impl/c2/op_select
remove_user_match -type pin $impl/c2/input_a[3]
remove_user_match -type pin $impl/c2/input_a[2]
remove_user_match -type pin $impl/c2/input_a[1]
remove_user_match -type pin $impl/c2/input_a[0]
remove_user_match -type pin $impl/c2/input_b[3]
remove_user_match -type pin $impl/c2/input_b[2]
remove_user_match -type pin $impl/c2/input_b[1]
remove_user_match -type pin $impl/c2/input_b[0]
remove_user_match -type pin $impl/c2/clk
remove_user_match -type pin $impl/c2/reset
remove_dont_verify_points -type pin $ref/c2/op_select
remove_dont_verify_points -type pin $impl/c2/op_select
}
verify
}
set fm_end_cputime [cputime]
set fm_this_verification_cputime [expr $fm_end_cputime - $fm_begin_cputime]
set fm_cumulative_memory [expr [memory] / 1000]
set fm_tmp_result_count [expr $fm_tmp_result_count + 1]
set fm_hier_result_array($fm_tmp_result_count) [list {r:/WORK/TopModule/a2} {i:/WORK/TopModule/a2} $verification_status]
set fm_failure_comment ""
if [expr (![string compare $verification_status "FAILED"])] {
set fm_failure_comment " (may be resolved in the parent level verification)"
}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " "}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format "Verification %s%s:" $verification_status $fm_failure_comment}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Ref: %s (instance of %s)" {r:/WORK/TopModule/a2} $ref}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Imp: %s (instance of %s)" {i:/WORK/TopModule/a2} $impl}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " %s, %4.0fMB (cumulative), %7.2fsec (incremental)" [date] $fm_cumulative_memory $fm_this_verification_cputime}
if [expr (![string compare $verification_status "INCONCLUSIVE"]) && \
($fm_session_files_saved < $fm_save_file_limit) && \
($fm_this_verification_cputime >= $fm_save_time_limit)] {
save_session -replace /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
lappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Session file: /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss"}
set fm_session_files_saved [expr $fm_session_files_saved + 1]
}
setup
if [expr ($at_least_one_black_box)] {
set at_least_one_black_box 0
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a2/c1} {i:/WORK/TopModule/a2/c1}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/c1
remove_black_box $impl/c1
remove_user_match -type cell $impl/c1
remove_user_match -type pin $impl/c1/out[3]
remove_user_match -type pin $impl/c1/out[2]
remove_user_match -type pin $impl/c1/out[1]
remove_user_match -type pin $impl/c1/out[0]
remove_user_match -type pin $impl/c1/op_select
remove_user_match -type pin $impl/c1/input_a[3]
remove_user_match -type pin $impl/c1/input_a[2]
remove_user_match -type pin $impl/c1/input_a[1]
remove_user_match -type pin $impl/c1/input_a[0]
remove_user_match -type pin $impl/c1/input_b[3]
remove_user_match -type pin $impl/c1/input_b[2]
remove_user_match -type pin $impl/c1/input_b[1]
remove_user_match -type pin $impl/c1/input_b[0]
remove_user_match -type pin $impl/c1/clk
remove_user_match -type pin $impl/c1/reset
remove_dont_verify_points -type pin $ref/c1/op_select
remove_dont_verify_points -type pin $impl/c1/op_select
}
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a2/c2} {i:/WORK/TopModule/a2/c2}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/c2
remove_black_box $impl/c2
remove_user_match -type cell $impl/c2
remove_user_match -type pin $impl/c2/out[3]
remove_user_match -type pin $impl/c2/out[2]
remove_user_match -type pin $impl/c2/out[1]
remove_user_match -type pin $impl/c2/out[0]
remove_user_match -type pin $impl/c2/op_select
remove_user_match -type pin $impl/c2/input_a[3]
remove_user_match -type pin $impl/c2/input_a[2]
remove_user_match -type pin $impl/c2/input_a[1]
remove_user_match -type pin $impl/c2/input_a[0]
remove_user_match -type pin $impl/c2/input_b[3]
remove_user_match -type pin $impl/c2/input_b[2]
remove_user_match -type pin $impl/c2/input_b[1]
remove_user_match -type pin $impl/c2/input_b[0]
remove_user_match -type pin $impl/c2/clk
remove_user_match -type pin $impl/c2/reset
remove_dont_verify_points -type pin $ref/c2/op_select
remove_dont_verify_points -type pin $impl/c2/op_select
}
}
remove_user_match -type port $impl/out[3]
remove_user_match -type port $impl/out[2]
remove_user_match -type port $impl/out[1]
remove_user_match -type port $impl/out[0]
remove_user_match -type port $impl/input_a[3]
remove_user_match -type port $impl/input_a[2]
remove_user_match -type port $impl/input_a[1]
remove_user_match -type port $impl/input_a[0]
remove_user_match -type port $impl/input_b[3]
remove_user_match -type port $impl/input_b[2]
remove_user_match -type port $impl/input_b[1]
remove_user_match -type port $impl/input_b[0]
remove_user_match -type port $impl/clk
remove_user_match -type port $impl/reset
remove_dont_match -type port $ref/c_out_1[3]
remove_dont_match -type port $ref/c_out_1[2]
remove_dont_match -type port $ref/c_out_1[1]
remove_dont_match -type port $ref/c_out_1[0]
remove_dont_match -type port $ref/c_out_2[3]
remove_dont_match -type port $ref/c_out_2[2]
remove_dont_match -type port $ref/c_out_2[1]
remove_dont_match -type port $ref/c_out_2[0]
remove_dont_match -type port $impl/c_out_1[3]
remove_dont_match -type port $impl/c_out_1[2]
remove_dont_match -type port $impl/c_out_1[1]
remove_dont_match -type port $impl/c_out_1[0]
remove_dont_match -type port $impl/c_out_2[3]
remove_dont_match -type port $impl/c_out_2[2]
remove_dont_match -type port $impl/c_out_2[1]
remove_dont_match -type port $impl/c_out_2[0]
remove_dont_verify_points -type port $ref/c_out_1[3]
remove_dont_verify_points -type port $ref/c_out_1[2]
remove_dont_verify_points -type port $ref/c_out_1[1]
remove_dont_verify_points -type port $ref/c_out_1[0]
remove_dont_verify_points -type port $ref/c_out_2[3]
remove_dont_verify_points -type port $ref/c_out_2[2]
remove_dont_verify_points -type port $ref/c_out_2[1]
remove_dont_verify_points -type port $ref/c_out_2[0]
remove_dont_verify_points -type port $impl/c_out_1[3]
remove_dont_verify_points -type port $impl/c_out_1[2]
remove_dont_verify_points -type port $impl/c_out_1[1]
remove_dont_verify_points -type port $impl/c_out_1[0]
remove_dont_verify_points -type port $impl/c_out_2[3]
remove_dont_verify_points -type port $impl/c_out_2[2]
remove_dont_verify_points -type port $impl/c_out_2[1]
remove_dont_verify_points -type port $impl/c_out_2[0]
###
### Verifying instances:
### Ref: r:/WORK/TopModule/a3/c1
### Imp: i:/WORK/TopModule/a3/c1
###
set_reference_design r:/WORK/C_2
set_implementation_design i:/WORK/C_2
set_user_match -type port $impl/out[3] $ref/out[3]
set_user_match -type port $impl/out[2] $ref/out[2]
set_user_match -type port $impl/out[1] $ref/out[1]
set_user_match -type port $impl/out[0] $ref/out[0]
set_user_match -type port $impl/op_select $ref/op_select
set_user_match -type port $impl/input_a[3] $ref/input_a[3]
set_user_match -type port $impl/input_a[2] $ref/input_a[2]
set_user_match -type port $impl/input_a[1] $ref/input_a[1]
set_user_match -type port $impl/input_a[0] $ref/input_a[0]
set_user_match -type port $impl/input_b[3] $ref/input_b[3]
set_user_match -type port $impl/input_b[2] $ref/input_b[2]
set_user_match -type port $impl/input_b[1] $ref/input_b[1]
set_user_match -type port $impl/input_b[0] $ref/input_b[0]
set_user_match -type port $impl/clk $ref/clk
set_user_match -type port $impl/reset $ref/reset
set_constant -type port $ref/op_select 0
set_constant -type port $impl/op_select 0
set fm_begin_cputime [cputime]
verify
set fm_end_cputime [cputime]
set fm_this_verification_cputime [expr $fm_end_cputime - $fm_begin_cputime]
set fm_cumulative_memory [expr [memory] / 1000]
set fm_tmp_result_count [expr $fm_tmp_result_count + 1]
set fm_hier_result_array($fm_tmp_result_count) [list {r:/WORK/TopModule/a3/c1} {i:/WORK/TopModule/a3/c1} $verification_status]
set fm_failure_comment ""
if [expr (![string compare $verification_status "FAILED"])] {
set fm_failure_comment " (may be resolved in the parent level verification)"
}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " "}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format "Verification %s%s:" $verification_status $fm_failure_comment}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Ref: %s (instance of %s)" {r:/WORK/TopModule/a3/c1} $ref}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Imp: %s (instance of %s)" {i:/WORK/TopModule/a3/c1} $impl}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " %s, %4.0fMB (cumulative), %7.2fsec (incremental)" [date] $fm_cumulative_memory $fm_this_verification_cputime}
if [expr (![string compare $verification_status "INCONCLUSIVE"]) && \
($fm_session_files_saved < $fm_save_file_limit) && \
($fm_this_verification_cputime >= $fm_save_time_limit)] {
save_session -replace /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
lappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Session file: /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss"}
set fm_session_files_saved [expr $fm_session_files_saved + 1]
}
setup
remove_user_match -type port $impl/out[3]
remove_user_match -type port $impl/out[2]
remove_user_match -type port $impl/out[1]
remove_user_match -type port $impl/out[0]
remove_user_match -type port $impl/op_select
remove_user_match -type port $impl/input_a[3]
remove_user_match -type port $impl/input_a[2]
remove_user_match -type port $impl/input_a[1]
remove_user_match -type port $impl/input_a[0]
remove_user_match -type port $impl/input_b[3]
remove_user_match -type port $impl/input_b[2]
remove_user_match -type port $impl/input_b[1]
remove_user_match -type port $impl/input_b[0]
remove_user_match -type port $impl/clk
remove_user_match -type port $impl/reset
remove_constant -type port $ref/op_select
remove_constant -type port $impl/op_select
###
### Verifying instances:
### Ref: r:/WORK/TopModule/a3/c2
### Imp: i:/WORK/TopModule/a3/c2
###
set_reference_design r:/WORK/C_1
set_implementation_design i:/WORK/C_1
set_user_match -type port $impl/out[3] $ref/out[3]
set_user_match -type port $impl/out[2] $ref/out[2]
set_user_match -type port $impl/out[1] $ref/out[1]
set_user_match -type port $impl/out[0] $ref/out[0]
set_user_match -type port $impl/op_select $ref/op_select
set_user_match -type port $impl/input_a[3] $ref/input_a[3]
set_user_match -type port $impl/input_a[2] $ref/input_a[2]
set_user_match -type port $impl/input_a[1] $ref/input_a[1]
set_user_match -type port $impl/input_a[0] $ref/input_a[0]
set_user_match -type port $impl/input_b[3] $ref/input_b[3]
set_user_match -type port $impl/input_b[2] $ref/input_b[2]
set_user_match -type port $impl/input_b[1] $ref/input_b[1]
set_user_match -type port $impl/input_b[0] $ref/input_b[0]
set_user_match -type port $impl/clk $ref/clk
set_user_match -type port $impl/reset $ref/reset
set_constant -type port $ref/op_select 1
set_constant -type port $impl/op_select 1
set fm_begin_cputime [cputime]
verify
set fm_end_cputime [cputime]
set fm_this_verification_cputime [expr $fm_end_cputime - $fm_begin_cputime]
set fm_cumulative_memory [expr [memory] / 1000]
set fm_tmp_result_count [expr $fm_tmp_result_count + 1]
set fm_hier_result_array($fm_tmp_result_count) [list {r:/WORK/TopModule/a3/c2} {i:/WORK/TopModule/a3/c2} $verification_status]
set fm_failure_comment ""
if [expr (![string compare $verification_status "FAILED"])] {
set fm_failure_comment " (may be resolved in the parent level verification)"
}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " "}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format "Verification %s%s:" $verification_status $fm_failure_comment}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Ref: %s (instance of %s)" {r:/WORK/TopModule/a3/c2} $ref}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Imp: %s (instance of %s)" {i:/WORK/TopModule/a3/c2} $impl}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " %s, %4.0fMB (cumulative), %7.2fsec (incremental)" [date] $fm_cumulative_memory $fm_this_verification_cputime}
if [expr (![string compare $verification_status "INCONCLUSIVE"]) && \
($fm_session_files_saved < $fm_save_file_limit) && \
($fm_this_verification_cputime >= $fm_save_time_limit)] {
save_session -replace /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
lappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Session file: /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss"}
set fm_session_files_saved [expr $fm_session_files_saved + 1]
}
setup
remove_user_match -type port $impl/out[3]
remove_user_match -type port $impl/out[2]
remove_user_match -type port $impl/out[1]
remove_user_match -type port $impl/out[0]
remove_user_match -type port $impl/op_select
remove_user_match -type port $impl/input_a[3]
remove_user_match -type port $impl/input_a[2]
remove_user_match -type port $impl/input_a[1]
remove_user_match -type port $impl/input_a[0]
remove_user_match -type port $impl/input_b[3]
remove_user_match -type port $impl/input_b[2]
remove_user_match -type port $impl/input_b[1]
remove_user_match -type port $impl/input_b[0]
remove_user_match -type port $impl/clk
remove_user_match -type port $impl/reset
remove_constant -type port $ref/op_select
remove_constant -type port $impl/op_select
###
### Verifying instances:
### Ref: r:/WORK/TopModule/a3
### Imp: i:/WORK/TopModule/a3
###
set_reference_design r:/WORK/A_1
set_implementation_design i:/WORK/A_1
set at_least_one_black_box 0
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a3/c1} {i:/WORK/TopModule/a3/c1}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
set_black_box $ref/c1
set_black_box $impl/c1
set at_least_one_black_box 1
set_user_match -type cell $impl/c1 $ref/c1
set_user_match -type pin $impl/c1/out[3] $ref/c1/out[3]
set_user_match -type pin $impl/c1/out[2] $ref/c1/out[2]
set_user_match -type pin $impl/c1/out[1] $ref/c1/out[1]
set_user_match -type pin $impl/c1/out[0] $ref/c1/out[0]
set_user_match -type pin $impl/c1/op_select $ref/c1/op_select
set_user_match -type pin $impl/c1/input_a[3] $ref/c1/input_a[3]
set_user_match -type pin $impl/c1/input_a[2] $ref/c1/input_a[2]
set_user_match -type pin $impl/c1/input_a[1] $ref/c1/input_a[1]
set_user_match -type pin $impl/c1/input_a[0] $ref/c1/input_a[0]
set_user_match -type pin $impl/c1/input_b[3] $ref/c1/input_b[3]
set_user_match -type pin $impl/c1/input_b[2] $ref/c1/input_b[2]
set_user_match -type pin $impl/c1/input_b[1] $ref/c1/input_b[1]
set_user_match -type pin $impl/c1/input_b[0] $ref/c1/input_b[0]
set_user_match -type pin $impl/c1/clk $ref/c1/clk
set_user_match -type pin $impl/c1/reset $ref/c1/reset
}
if [expr true] {
}
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
# The following matched pin(s) are constant,
# therefore need not be verified at this level.
set_dont_verify_points -type pin $ref/c1/op_select
# The following matched pin(s) are constant,
# therefore need not be verified at this level.
set_dont_verify_points -type pin $impl/c1/op_select
}
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a3/c2} {i:/WORK/TopModule/a3/c2}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
set_black_box $ref/c2
set_black_box $impl/c2
set at_least_one_black_box 1
set_user_match -type cell $impl/c2 $ref/c2
set_user_match -type pin $impl/c2/out[3] $ref/c2/out[3]
set_user_match -type pin $impl/c2/out[2] $ref/c2/out[2]
set_user_match -type pin $impl/c2/out[1] $ref/c2/out[1]
set_user_match -type pin $impl/c2/out[0] $ref/c2/out[0]
set_user_match -type pin $impl/c2/op_select $ref/c2/op_select
set_user_match -type pin $impl/c2/input_a[3] $ref/c2/input_a[3]
set_user_match -type pin $impl/c2/input_a[2] $ref/c2/input_a[2]
set_user_match -type pin $impl/c2/input_a[1] $ref/c2/input_a[1]
set_user_match -type pin $impl/c2/input_a[0] $ref/c2/input_a[0]
set_user_match -type pin $impl/c2/input_b[3] $ref/c2/input_b[3]
set_user_match -type pin $impl/c2/input_b[2] $ref/c2/input_b[2]
set_user_match -type pin $impl/c2/input_b[1] $ref/c2/input_b[1]
set_user_match -type pin $impl/c2/input_b[0] $ref/c2/input_b[0]
set_user_match -type pin $impl/c2/clk $ref/c2/clk
set_user_match -type pin $impl/c2/reset $ref/c2/reset
}
if [expr true] {
}
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
# The following matched pin(s) are constant,
# therefore need not be verified at this level.
set_dont_verify_points -type pin $ref/c2/op_select
# The following matched pin(s) are constant,
# therefore need not be verified at this level.
set_dont_verify_points -type pin $impl/c2/op_select
}
set_user_match -type port $impl/out[3] $ref/out[3]
set_user_match -type port $impl/out[2] $ref/out[2]
set_user_match -type port $impl/out[1] $ref/out[1]
set_user_match -type port $impl/out[0] $ref/out[0]
set_user_match -type port $impl/input_a[3] $ref/input_a[3]
set_user_match -type port $impl/input_a[2] $ref/input_a[2]
set_user_match -type port $impl/input_a[1] $ref/input_a[1]
set_user_match -type port $impl/input_a[0] $ref/input_a[0]
set_user_match -type port $impl/input_b[3] $ref/input_b[3]
set_user_match -type port $impl/input_b[2] $ref/input_b[2]
set_user_match -type port $impl/input_b[1] $ref/input_b[1]
set_user_match -type port $impl/input_b[0] $ref/input_b[0]
set_user_match -type port $impl/clk $ref/clk
set_user_match -type port $impl/reset $ref/reset
set_dont_match -type port $ref/c_out_1[3]
set_dont_match -type port $ref/c_out_1[2]
set_dont_match -type port $ref/c_out_1[1]
set_dont_match -type port $ref/c_out_1[0]
set_dont_match -type port $ref/c_out_2[3]
set_dont_match -type port $ref/c_out_2[2]
set_dont_match -type port $ref/c_out_2[1]
set_dont_match -type port $ref/c_out_2[0]
set_dont_match -type port $impl/c_out_1[3]
set_dont_match -type port $impl/c_out_1[2]
set_dont_match -type port $impl/c_out_1[1]
set_dont_match -type port $impl/c_out_1[0]
set_dont_match -type port $impl/c_out_2[3]
set_dont_match -type port $impl/c_out_2[2]
set_dont_match -type port $impl/c_out_2[1]
set_dont_match -type port $impl/c_out_2[0]
# The following unmatched port(s) will cause verification failure at higher level if used there,
# therefore need not cause verification failure at this level.
set_dont_verify_points -type port $ref/c_out_1[3]
set_dont_verify_points -type port $ref/c_out_1[2]
set_dont_verify_points -type port $ref/c_out_1[1]
set_dont_verify_points -type port $ref/c_out_1[0]
set_dont_verify_points -type port $ref/c_out_2[3]
set_dont_verify_points -type port $ref/c_out_2[2]
set_dont_verify_points -type port $ref/c_out_2[1]
set_dont_verify_points -type port $ref/c_out_2[0]
# The following unmatched port(s) will cause verification failure at higher level if used there,
# therefore need not cause verification failure at this level.
set_dont_verify_points -type port $impl/c_out_1[3]
set_dont_verify_points -type port $impl/c_out_1[2]
set_dont_verify_points -type port $impl/c_out_1[1]
set_dont_verify_points -type port $impl/c_out_1[0]
set_dont_verify_points -type port $impl/c_out_2[3]
set_dont_verify_points -type port $impl/c_out_2[2]
set_dont_verify_points -type port $impl/c_out_2[1]
set_dont_verify_points -type port $impl/c_out_2[0]
set fm_begin_cputime [cputime]
verify
if [expr ($at_least_one_black_box) && \
(![string compare $verification_status "FAILED"])] {
setup
set at_least_one_black_box 0
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a3/c1} {i:/WORK/TopModule/a3/c1}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/c1
remove_black_box $impl/c1
remove_user_match -type cell $impl/c1
remove_user_match -type pin $impl/c1/out[3]
remove_user_match -type pin $impl/c1/out[2]
remove_user_match -type pin $impl/c1/out[1]
remove_user_match -type pin $impl/c1/out[0]
remove_user_match -type pin $impl/c1/op_select
remove_user_match -type pin $impl/c1/input_a[3]
remove_user_match -type pin $impl/c1/input_a[2]
remove_user_match -type pin $impl/c1/input_a[1]
remove_user_match -type pin $impl/c1/input_a[0]
remove_user_match -type pin $impl/c1/input_b[3]
remove_user_match -type pin $impl/c1/input_b[2]
remove_user_match -type pin $impl/c1/input_b[1]
remove_user_match -type pin $impl/c1/input_b[0]
remove_user_match -type pin $impl/c1/clk
remove_user_match -type pin $impl/c1/reset
remove_dont_verify_points -type pin $ref/c1/op_select
remove_dont_verify_points -type pin $impl/c1/op_select
}
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a3/c2} {i:/WORK/TopModule/a3/c2}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/c2
remove_black_box $impl/c2
remove_user_match -type cell $impl/c2
remove_user_match -type pin $impl/c2/out[3]
remove_user_match -type pin $impl/c2/out[2]
remove_user_match -type pin $impl/c2/out[1]
remove_user_match -type pin $impl/c2/out[0]
remove_user_match -type pin $impl/c2/op_select
remove_user_match -type pin $impl/c2/input_a[3]
remove_user_match -type pin $impl/c2/input_a[2]
remove_user_match -type pin $impl/c2/input_a[1]
remove_user_match -type pin $impl/c2/input_a[0]
remove_user_match -type pin $impl/c2/input_b[3]
remove_user_match -type pin $impl/c2/input_b[2]
remove_user_match -type pin $impl/c2/input_b[1]
remove_user_match -type pin $impl/c2/input_b[0]
remove_user_match -type pin $impl/c2/clk
remove_user_match -type pin $impl/c2/reset
remove_dont_verify_points -type pin $ref/c2/op_select
remove_dont_verify_points -type pin $impl/c2/op_select
}
verify
}
set fm_end_cputime [cputime]
set fm_this_verification_cputime [expr $fm_end_cputime - $fm_begin_cputime]
set fm_cumulative_memory [expr [memory] / 1000]
set fm_tmp_result_count [expr $fm_tmp_result_count + 1]
set fm_hier_result_array($fm_tmp_result_count) [list {r:/WORK/TopModule/a3} {i:/WORK/TopModule/a3} $verification_status]
set fm_failure_comment ""
if [expr (![string compare $verification_status "FAILED"])] {
set fm_failure_comment " (may be resolved in the parent level verification)"
}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " "}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format "Verification %s%s:" $verification_status $fm_failure_comment}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Ref: %s (instance of %s)" {r:/WORK/TopModule/a3} $ref}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Imp: %s (instance of %s)" {i:/WORK/TopModule/a3} $impl}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " %s, %4.0fMB (cumulative), %7.2fsec (incremental)" [date] $fm_cumulative_memory $fm_this_verification_cputime}
if [expr (![string compare $verification_status "INCONCLUSIVE"]) && \
($fm_session_files_saved < $fm_save_file_limit) && \
($fm_this_verification_cputime >= $fm_save_time_limit)] {
save_session -replace /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
lappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Session file: /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss"}
set fm_session_files_saved [expr $fm_session_files_saved + 1]
}
setup
if [expr ($at_least_one_black_box)] {
set at_least_one_black_box 0
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a3/c1} {i:/WORK/TopModule/a3/c1}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/c1
remove_black_box $impl/c1
remove_user_match -type cell $impl/c1
remove_user_match -type pin $impl/c1/out[3]
remove_user_match -type pin $impl/c1/out[2]
remove_user_match -type pin $impl/c1/out[1]
remove_user_match -type pin $impl/c1/out[0]
remove_user_match -type pin $impl/c1/op_select
remove_user_match -type pin $impl/c1/input_a[3]
remove_user_match -type pin $impl/c1/input_a[2]
remove_user_match -type pin $impl/c1/input_a[1]
remove_user_match -type pin $impl/c1/input_a[0]
remove_user_match -type pin $impl/c1/input_b[3]
remove_user_match -type pin $impl/c1/input_b[2]
remove_user_match -type pin $impl/c1/input_b[1]
remove_user_match -type pin $impl/c1/input_b[0]
remove_user_match -type pin $impl/c1/clk
remove_user_match -type pin $impl/c1/reset
remove_dont_verify_points -type pin $ref/c1/op_select
remove_dont_verify_points -type pin $impl/c1/op_select
}
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a3/c2} {i:/WORK/TopModule/a3/c2}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/c2
remove_black_box $impl/c2
remove_user_match -type cell $impl/c2
remove_user_match -type pin $impl/c2/out[3]
remove_user_match -type pin $impl/c2/out[2]
remove_user_match -type pin $impl/c2/out[1]
remove_user_match -type pin $impl/c2/out[0]
remove_user_match -type pin $impl/c2/op_select
remove_user_match -type pin $impl/c2/input_a[3]
remove_user_match -type pin $impl/c2/input_a[2]
remove_user_match -type pin $impl/c2/input_a[1]
remove_user_match -type pin $impl/c2/input_a[0]
remove_user_match -type pin $impl/c2/input_b[3]
remove_user_match -type pin $impl/c2/input_b[2]
remove_user_match -type pin $impl/c2/input_b[1]
remove_user_match -type pin $impl/c2/input_b[0]
remove_user_match -type pin $impl/c2/clk
remove_user_match -type pin $impl/c2/reset
remove_dont_verify_points -type pin $ref/c2/op_select
remove_dont_verify_points -type pin $impl/c2/op_select
}
}
remove_user_match -type port $impl/out[3]
remove_user_match -type port $impl/out[2]
remove_user_match -type port $impl/out[1]
remove_user_match -type port $impl/out[0]
remove_user_match -type port $impl/input_a[3]
remove_user_match -type port $impl/input_a[2]
remove_user_match -type port $impl/input_a[1]
remove_user_match -type port $impl/input_a[0]
remove_user_match -type port $impl/input_b[3]
remove_user_match -type port $impl/input_b[2]
remove_user_match -type port $impl/input_b[1]
remove_user_match -type port $impl/input_b[0]
remove_user_match -type port $impl/clk
remove_user_match -type port $impl/reset
remove_dont_match -type port $ref/c_out_1[3]
remove_dont_match -type port $ref/c_out_1[2]
remove_dont_match -type port $ref/c_out_1[1]
remove_dont_match -type port $ref/c_out_1[0]
remove_dont_match -type port $ref/c_out_2[3]
remove_dont_match -type port $ref/c_out_2[2]
remove_dont_match -type port $ref/c_out_2[1]
remove_dont_match -type port $ref/c_out_2[0]
remove_dont_match -type port $impl/c_out_1[3]
remove_dont_match -type port $impl/c_out_1[2]
remove_dont_match -type port $impl/c_out_1[1]
remove_dont_match -type port $impl/c_out_1[0]
remove_dont_match -type port $impl/c_out_2[3]
remove_dont_match -type port $impl/c_out_2[2]
remove_dont_match -type port $impl/c_out_2[1]
remove_dont_match -type port $impl/c_out_2[0]
remove_dont_verify_points -type port $ref/c_out_1[3]
remove_dont_verify_points -type port $ref/c_out_1[2]
remove_dont_verify_points -type port $ref/c_out_1[1]
remove_dont_verify_points -type port $ref/c_out_1[0]
remove_dont_verify_points -type port $ref/c_out_2[3]
remove_dont_verify_points -type port $ref/c_out_2[2]
remove_dont_verify_points -type port $ref/c_out_2[1]
remove_dont_verify_points -type port $ref/c_out_2[0]
remove_dont_verify_points -type port $impl/c_out_1[3]
remove_dont_verify_points -type port $impl/c_out_1[2]
remove_dont_verify_points -type port $impl/c_out_1[1]
remove_dont_verify_points -type port $impl/c_out_1[0]
remove_dont_verify_points -type port $impl/c_out_2[3]
remove_dont_verify_points -type port $impl/c_out_2[2]
remove_dont_verify_points -type port $impl/c_out_2[1]
remove_dont_verify_points -type port $impl/c_out_2[0]
###
### Verifying instances:
### Ref: r:/WORK/TopModule
### Imp: i:/WORK/TopModule
###
set_reference_design r:/WORK/TopModule
set_implementation_design i:/WORK/TopModule
set at_least_one_black_box 0
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a1} {i:/WORK/TopModule/a1}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
set_black_box $ref/a1
set_black_box $impl/a1
set at_least_one_black_box 1
set_user_match -type cell $impl/a1 $ref/a1
set_user_match -type pin $impl/a1/out[3] $ref/a1/out[3]
set_user_match -type pin $impl/a1/out[2] $ref/a1/out[2]
set_user_match -type pin $impl/a1/out[1] $ref/a1/out[1]
set_user_match -type pin $impl/a1/out[0] $ref/a1/out[0]
set_user_match -type pin $impl/a1/input_a[3] $ref/a1/input_a[3]
set_user_match -type pin $impl/a1/input_a[2] $ref/a1/input_a[2]
set_user_match -type pin $impl/a1/input_a[1] $ref/a1/input_a[1]
set_user_match -type pin $impl/a1/input_a[0] $ref/a1/input_a[0]
set_user_match -type pin $impl/a1/input_b[3] $ref/a1/input_b[3]
set_user_match -type pin $impl/a1/input_b[2] $ref/a1/input_b[2]
set_user_match -type pin $impl/a1/input_b[1] $ref/a1/input_b[1]
set_user_match -type pin $impl/a1/input_b[0] $ref/a1/input_b[0]
set_user_match -type pin $impl/a1/clk $ref/a1/clk
set_user_match -type pin $impl/a1/reset $ref/a1/reset
}
if [expr true] {
}
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
}
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a2} {i:/WORK/TopModule/a2}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
set_black_box $ref/a2
set_black_box $impl/a2
set at_least_one_black_box 1
set_user_match -type cell $impl/a2 $ref/a2
set_user_match -type pin $impl/a2/out[3] $ref/a2/out[3]
set_user_match -type pin $impl/a2/out[2] $ref/a2/out[2]
set_user_match -type pin $impl/a2/out[1] $ref/a2/out[1]
set_user_match -type pin $impl/a2/out[0] $ref/a2/out[0]
set_user_match -type pin $impl/a2/input_a[3] $ref/a2/input_a[3]
set_user_match -type pin $impl/a2/input_a[2] $ref/a2/input_a[2]
set_user_match -type pin $impl/a2/input_a[1] $ref/a2/input_a[1]
set_user_match -type pin $impl/a2/input_a[0] $ref/a2/input_a[0]
set_user_match -type pin $impl/a2/input_b[3] $ref/a2/input_b[3]
set_user_match -type pin $impl/a2/input_b[2] $ref/a2/input_b[2]
set_user_match -type pin $impl/a2/input_b[1] $ref/a2/input_b[1]
set_user_match -type pin $impl/a2/input_b[0] $ref/a2/input_b[0]
set_user_match -type pin $impl/a2/clk $ref/a2/clk
set_user_match -type pin $impl/a2/reset $ref/a2/reset
}
if [expr true] {
}
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
}
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a3} {i:/WORK/TopModule/a3}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
set_black_box $ref/a3
set_black_box $impl/a3
set at_least_one_black_box 1
set_user_match -type cell $impl/a3 $ref/a3
set_user_match -type pin $impl/a3/out[3] $ref/a3/out[3]
set_user_match -type pin $impl/a3/out[2] $ref/a3/out[2]
set_user_match -type pin $impl/a3/out[1] $ref/a3/out[1]
set_user_match -type pin $impl/a3/out[0] $ref/a3/out[0]
set_user_match -type pin $impl/a3/input_a[3] $ref/a3/input_a[3]
set_user_match -type pin $impl/a3/input_a[2] $ref/a3/input_a[2]
set_user_match -type pin $impl/a3/input_a[1] $ref/a3/input_a[1]
set_user_match -type pin $impl/a3/input_a[0] $ref/a3/input_a[0]
set_user_match -type pin $impl/a3/input_b[3] $ref/a3/input_b[3]
set_user_match -type pin $impl/a3/input_b[2] $ref/a3/input_b[2]
set_user_match -type pin $impl/a3/input_b[1] $ref/a3/input_b[1]
set_user_match -type pin $impl/a3/input_b[0] $ref/a3/input_b[0]
set_user_match -type pin $impl/a3/clk $ref/a3/clk
set_user_match -type pin $impl/a3/reset $ref/a3/reset
}
if [expr true] {
}
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
}
set fm_begin_cputime [cputime]
verify
if [expr ($at_least_one_black_box) && \
(![string compare $verification_status "FAILED"])] {
setup
set at_least_one_black_box 0
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a1} {i:/WORK/TopModule/a1}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/a1
remove_black_box $impl/a1
remove_user_match -type cell $impl/a1
remove_user_match -type pin $impl/a1/out[3]
remove_user_match -type pin $impl/a1/out[2]
remove_user_match -type pin $impl/a1/out[1]
remove_user_match -type pin $impl/a1/out[0]
remove_user_match -type pin $impl/a1/input_a[3]
remove_user_match -type pin $impl/a1/input_a[2]
remove_user_match -type pin $impl/a1/input_a[1]
remove_user_match -type pin $impl/a1/input_a[0]
remove_user_match -type pin $impl/a1/input_b[3]
remove_user_match -type pin $impl/a1/input_b[2]
remove_user_match -type pin $impl/a1/input_b[1]
remove_user_match -type pin $impl/a1/input_b[0]
remove_user_match -type pin $impl/a1/clk
remove_user_match -type pin $impl/a1/reset
}
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a2} {i:/WORK/TopModule/a2}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/a2
remove_black_box $impl/a2
remove_user_match -type cell $impl/a2
remove_user_match -type pin $impl/a2/out[3]
remove_user_match -type pin $impl/a2/out[2]
remove_user_match -type pin $impl/a2/out[1]
remove_user_match -type pin $impl/a2/out[0]
remove_user_match -type pin $impl/a2/input_a[3]
remove_user_match -type pin $impl/a2/input_a[2]
remove_user_match -type pin $impl/a2/input_a[1]
remove_user_match -type pin $impl/a2/input_a[0]
remove_user_match -type pin $impl/a2/input_b[3]
remove_user_match -type pin $impl/a2/input_b[2]
remove_user_match -type pin $impl/a2/input_b[1]
remove_user_match -type pin $impl/a2/input_b[0]
remove_user_match -type pin $impl/a2/clk
remove_user_match -type pin $impl/a2/reset
}
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a3} {i:/WORK/TopModule/a3}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/a3
remove_black_box $impl/a3
remove_user_match -type cell $impl/a3
remove_user_match -type pin $impl/a3/out[3]
remove_user_match -type pin $impl/a3/out[2]
remove_user_match -type pin $impl/a3/out[1]
remove_user_match -type pin $impl/a3/out[0]
remove_user_match -type pin $impl/a3/input_a[3]
remove_user_match -type pin $impl/a3/input_a[2]
remove_user_match -type pin $impl/a3/input_a[1]
remove_user_match -type pin $impl/a3/input_a[0]
remove_user_match -type pin $impl/a3/input_b[3]
remove_user_match -type pin $impl/a3/input_b[2]
remove_user_match -type pin $impl/a3/input_b[1]
remove_user_match -type pin $impl/a3/input_b[0]
remove_user_match -type pin $impl/a3/clk
remove_user_match -type pin $impl/a3/reset
}
verify
}
set fm_end_cputime [cputime]
set fm_this_verification_cputime [expr $fm_end_cputime - $fm_begin_cputime]
set fm_cumulative_memory [expr [memory] / 1000]
set fm_tmp_result_count [expr $fm_tmp_result_count + 1]
set fm_hier_result_array($fm_tmp_result_count) [list {r:/WORK/TopModule} {i:/WORK/TopModule} $verification_status]
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " "}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format "Verification %s:" $verification_status}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Ref: %s (top)" {r:/WORK/TopModule}}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Imp: %s (top)" {i:/WORK/TopModule}}
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " %s, %4.0fMB (cumulative), %7.2fsec (incremental)" [date] $fm_cumulative_memory $fm_this_verification_cputime}
if [expr (![string compare $verification_status "INCONCLUSIVE"]) && \
($fm_session_files_saved < $fm_save_file_limit) && \
($fm_this_verification_cputime >= $fm_save_time_limit)] {
save_session -replace /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
lappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss
redirect -append /home/zhangchen/Desktop/test1/fm_hier.log {format " Session file: /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fss"}
set fm_session_files_saved [expr $fm_session_files_saved + 1]
}
setup
if [expr ($at_least_one_black_box)] {
set at_least_one_black_box 0
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a1} {i:/WORK/TopModule/a1}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/a1
remove_black_box $impl/a1
remove_user_match -type cell $impl/a1
remove_user_match -type pin $impl/a1/out[3]
remove_user_match -type pin $impl/a1/out[2]
remove_user_match -type pin $impl/a1/out[1]
remove_user_match -type pin $impl/a1/out[0]
remove_user_match -type pin $impl/a1/input_a[3]
remove_user_match -type pin $impl/a1/input_a[2]
remove_user_match -type pin $impl/a1/input_a[1]
remove_user_match -type pin $impl/a1/input_a[0]
remove_user_match -type pin $impl/a1/input_b[3]
remove_user_match -type pin $impl/a1/input_b[2]
remove_user_match -type pin $impl/a1/input_b[1]
remove_user_match -type pin $impl/a1/input_b[0]
remove_user_match -type pin $impl/a1/clk
remove_user_match -type pin $impl/a1/reset
}
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a2} {i:/WORK/TopModule/a2}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/a2
remove_black_box $impl/a2
remove_user_match -type cell $impl/a2
remove_user_match -type pin $impl/a2/out[3]
remove_user_match -type pin $impl/a2/out[2]
remove_user_match -type pin $impl/a2/out[1]
remove_user_match -type pin $impl/a2/out[0]
remove_user_match -type pin $impl/a2/input_a[3]
remove_user_match -type pin $impl/a2/input_a[2]
remove_user_match -type pin $impl/a2/input_a[1]
remove_user_match -type pin $impl/a2/input_a[0]
remove_user_match -type pin $impl/a2/input_b[3]
remove_user_match -type pin $impl/a2/input_b[2]
remove_user_match -type pin $impl/a2/input_b[1]
remove_user_match -type pin $impl/a2/input_b[0]
remove_user_match -type pin $impl/a2/clk
remove_user_match -type pin $impl/a2/reset
}
set tmp_verification_status [get_verification_status {r:/WORK/TopModule/a3} {i:/WORK/TopModule/a3}]
if [expr ((![string compare $tmp_verification_status "SUCCEEDED"]) || \
(![string compare $tmp_verification_status "INCONCLUSIVE"]))] {
remove_black_box $ref/a3
remove_black_box $impl/a3
remove_user_match -type cell $impl/a3
remove_user_match -type pin $impl/a3/out[3]
remove_user_match -type pin $impl/a3/out[2]
remove_user_match -type pin $impl/a3/out[1]
remove_user_match -type pin $impl/a3/out[0]
remove_user_match -type pin $impl/a3/input_a[3]
remove_user_match -type pin $impl/a3/input_a[2]
remove_user_match -type pin $impl/a3/input_a[1]
remove_user_match -type pin $impl/a3/input_a[0]
remove_user_match -type pin $impl/a3/input_b[3]
remove_user_match -type pin $impl/a3/input_b[2]
remove_user_match -type pin $impl/a3/input_b[1]
remove_user_match -type pin $impl/a3/input_b[0]
remove_user_match -type pin $impl/a3/clk
remove_user_match -type pin $impl/a3/reset
}
}
if [info exists fm_write_hier_saved_vars] {
foreach _var [array names fm_write_hier_saved_vars] {
set $_var $fm_write_hier_saved_vars($_var)
};
unset fm_write_hier_saved_vars
}
###
### Report results
###
set fm_hier_result_count $fm_tmp_result_count
set fm_log_fp [open /home/zhangchen/Desktop/test1/fm_hier.log]
puts [read $fm_log_fp]
close $fm_log_fp
![[BrainShadow-V1] VR头戴设备统计报告](https://i-blog.csdnimg.cn/direct/eeab3db06983452f88779fcb6e9f3da1.png)
