Formality：参考设计/实现设计以及顶层设计

相关阅读

Formalityhttps://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_arrayredirect         /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 "**************************************************************************************************"}setupif [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 noneif [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 falseif [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 falseif [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 falseif [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 falseif [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 0proc get_verification_status {ref_inst imp_inst} {global fm_tmp_result_countglobal fm_hier_result_arrayfor {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.fsslappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fssredirect -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.fsslappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fssredirect -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/c1set_black_box $impl/c1set at_least_one_black_box 1set_user_match -type cell $impl/c1 $ref/c1set_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_selectset_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/clkset_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/c2set_black_box $impl/c2set at_least_one_black_box 1set_user_match -type cell $impl/c2 $ref/c2set_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_selectset_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/clkset_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"])] {setupset at_least_one_black_box 0set 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/c1remove_black_box $impl/c1remove_user_match -type cell $impl/c1remove_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_selectremove_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/clkremove_user_match -type pin $impl/c1/resetremove_dont_verify_points -type pin  $ref/c1/op_selectremove_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/c2remove_black_box $impl/c2remove_user_match -type cell $impl/c2remove_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_selectremove_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/clkremove_user_match -type pin $impl/c2/resetremove_dont_verify_points -type pin  $ref/c2/op_selectremove_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.fsslappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fssredirect -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 0set 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/c1remove_black_box $impl/c1remove_user_match -type cell $impl/c1remove_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_selectremove_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/clkremove_user_match -type pin $impl/c1/resetremove_dont_verify_points -type pin  $ref/c1/op_selectremove_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/c2remove_black_box $impl/c2remove_user_match -type cell $impl/c2remove_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_selectremove_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/clkremove_user_match -type pin $impl/c2/resetremove_dont_verify_points -type pin  $ref/c2/op_selectremove_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.fsslappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fssredirect -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.fsslappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fssredirect -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/c1set_black_box $impl/c1set at_least_one_black_box 1set_user_match -type cell $impl/c1 $ref/c1set_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_selectset_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/clkset_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/c2set_black_box $impl/c2set at_least_one_black_box 1set_user_match -type cell $impl/c2 $ref/c2set_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_selectset_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/clkset_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"])] {setupset at_least_one_black_box 0set 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/c1remove_black_box $impl/c1remove_user_match -type cell $impl/c1remove_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_selectremove_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/clkremove_user_match -type pin $impl/c1/resetremove_dont_verify_points -type pin  $ref/c1/op_selectremove_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/c2remove_black_box $impl/c2remove_user_match -type cell $impl/c2remove_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_selectremove_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/clkremove_user_match -type pin $impl/c2/resetremove_dont_verify_points -type pin  $ref/c2/op_selectremove_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.fsslappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fssredirect -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 0set 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/c1remove_black_box $impl/c1remove_user_match -type cell $impl/c1remove_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_selectremove_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/clkremove_user_match -type pin $impl/c1/resetremove_dont_verify_points -type pin  $ref/c1/op_selectremove_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/c2remove_black_box $impl/c2remove_user_match -type cell $impl/c2remove_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_selectremove_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/clkremove_user_match -type pin $impl/c2/resetremove_dont_verify_points -type pin  $ref/c2/op_selectremove_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.fsslappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fssredirect -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.fsslappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fssredirect -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/c1set_black_box $impl/c1set at_least_one_black_box 1set_user_match -type cell $impl/c1 $ref/c1set_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_selectset_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/clkset_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/c2set_black_box $impl/c2set at_least_one_black_box 1set_user_match -type cell $impl/c2 $ref/c2set_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_selectset_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/clkset_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"])] {setupset at_least_one_black_box 0set 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/c1remove_black_box $impl/c1remove_user_match -type cell $impl/c1remove_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_selectremove_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/clkremove_user_match -type pin $impl/c1/resetremove_dont_verify_points -type pin  $ref/c1/op_selectremove_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/c2remove_black_box $impl/c2remove_user_match -type cell $impl/c2remove_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_selectremove_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/clkremove_user_match -type pin $impl/c2/resetremove_dont_verify_points -type pin  $ref/c2/op_selectremove_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.fsslappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fssredirect -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 0set 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/c1remove_black_box $impl/c1remove_user_match -type cell $impl/c1remove_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_selectremove_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/clkremove_user_match -type pin $impl/c1/resetremove_dont_verify_points -type pin  $ref/c1/op_selectremove_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/c2remove_black_box $impl/c2remove_user_match -type cell $impl/c2remove_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_selectremove_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/clkremove_user_match -type pin $impl/c2/resetremove_dont_verify_points -type pin  $ref/c2/op_selectremove_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/a1set_black_box $impl/a1set at_least_one_black_box 1set_user_match -type cell $impl/a1 $ref/a1set_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/clkset_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/a2set_black_box $impl/a2set at_least_one_black_box 1set_user_match -type cell $impl/a2 $ref/a2set_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/clkset_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/a3set_black_box $impl/a3set at_least_one_black_box 1set_user_match -type cell $impl/a3 $ref/a3set_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/clkset_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"])] {setupset at_least_one_black_box 0set 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/a1remove_black_box $impl/a1remove_user_match -type cell $impl/a1remove_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/clkremove_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/a2remove_black_box $impl/a2remove_user_match -type cell $impl/a2remove_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/clkremove_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/a3remove_black_box $impl/a3remove_user_match -type cell $impl/a3remove_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/clkremove_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.fsslappend fm_hier_result_array($fm_tmp_result_count) /home/zhangchen/Desktop/test1/fm_hier.tcl.$fm_tmp_result_count.fssredirect -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 0set 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/a1remove_black_box $impl/a1remove_user_match -type cell $impl/a1remove_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/clkremove_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/a2remove_black_box $impl/a2remove_user_match -type cell $impl/a2remove_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/clkremove_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/a3remove_black_box $impl/a3remove_user_match -type cell $impl/a3remove_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/clkremove_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