相關閱讀
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_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
