网站联系方式要素,做网站要固定ip,大气预警在建设局网站,北京开发小程序相关阅读
Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm1001.2014.3001.5482 Formality存在两个重要的概念#xff1a;参考设计/实现设计和顶层设计#xff0c;本文就将对此进行详细阐述。参考设计/实现设计是中两个重要的全局概念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
