相关阅读Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm1001.2014.3001.5482在进行RTL2Gate或Gate2Gate等价性检查时最常见的挑战之一是设计规模过大带来的验证复杂度问题。对于包含大量层级、重复实例以及复杂子模块的SoC设计如果采用展平验证(Flat Verification)工具需要在同一层级展开所有逻辑进行整体比对这不仅会显著增加匹配与证明的计算开销还容易因为局部约束不完整或上下文丢失而产生假失败(False Failure)尽管在进行展平验证时Formality也会在用户不感知的情况下对层次单元的引脚进行匹配并将它们作为潜在比较点验证过程中可能提示Status: Matching hierarchy...但这是隐式和不可见的使用set_parameters -flatten命令可以强制拒绝层次单元的引脚匹配如果设计中有大量的边界优化(Boundary Optimization)则可以使用该命令改善验证时间否则会导致验证运行时间变长。为了解决这一问题Formality提供了层次化验证(Hierarchical Verification)机制。其核心思想是将整体设计按照层级结构拆分为多个可独立验证的Block并以“逐层向上”的方式完成等价性证明。具体来说验证过程从设计的最底层Block开始对每一个可匹配的子Block进行独立验证在该Block验证完成后将其设置为黑盒(Black Box)从而在上层验证中不再考虑其内部逻辑。随后上层Block在这些已验证Block的基础上继续进行等价性检查如此逐级向上推进直到完成顶层验证。这种方法的优势在于每个Block都是在相对隔离且受控的上下文中验证的既降低了匹配空间也减少了由于层次耦合导致的误判。同时通过Block级端口约束的精确建模可以进一步减少边界条件错误使验证结果更加稳定可靠。 这种方法的缺点在于层次化验证不适合存在大量边界优化的设计不过对于目前常见的层次化综合设计流程来说一般会限制Block的边界优化。在Formailty中这一层次化验证流程通常不是手工逐个执行的而是通过自动生成Tcl脚本来完成。工具会根据当前参考设计(Reference Design)与实现设计(Implementation Design)的匹配关系自动生成一套完整的层次化验证脚本用于控制黑盒设置、端口匹配、约束传递以及会话保存等行为。可以通过以下两种方式生成脚本需要注意的是脚本需要在完成SVF文件读取和设计读取后才可生成或运行。fm_shellGUI使用write_hierarchical_verification_script命令选项包括[-replace][-noconstant][-noequivalence][-match type][-save_mode mode][-save_directory pathname][-save_file_limit integer][-save_time_limit integer][-level integer][-path instance-specific-pathname(s)][-block instance-specific-pathname(s)][-dont_resolve_failures][-top_level_only]filename1、选择File Write Hierarchical Script。2、设置需要隔离的Block层次(Levels)。3、设置偏好(Setup Preferences)。4、设置匹配类型(Matching)。5、设置文件输出(FIle Output)包含会话保存方式、会话保存位置、会话保存数量、会话超时保存、脚本保存位置。下面对各个选项进行说明。-replace-replace选项用于指定是否覆盖已有脚本文件。默认情况下如果文件已存在则会报错。-noconstant-noconstant选项用于指定是否在子Block边界生成常量约束。默认情况下脚本会自动提取输入端口常量约束(set_constant命令)用于增强匹配稳定性。-noequivalence-noequivalence选项用于指定是否在子Block边界生成等价约束。默认情况下脚本会对那些已知等价但未匹配的端口生成等价约束set_constraint coupled命令。-match-match选项用于指定匹配信息的生成范围。如果为auto默认即仅对非基于名称的匹配的对象生成匹配信息、为all即对所有对象生成完整匹配信息。关于匹配的更详细内容可以参考下面的博客。Formality匹配(match)是如何进行的https://blog.csdn.net/weixin_45791458/article/details/144404964?ops_request_miscelastic_search_miscrequest_id5fa0541072fe8dac30639b0c9b14bc62biz_id0utm_mediumdistribute.pc_search_result.none-task-blog-2~all~ElasticSearch~search_v2-1-144404964-null-null.nonecaseutm_term%E5%8C%B9%E9%85%8Dspm1018.2226.3001.4450-save_mode-save_mode选项用于指定在哪些验证结果下保存会话。如果为auto默认仅保存不确定(inconclusive)结果若开启Failure Resolve则同时保存失败结果、为not_passed即保存所有未通过验证结果、为failed仅保存失败(Failed)结果、为inconclusive仅保存不确定结果。-save_directory-save_directory选项用于指定会话文件保存路径默认是当前工作目录。-save_file_limit-save_file_limit选项用于指定最多保存的会话文件数量默认值为1。-save_time_limit-save_time_limit选项用于指定控制会话保存的CPU时间阈值默认值为0。只有大于阈值的会话能被保存。-level-level选项用于指定层次仅对指定层次及以上Block进行黑盒化和独立验证顶层模块的层次为0。例如对于以下的设计结构如果指定-level选项为1则首先验证top_block/u1和top_block/u2随后在top_block将这二者设置为黑盒后进行顶层验证如果指定-level选项为2则首先验证top_block/u1/u1_sub和top_block/u2/u2_sub随后自底而上进行层次验证。top_block (level 0) ├── u1 (level 1) │ └── u1_sub (level 2) └── u2 (level 1) └── u2_sub (level 2)-path-path选项用于指定沿着具体路径开始进行黑盒化和独立验证。例如对于以下的设计结构如果指定-path选项为top_block/u1则首先验证top_block/u1随后在top_block将这top_block/u1设置为黑盒后进行顶层验证如果指定-path选项为top_block/u1/u1_sub则首先验证top_block/u1/u1_sub随后在top_block/u1将top_block/u1/u1_sub设置为黑盒后进行验证最后在top_block将top_block/u1为黑盒后进行顶层验证。top_block (level 0) ├── u1 (level 1) │ └── u1_sub (level 2) └── u2 (level 1) └── u2_sub (level 2)-block-block选项用于指定仅对具体Block进行黑盒化和独立验证。例如对于以下的设计结构如果指定-block选项为top_block/u1则首先验证top_block/u1随后在top_block将这top_block/u1设置为黑盒后进行顶层验证如果指定-block选项为top_block/u1/u1_sub和top_block/u2/u2_sub则首先验证top_block/u1/u1_sub和top_block/u2/u2_sub随后直接在top_block将这二者设置为黑盒后进行顶层验证。top_block (level 0) ├── u1 (level 1) │ └── u1_sub (level 2) └── u2 (level 1) └── u2_sub (level 2)-dont_resolve_failures-dont_resolve_failures选项用于指定是否开启重新验证。默认情况下当上层Block验证失败时会尝试将下层Block的黑盒移除重新进行验证。-top_level_only-top_level_only选项用于指定只将顶层Block下的子Block设置为黑盒后进行顶层验证。如与-block选项一起使用则将指定Block设置为黑盒后将直接进行顶层验证而不会验证指定Block如与-path选项一起使用则将指定路径下属于顶层Block下的子Block设置为黑盒后进行顶层验证。下面展示了一个write_hierarchical_verification_script命令输出的层次化验证脚本。### ### Formality (R) hierarchical verification script: hier.tcl ### ### Reference design: r:/WORK/top_block ### Implementation design: i:/WORK/top_block ### Generated Sat Jun 13 22:40:43 2026 ### global ref global impl global verification_constant_prop_mode global signature_analysis_match_blackbox_input global signature_analysis_match_blackbox_output global signature_analysis_match_primary_input global signature_analysis_match_primary_output global verification_status global fm_tmp_result_count global fm_hier_result_array redirect ./sess_fail/fm_hier.log {echo **************************************************************************************************} redirect -append ./sess_fail/fm_hier.log {echo Results of hierarchical verification script: hier.tcl} redirect -append ./sess_fail/fm_hier.log {echo **************************************************************************************************} setup if [info exists verification_constant_prop_mode] { set fm_write_hier_saved_vars(verification_constant_prop_mode) $verification_constant_prop_mode } set verification_constant_prop_mode none if [info exists signature_analysis_match_blackbox_input] { set fm_write_hier_saved_vars(signature_analysis_match_blackbox_input) $signature_analysis_match_blackbox_input } set signature_analysis_match_blackbox_input false if [info exists signature_analysis_match_blackbox_output] { set fm_write_hier_saved_vars(signature_analysis_match_blackbox_output) $signature_analysis_match_blackbox_output } set signature_analysis_match_blackbox_output false if [info exists signature_analysis_match_primary_input] { set fm_write_hier_saved_vars(signature_analysis_match_primary_input) $signature_analysis_match_primary_input } set signature_analysis_match_primary_input false if [info exists signature_analysis_match_primary_output] { set fm_write_hier_saved_vars(signature_analysis_match_primary_output) $signature_analysis_match_primary_output } set signature_analysis_match_primary_output false if [info exists fm_hier_result_array] { unset fm_hier_result_array } set fm_hier_result_count 0 set fm_tmp_result_count 0 set fm_session_files_saved 0 set fm_save_file_limit 1 set fm_save_time_limit 0 proc get_verification_status {ref_inst imp_inst} { global fm_tmp_result_count global fm_hier_result_array for {set i 0} {$i $fm_tmp_result_count} {incr i} { if [expr (![string compare [lindex $fm_hier_result_array([expr $i 1]) 0] $ref_inst])] { if [expr (![string compare [lindex $fm_hier_result_array([expr $i 1]) 1] $imp_inst])] { return [lindex $fm_hier_result_array([expr $i 1]) 2] } } } return UNKNOWN } ### ### Verifying instances: ### Ref: r:/WORK/top_block/inst_u1/inst_u1_sub ### Imp: i:/WORK/top_block/inst_u1/inst_u1_sub ### set_reference_design r:/WORK/u1_sub set_implementation_design i:/WORK/u1_sub set_user_match -type port $impl/a $ref/a set_user_match -type port $impl/b $ref/b set_user_match -type port $impl/y $ref/y 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/top_block/inst_u1/inst_u1_sub} {i:/WORK/top_block/inst_u1/inst_u1_sub} $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 ./sess_fail/fm_hier.log {format } redirect -append ./sess_fail/fm_hier.log {format Verification %s%s: $verification_status $fm_failure_comment} redirect -append ./sess_fail/fm_hier.log {format Ref: %s (instance of %s) {r:/WORK/top_block/inst_u1/inst_u1_sub} $ref} redirect -append ./sess_fail/fm_hier.log {format Imp: %s (instance of %s) {i:/WORK/top_block/inst_u1/inst_u1_sub} $impl} redirect -append ./sess_fail/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 ./sess_fail/fm_hier.tcl.$fm_tmp_result_count.fss lappend fm_hier_result_array($fm_tmp_result_count) ./sess_fail/fm_hier.tcl.$fm_tmp_result_count.fss redirect -append ./sess_fail/fm_hier.log {format Session file: ./sess_fail/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/a remove_user_match -type port $impl/b remove_user_match -type port $impl/y ### ### Verifying instances: ### Ref: r:/WORK/top_block/inst_u1 ### Imp: i:/WORK/top_block/inst_u1 ### set_reference_design r:/WORK/u1 set_implementation_design i:/WORK/u1 set at_least_one_black_box 0 set tmp_verification_status [get_verification_status {r:/WORK/top_block/inst_u1/inst_u1_sub} {i:/WORK/top_block/inst_u1/inst_u1_sub}] if [expr ((![string compare $tmp_verification_status SUCCEEDED]) || \ (![string compare $tmp_verification_status INCONCLUSIVE]))] { set_black_box $ref/inst_u1_sub set_black_box $impl/inst_u1_sub set at_least_one_black_box 1 set_user_match -type cell $impl/inst_u1_sub $ref/inst_u1_sub set_user_match -type pin $impl/inst_u1_sub/a $ref/inst_u1_sub/a set_user_match -type pin $impl/inst_u1_sub/b $ref/inst_u1_sub/b set_user_match -type pin $impl/inst_u1_sub/y $ref/inst_u1_sub/y } if [expr true] { } if [expr ((![string compare $tmp_verification_status SUCCEEDED]) || \ (![string compare $tmp_verification_status INCONCLUSIVE]))] { } set_user_match -type port $impl/a $ref/a set_user_match -type port $impl/b $ref/b set_user_match -type port $impl/y $ref/y set fm_begin_cputime [cputime] verify if [expr ($at_least_one_black_box) \ (![string compare $verification_status FAILED])] { setup set at_least_one_black_box 0 set tmp_verification_status [get_verification_status {r:/WORK/top_block/inst_u1/inst_u1_sub} {i:/WORK/top_block/inst_u1/inst_u1_sub}] if [expr ((![string compare $tmp_verification_status SUCCEEDED]) || \ (![string compare $tmp_verification_status INCONCLUSIVE]))] { remove_black_box $ref/inst_u1_sub remove_black_box $impl/inst_u1_sub remove_user_match -type cell $impl/inst_u1_sub remove_user_match -type pin $impl/inst_u1_sub/a remove_user_match -type pin $impl/inst_u1_sub/b remove_user_match -type pin $impl/inst_u1_sub/y } 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/top_block/inst_u1} {i:/WORK/top_block/inst_u1} $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 ./sess_fail/fm_hier.log {format } redirect -append ./sess_fail/fm_hier.log {format Verification %s%s: $verification_status $fm_failure_comment} redirect -append ./sess_fail/fm_hier.log {format Ref: %s (instance of %s) {r:/WORK/top_block/inst_u1} $ref} redirect -append ./sess_fail/fm_hier.log {format Imp: %s (instance of %s) {i:/WORK/top_block/inst_u1} $impl} redirect -append ./sess_fail/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 ./sess_fail/fm_hier.tcl.$fm_tmp_result_count.fss lappend fm_hier_result_array($fm_tmp_result_count) ./sess_fail/fm_hier.tcl.$fm_tmp_result_count.fss redirect -append ./sess_fail/fm_hier.log {format Session file: ./sess_fail/fm_hier.tcl.$fm_tmp_result_count.fss} set fm_session_files_saved [expr $fm_session_files_saved 1] } setup if [expr ($at_least_one_black_box)] { set at_least_one_black_box 0 set tmp_verification_status [get_verification_status {r:/WORK/top_block/inst_u1/inst_u1_sub} {i:/WORK/top_block/inst_u1/inst_u1_sub}] if [expr ((![string compare $tmp_verification_status SUCCEEDED]) || \ (![string compare $tmp_verification_status INCONCLUSIVE]))] { remove_black_box $ref/inst_u1_sub remove_black_box $impl/inst_u1_sub remove_user_match -type cell $impl/inst_u1_sub remove_user_match -type pin $impl/inst_u1_sub/a remove_user_match -type pin $impl/inst_u1_sub/b remove_user_match -type pin $impl/inst_u1_sub/y } } remove_user_match -type port $impl/a remove_user_match -type port $impl/b remove_user_match -type port $impl/y ### ### Verifying instances: ### Ref: r:/WORK/top_block/inst_u2/inst_u2_sub ### Imp: i:/WORK/top_block/inst_u2/inst_u2_sub ### set_reference_design r:/WORK/u2_sub set_implementation_design i:/WORK/u2_sub set_user_match -type port $impl/a $ref/a set_user_match -type port $impl/b $ref/b set_user_match -type port $impl/y $ref/y 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/top_block/inst_u2/inst_u2_sub} {i:/WORK/top_block/inst_u2/inst_u2_sub} $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 ./sess_fail/fm_hier.log {format } redirect -append ./sess_fail/fm_hier.log {format Verification %s%s: $verification_status $fm_failure_comment} redirect -append ./sess_fail/fm_hier.log {format Ref: %s (instance of %s) {r:/WORK/top_block/inst_u2/inst_u2_sub} $ref} redirect -append ./sess_fail/fm_hier.log {format Imp: %s (instance of %s) {i:/WORK/top_block/inst_u2/inst_u2_sub} $impl} redirect -append ./sess_fail/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 ./sess_fail/fm_hier.tcl.$fm_tmp_result_count.fss lappend fm_hier_result_array($fm_tmp_result_count) ./sess_fail/fm_hier.tcl.$fm_tmp_result_count.fss redirect -append ./sess_fail/fm_hier.log {format Session file: ./sess_fail/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/a remove_user_match -type port $impl/b remove_user_match -type port $impl/y ### ### Verifying instances: ### Ref: r:/WORK/top_block/inst_u2 ### Imp: i:/WORK/top_block/inst_u2 ### set_reference_design r:/WORK/u2 set_implementation_design i:/WORK/u2 set at_least_one_black_box 0 set tmp_verification_status [get_verification_status {r:/WORK/top_block/inst_u2/inst_u2_sub} {i:/WORK/top_block/inst_u2/inst_u2_sub}] if [expr ((![string compare $tmp_verification_status SUCCEEDED]) || \ (![string compare $tmp_verification_status INCONCLUSIVE]))] { set_black_box $ref/inst_u2_sub set_black_box $impl/inst_u2_sub set at_least_one_black_box 1 set_user_match -type cell $impl/inst_u2_sub $ref/inst_u2_sub set_user_match -type pin $impl/inst_u2_sub/a $ref/inst_u2_sub/a set_user_match -type pin $impl/inst_u2_sub/b $ref/inst_u2_sub/b set_user_match -type pin $impl/inst_u2_sub/y $ref/inst_u2_sub/y } if [expr true] { } if [expr ((![string compare $tmp_verification_status SUCCEEDED]) || \ (![string compare $tmp_verification_status INCONCLUSIVE]))] { } set_user_match -type port $impl/a $ref/a set_user_match -type port $impl/b $ref/b set_user_match -type port $impl/y $ref/y set fm_begin_cputime [cputime] verify if [expr ($at_least_one_black_box) \ (![string compare $verification_status FAILED])] { setup set at_least_one_black_box 0 set tmp_verification_status [get_verification_status {r:/WORK/top_block/inst_u2/inst_u2_sub} {i:/WORK/top_block/inst_u2/inst_u2_sub}] if [expr ((![string compare $tmp_verification_status SUCCEEDED]) || \ (![string compare $tmp_verification_status INCONCLUSIVE]))] { remove_black_box $ref/inst_u2_sub remove_black_box $impl/inst_u2_sub remove_user_match -type cell $impl/inst_u2_sub remove_user_match -type pin $impl/inst_u2_sub/a remove_user_match -type pin $impl/inst_u2_sub/b remove_user_match -type pin $impl/inst_u2_sub/y } 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/top_block/inst_u2} {i:/WORK/top_block/inst_u2} $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 ./sess_fail/fm_hier.log {format } redirect -append ./sess_fail/fm_hier.log {format Verification %s%s: $verification_status $fm_failure_comment} redirect -append ./sess_fail/fm_hier.log {format Ref: %s (instance of %s) {r:/WORK/top_block/inst_u2} $ref} redirect -append ./sess_fail/fm_hier.log {format Imp: %s (instance of %s) {i:/WORK/top_block/inst_u2} $impl} redirect -append ./sess_fail/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 ./sess_fail/fm_hier.tcl.$fm_tmp_result_count.fss lappend fm_hier_result_array($fm_tmp_result_count) ./sess_fail/fm_hier.tcl.$fm_tmp_result_count.fss redirect -append ./sess_fail/fm_hier.log {format Session file: ./sess_fail/fm_hier.tcl.$fm_tmp_result_count.fss} set fm_session_files_saved [expr $fm_session_files_saved 1] } setup if [expr ($at_least_one_black_box)] { set at_least_one_black_box 0 set tmp_verification_status [get_verification_status {r:/WORK/top_block/inst_u2/inst_u2_sub} {i:/WORK/top_block/inst_u2/inst_u2_sub}] if [expr ((![string compare $tmp_verification_status SUCCEEDED]) || \ (![string compare $tmp_verification_status INCONCLUSIVE]))] { remove_black_box $ref/inst_u2_sub remove_black_box $impl/inst_u2_sub remove_user_match -type cell $impl/inst_u2_sub remove_user_match -type pin $impl/inst_u2_sub/a remove_user_match -type pin $impl/inst_u2_sub/b remove_user_match -type pin $impl/inst_u2_sub/y } } remove_user_match -type port $impl/a remove_user_match -type port $impl/b remove_user_match -type port $impl/y ### ### Verifying instances: ### Ref: r:/WORK/top_block ### Imp: i:/WORK/top_block ### set_reference_design r:/WORK/top_block set_implementation_design i:/WORK/top_block set at_least_one_black_box 0 set tmp_verification_status [get_verification_status {r:/WORK/top_block/inst_u1} {i:/WORK/top_block/inst_u1}] if [expr ((![string compare $tmp_verification_status SUCCEEDED]) || \ (![string compare $tmp_verification_status INCONCLUSIVE]))] { set_black_box $ref/inst_u1 set_black_box $impl/inst_u1 set at_least_one_black_box 1 set_user_match -type cell $impl/inst_u1 $ref/inst_u1 set_user_match -type pin $impl/inst_u1/a $ref/inst_u1/a set_user_match -type pin $impl/inst_u1/b $ref/inst_u1/b set_user_match -type pin $impl/inst_u1/y $ref/inst_u1/y } 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/top_block/inst_u2} {i:/WORK/top_block/inst_u2}] if [expr ((![string compare $tmp_verification_status SUCCEEDED]) || \ (![string compare $tmp_verification_status INCONCLUSIVE]))] { set_black_box $ref/inst_u2 set_black_box $impl/inst_u2 set at_least_one_black_box 1 set_user_match -type cell $impl/inst_u2 $ref/inst_u2 set_user_match -type pin $impl/inst_u2/a $ref/inst_u2/a set_user_match -type pin $impl/inst_u2/b $ref/inst_u2/b set_user_match -type pin $impl/inst_u2/y $ref/inst_u2/y } if [expr true] { } if [expr ((![string compare $tmp_verification_status SUCCEEDED]) || \ (![string compare $tmp_verification_status INCONCLUSIVE]))] { } set fm_begin_cputime [cputime] verify if [expr ($at_least_one_black_box) \ (![string compare $verification_status FAILED])] { setup set at_least_one_black_box 0 set tmp_verification_status [get_verification_status {r:/WORK/top_block/inst_u1} {i:/WORK/top_block/inst_u1}] if [expr ((![string compare $tmp_verification_status SUCCEEDED]) || \ (![string compare $tmp_verification_status INCONCLUSIVE]))] { remove_black_box $ref/inst_u1 remove_black_box $impl/inst_u1 remove_user_match -type cell $impl/inst_u1 remove_user_match -type pin $impl/inst_u1/a remove_user_match -type pin $impl/inst_u1/b remove_user_match -type pin $impl/inst_u1/y } set tmp_verification_status [get_verification_status {r:/WORK/top_block/inst_u2} {i:/WORK/top_block/inst_u2}] if [expr ((![string compare $tmp_verification_status SUCCEEDED]) || \ (![string compare $tmp_verification_status INCONCLUSIVE]))] { remove_black_box $ref/inst_u2 remove_black_box $impl/inst_u2 remove_user_match -type cell $impl/inst_u2 remove_user_match -type pin $impl/inst_u2/a remove_user_match -type pin $impl/inst_u2/b remove_user_match -type pin $impl/inst_u2/y } 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/top_block} {i:/WORK/top_block} $verification_status] redirect -append ./sess_fail/fm_hier.log {format } redirect -append ./sess_fail/fm_hier.log {format Verification %s: $verification_status} redirect -append ./sess_fail/fm_hier.log {format Ref: %s (top) {r:/WORK/top_block}} redirect -append ./sess_fail/fm_hier.log {format Imp: %s (top) {i:/WORK/top_block}} redirect -append ./sess_fail/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 ./sess_fail/fm_hier.tcl.$fm_tmp_result_count.fss lappend fm_hier_result_array($fm_tmp_result_count) ./sess_fail/fm_hier.tcl.$fm_tmp_result_count.fss redirect -append ./sess_fail/fm_hier.log {format Session file: ./sess_fail/fm_hier.tcl.$fm_tmp_result_count.fss} set fm_session_files_saved [expr $fm_session_files_saved 1] } setup if [expr ($at_least_one_black_box)] { set at_least_one_black_box 0 set tmp_verification_status [get_verification_status {r:/WORK/top_block/inst_u1} {i:/WORK/top_block/inst_u1}] if [expr ((![string compare $tmp_verification_status SUCCEEDED]) || \ (![string compare $tmp_verification_status INCONCLUSIVE]))] { remove_black_box $ref/inst_u1 remove_black_box $impl/inst_u1 remove_user_match -type cell $impl/inst_u1 remove_user_match -type pin $impl/inst_u1/a remove_user_match -type pin $impl/inst_u1/b remove_user_match -type pin $impl/inst_u1/y } set tmp_verification_status [get_verification_status {r:/WORK/top_block/inst_u2} {i:/WORK/top_block/inst_u2}] if [expr ((![string compare $tmp_verification_status SUCCEEDED]) || \ (![string compare $tmp_verification_status INCONCLUSIVE]))] { remove_black_box $ref/inst_u2 remove_black_box $impl/inst_u2 remove_user_match -type cell $impl/inst_u2 remove_user_match -type pin $impl/inst_u2/a remove_user_match -type pin $impl/inst_u2/b remove_user_match -type pin $impl/inst_u2/y } } 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 ./sess_fail/fm_hier.log] puts [read $fm_log_fp] close $fm_log_fp上述层次化验证脚本的验证过程可以用下面的流程图描述。开始 │ ▼ 初始化层次化验证环境 │ ├─ 保存原有验证参数 ├─ 关闭指定的常量传播及签名分析匹配功能 ├─ 初始化验证结果数组和计数器 ├─ 创建 fm_hier.log 日志 └─ 定义 get_verification_status 过程 │ ▼ 验证底层模块 u1_sub │ ├─ 设置 Reference / Implementation ├─ 建立模块端口匹配关系 ├─ 执行 verify ├─ 记录验证状态、CPU时间和内存 └─ 清理端口匹配关系 │ ▼ 验证中间层模块 u1 │ ▼ 查询 u1_sub 的验证状态 │ ├─ SUCCEEDED / INCONCLUSIVE │ │ │ ├─ 将两侧 u1_sub 设置为 Black Box │ └─ 建立黑盒实例及引脚匹配关系 │ └─ FAILED / 其他状态 │ └─ 不设置 Black Box │ ▼ 执行 u1 的 verify │ ▼ 是否存在 Black Box 且验证 FAILED │ ├─ 是 │ ├─ 取消 Black Box │ ├─ 清理对应匹配关系 │ └─ 重新执行 verify │ └─ 否 └─ 保留当前验证结果 │ ▼ 记录 u1 验证状态并清理临时设置 │ ▼ 验证底层模块 u2_sub │ ├─ 设置 Reference / Implementation ├─ 建立模块端口匹配关系 ├─ 执行 verify ├─ 记录验证结果 └─ 清理端口匹配关系 │ ▼ 验证中间层模块 u2 │ ├─ 查询 u2_sub 验证状态 │ ├─ SUCCEEDED / INCONCLUSIVE │ └─ 设置 Black Box 并匹配实例及引脚 │ └─ FAILED / 其他状态 └─ 不设置 Black Box │ ▼ 执行 u2 的 verify │ ▼ 是否存在 Black Box 且验证 FAILED │ ├─ 是 │ ├─ 取消 Black Box │ ├─ 清理对应匹配关系 │ └─ 重新执行 verify │ └─ 否 └─ 保留当前验证结果 │ ▼ 记录 u2 验证状态并清理临时设置 │ ▼ 验证顶层设计 top_block │ ├─ 查询 u1 的验证状态 │ ├─ SUCCEEDED / INCONCLUSIVE → 设置 Black Box │ └─ FAILED / 其他状态 → 不设置 Black Box │ ├─ 查询 u2 的验证状态 │ ├─ SUCCEEDED / INCONCLUSIVE → 设置 Black Box │ └─ FAILED / 其他状态 → 不设置 Black Box │ └─ 建立黑盒实例及引脚匹配关系 │ ▼ 执行 top_block 的 verify │ ▼ 是否存在 Black Box 且验证 FAILED │ ├─ 是 │ ├─ 取消 u1 / u2 的 Black Box │ ├─ 清理对应匹配关系 │ └─ 重新执行 verify │ └─ 否 └─ 保留当前验证结果 │ ▼ 记录顶层验证结果 │ ▼ 清理临时 Black Box 和匹配关系 │ ▼ 恢复原有验证参数 │ ▼ 汇总所有层级的验证结果 │ ├─ 输出 fm_hier.log └─ 满足条件时保存 INCONCLUSIVE 的 Session │ ▼ 结束