相关阅读Design Compilerhttps://blog.csdn.net/weixin_45791458/category_12738116.html?spm1001.2014.3001.5482SVF文件简介SVF文件的全称是Setup Verification for Formality即Design Compiler提供给Formality的设置验证文件它的作用是为Formality的指导模式(Guidance)和设置模式(Setup)提供信息以帮助其更好地理解和处理设计流程中因使用Design Compiler而引起的设计变更的一种机制。SVF文件记录了在综合过程中的下面这些信息对象名称更改(Object name changes)综合工具可能在综合过程中改变对象如触发器、模块、信号等的名称比如group、ungroup、uniquify和change_names命令记录该信息可以帮助验证工具正确匹配变更前后的比较点(Compare Points)。常量触发器优化(Constant register optimizations)综合工具可能在综合过程中对包含固定值的触发器进行优化记录该信息可以帮助验证工具理解这些优化后的触发器。重复和合并触发器(Duplicate and merged registers)综合工具可能在综合过程中将功能相同的多个触发器合并以减少资源使用记录该信息可以帮助验证工具正确处理。乘法器和除法器架构类型(Multiplier and divider architecture types)综合工具可能在综合过程中用不同的硬件实现方式(DesignWare)来优化乘法和除法操作记录该信息便于验证工具理解。·数据路径转换(Datapath transformations)综合工具可能在综合过程中对数据路径进行优化例如重排、共享硬件资源等记录该信息以验证数据路径。有限状态机重新编码(FSM re-encoding)综合工具可能在综合过程中对状态机进行重新编码如从二进制编码改为独热码需要在Formality中启用相关功能设置svf_ignore_unqualified_fsm_information变量为false才能使用这些信息帮助工具正确匹配变更前后的状态机。时序重排(Retiming)综合工具可能在综合过程中调整触发器位置以优化时序性能如减少关键路径延迟。SVF 文件提供这些调整的信息以确保验证工具能识别这些优化。触发器相位反转(Register phase inversion)综合工具可能在综合过程中对某些触发器信号进行了相位反转如时钟信号被反相确保验证工具处理相应的变化。set_svf命令set_svf命令的的BNF范式有关BNF范式可以参考以往文章为set_svf filename [-append | -off]指定文件名filename参数指定了SVF文件名需要注意的是除非使用了-off选项否则必须指定文件名。默认情况下在Design Compiler安装目录的配置文件.synopsys_dc.setup会有一条默认的set_svf命令设置的文件名为default.svf这也就解释了为什么Design Compiler运行后在工作目录会生成default.svf文件了。指定追加-append选项将信息附加到指定SVF文件如果另一个SVF文件已使用本命令打开则会在打开指定SVF文件之前关闭另一个SVF文件。如果未使用-append选项则会覆盖已存在的文件。指定关闭-off选项停止记录如果要恢复记录到同一文件必须重新运行set_svf命令并添加-append选项。详细描述此命令的会使Design Compiler开始为FormalitySynopsys的逻辑等价性检查工具记录信息。通过使用自动生成SVF文件用户可以免去手动输入信息的繁琐和易出错过程。如果要为其他形式验证工具记录信息请使用set_vsdc命令。一旦使用此命令Design Compiler将开始记录所有相关信息由于信息是内部缓冲的因此文件可能不会立即完成直到停止记录为止。set_svf -off命令可以停止当前记录set_svf new_file命令可以停止当前记录并在新的SVF文件中继续记录quit命令和exit命令会停止记录并退出Design Compiler注意直接Kill进程会导致SVF文件损坏。SVF文件以加密格式存储当Formality加载SVF文件后会在当前工作目录创建一个formality_svf目录其中的svf.txt文件会包含所有被解密的svf信息。示例下面一个简单的由乘法运算符描述的乘法器在综合后它将以DesignWare组件实现。module top_module(input [3:0]A, B, output [3:0]SUM); assign SUM A B; endmodule使用下面的脚本进行综合假设环境已提前设置set_svf命令应该在进行操作前设置。set_svf test.svf read_file -format verilog {/home/zhangchen/Desktop/formality/top_module.v} compile -exact_map write_file -format verilog -hierarchy -output top_module.mapped.v exit在Design Compiler的当前工作目录中生成了一个名为test.svf的二进制文件使用Formality可以打开它。1、可以选择使用Formality的GUI界面进行SVF文件的加载如图1所示。图1 加载SVF文件2、可以选择命令行的方式执行set_svf命令与DC中的命令同名即可如下所示。Formality (setup) set_svf -append { /home/zhangchen/Desktop/formality/test.svf }一旦SVF文件被加载Formality就会在当前工作目录的formality_svf子目录中找到svf.txt文件其内容如下所示。# Active SVF file /home/zhangchen/Desktop/formality/test.svf #----------------------------------------------------------------------------- # This file is automatically generated by Design Compiler # Filename : /home/zhangchen/Desktop/formality/test.svf # Timestamp : Thu Nov 28 00:25:39 2024 # DC Version: O-2018.06-SP1 (built Jul 19, 2018) #----------------------------------------------------------------------------- guide guide_environment \ { { cwd /home/zhangchen/Desktop/formality } } guide_mark \ -type { svfMarkTypeBegin } \ -phase { svfMarkPhasePresto } guide_info \ -version { /home/zhangchen/Desktop/formality/top_module.v 15.078 } guide_mark \ -type { svfMarkTypeEnd } \ -phase { svfMarkPhasePresto } guide_environment \ { { read_verilog /home/zhangchen/Desktop/formality/top_module.v } \ { current_design top_module } } guide_transformation \ -design { top_module } \ -type { map } \ -input { 4 src1 } \ -input { 4 src2 } \ -output { 4 src3 } \ -pre_resource { { 4 } add_3 UADD { { src1 } { src2 } } } \ -pre_assign { src3 { add_3.out.1 } } \ -post_resource { { 4 } add_3 ADD { { src1 } { src2 } } } \ -post_assign { src3 { add_3.out.1 } } guide_environment \ { { current_design top_module } \ { write_file { -format verilog -hierarchy -output top_module.mapped.v } } \ { current_design top_module } } #---- Recording stopped at Thu Nov 28 00:27:48 2024 setup可以看到其实SVF文件就是由Formality命令构成的文件第一条命令是guide这是因为Formality启动时默认进入setup模式而只有使用guide命令进入guide模式才能执行guide类命令比如guide_environment命令。在SVF文件的最后使用setup命令重新回到了setup模式。这些guide类命令加载/执行后会在preverify模式进行处理不一定被接受并在match模式和verification模式考虑到这些信息。顺带一提用户可以使用fm_mk_script程序其实它是一个指向fm_shell的符号链接但fm_shell可以根据启动命令名判断执行哪部分程序将Design Compiler生成的SVF文件直接转换为等价性检查的脚本免去工程师手动编写设计读入、库加载和环境配置的繁琐工作快速完成环境搭建如下所示。$ fm_mk_script test.svf -output test.tclfm_mk_script程序的转换结果如下所示可以看到甚至不需要用户读取设计文件因为SVF文件中记录了这些信息利用guide_environment命令。######################################################################## # Formality Verification Script generated by: # fm_mk_script -o test.tcl test.svf # Formality (R) Version O-2018.06-SP1 -- Jul 18, 2018 # Copyright (C) 2007-2010 Synopsys, Inc. All rights reserved. ######################################################################## ######################################################################## # Synopsys Auto Setup Mode ######################################################################## set synopsys_auto_setup true # Note: The Synopsys Auto Setup mode is less conservative than the # Formality default mode, and is more likely to result in a successful # verification out-of-the-box. # # Setting synopsys_auto_setup will change the values of the variables # listed here below. You may change any of these variables back to # their default settings to be more conservative. Uncomment the # appropriate lines below to revert back to their default settings: # set hdlin_ignore_parallel_case true # set hdlin_ignore_full_case true # set verification_verify_directly_undriven_output true # set hdlin_ignore_embedded_configuration false # set svf_ignore_unqualified_fsm_information true ######################################################################## # Specify number of processes on the local machine to use in parallel # Default is 1 core ######################################################################## #set_host_options -max_cores 4 ######################################################################## # Read in the SVF file(s) ######################################################################## set_svf test.svf ######################################################################## # Read in the libraries ######################################################################## ######################################################################## ######################################################################## # Read in the Reference Design as verilog/vhdl source code ######################################################################## # No guide_environment analyze commands found in SVF # read_verilog -r \ /home/zhangchen/Desktop/formality/top_module.v # USER INTERVENTION REQUIRED HERE: # set_top top_module ######################################################################## # Read in the Implementation Design created from DC # # Choose the file that you wish to verify ######################################################################## read_verilog -i /home/zhangchen/Desktop/formality/top_module.mapped.v # USER INTERVENTION REQUIRED HERE: # set_top top_module ######################################################################## # Verify and Report # # If the verification is not successful, the session will be saved and reports # will be generated to help debug the failed or inconclusive verification. ######################################################################## if { ![verify] } { set DESIGN_NAME top_module ;# The name of the top-level design set FMRM_FAILING_SESSION_NAME ${DESIGN_NAME} set FMRM_FAILING_POINTS_REPORT ${DESIGN_NAME}.fmv_failing_points.rpt set FMRM_ABORTED_POINTS_REPORT ${DESIGN_NAME}.fmv_aborted_points.rpt set REPORTS_DIR reports file mkdir ${REPORTS_DIR} save_session -replace ${REPORTS_DIR}/${FMRM_FAILING_SESSION_NAME} report_failing_points ${REPORTS_DIR}/${FMRM_FAILING_POINTS_REPORT} report_aborted ${REPORTS_DIR}/${FMRM_ABORTED_POINTS_REPORT} }
相关阅读Design Compilerhttps://blog.csdn.net/weixin_45791458/category_12738116.html?spm1001.2014.3001.5482SVF文件简介SVF文件的全称是Setup Verification for Formality即Design Compiler提供给Formality的设置验证文件它的作用是为Formality的指导模式(Guidance)和设置模式(Setup)提供信息以帮助其更好地理解和处理设计流程中因使用Design Compiler而引起的设计变更的一种机制。SVF文件记录了在综合过程中的下面这些信息对象名称更改(Object name changes)综合工具可能在综合过程中改变对象如触发器、模块、信号等的名称比如group、ungroup、uniquify和change_names命令记录该信息可以帮助验证工具正确匹配变更前后的比较点(Compare Points)。常量触发器优化(Constant register optimizations)综合工具可能在综合过程中对包含固定值的触发器进行优化记录该信息可以帮助验证工具理解这些优化后的触发器。重复和合并触发器(Duplicate and merged registers)综合工具可能在综合过程中将功能相同的多个触发器合并以减少资源使用记录该信息可以帮助验证工具正确处理。乘法器和除法器架构类型(Multiplier and divider architecture types)综合工具可能在综合过程中用不同的硬件实现方式(DesignWare)来优化乘法和除法操作记录该信息便于验证工具理解。·数据路径转换(Datapath transformations)综合工具可能在综合过程中对数据路径进行优化例如重排、共享硬件资源等记录该信息以验证数据路径。有限状态机重新编码(FSM re-encoding)综合工具可能在综合过程中对状态机进行重新编码如从二进制编码改为独热码需要在Formality中启用相关功能设置svf_ignore_unqualified_fsm_information变量为false才能使用这些信息帮助工具正确匹配变更前后的状态机。时序重排(Retiming)综合工具可能在综合过程中调整触发器位置以优化时序性能如减少关键路径延迟。SVF 文件提供这些调整的信息以确保验证工具能识别这些优化。触发器相位反转(Register phase inversion)综合工具可能在综合过程中对某些触发器信号进行了相位反转如时钟信号被反相确保验证工具处理相应的变化。set_svf命令set_svf命令的的BNF范式有关BNF范式可以参考以往文章为set_svf filename [-append | -off]指定文件名filename参数指定了SVF文件名需要注意的是除非使用了-off选项否则必须指定文件名。默认情况下在Design Compiler安装目录的配置文件.synopsys_dc.setup会有一条默认的set_svf命令设置的文件名为default.svf这也就解释了为什么Design Compiler运行后在工作目录会生成default.svf文件了。指定追加-append选项将信息附加到指定SVF文件如果另一个SVF文件已使用本命令打开则会在打开指定SVF文件之前关闭另一个SVF文件。如果未使用-append选项则会覆盖已存在的文件。指定关闭-off选项停止记录如果要恢复记录到同一文件必须重新运行set_svf命令并添加-append选项。详细描述此命令的会使Design Compiler开始为FormalitySynopsys的逻辑等价性检查工具记录信息。通过使用自动生成SVF文件用户可以免去手动输入信息的繁琐和易出错过程。如果要为其他形式验证工具记录信息请使用set_vsdc命令。一旦使用此命令Design Compiler将开始记录所有相关信息由于信息是内部缓冲的因此文件可能不会立即完成直到停止记录为止。set_svf -off命令可以停止当前记录set_svf new_file命令可以停止当前记录并在新的SVF文件中继续记录quit命令和exit命令会停止记录并退出Design Compiler注意直接Kill进程会导致SVF文件损坏。SVF文件以加密格式存储当Formality加载SVF文件后会在当前工作目录创建一个formality_svf目录其中的svf.txt文件会包含所有被解密的svf信息。示例下面一个简单的由乘法运算符描述的乘法器在综合后它将以DesignWare组件实现。module top_module(input [3:0]A, B, output [3:0]SUM); assign SUM A B; endmodule使用下面的脚本进行综合假设环境已提前设置set_svf命令应该在进行操作前设置。set_svf test.svf read_file -format verilog {/home/zhangchen/Desktop/formality/top_module.v} compile -exact_map write_file -format verilog -hierarchy -output top_module.mapped.v exit在Design Compiler的当前工作目录中生成了一个名为test.svf的二进制文件使用Formality可以打开它。1、可以选择使用Formality的GUI界面进行SVF文件的加载如图1所示。图1 加载SVF文件2、可以选择命令行的方式执行set_svf命令与DC中的命令同名即可如下所示。Formality (setup) set_svf -append { /home/zhangchen/Desktop/formality/test.svf }一旦SVF文件被加载Formality就会在当前工作目录的formality_svf子目录中找到svf.txt文件其内容如下所示。# Active SVF file /home/zhangchen/Desktop/formality/test.svf #----------------------------------------------------------------------------- # This file is automatically generated by Design Compiler # Filename : /home/zhangchen/Desktop/formality/test.svf # Timestamp : Thu Nov 28 00:25:39 2024 # DC Version: O-2018.06-SP1 (built Jul 19, 2018) #----------------------------------------------------------------------------- guide guide_environment \ { { cwd /home/zhangchen/Desktop/formality } } guide_mark \ -type { svfMarkTypeBegin } \ -phase { svfMarkPhasePresto } guide_info \ -version { /home/zhangchen/Desktop/formality/top_module.v 15.078 } guide_mark \ -type { svfMarkTypeEnd } \ -phase { svfMarkPhasePresto } guide_environment \ { { read_verilog /home/zhangchen/Desktop/formality/top_module.v } \ { current_design top_module } } guide_transformation \ -design { top_module } \ -type { map } \ -input { 4 src1 } \ -input { 4 src2 } \ -output { 4 src3 } \ -pre_resource { { 4 } add_3 UADD { { src1 } { src2 } } } \ -pre_assign { src3 { add_3.out.1 } } \ -post_resource { { 4 } add_3 ADD { { src1 } { src2 } } } \ -post_assign { src3 { add_3.out.1 } } guide_environment \ { { current_design top_module } \ { write_file { -format verilog -hierarchy -output top_module.mapped.v } } \ { current_design top_module } } #---- Recording stopped at Thu Nov 28 00:27:48 2024 setup可以看到其实SVF文件就是由Formality命令构成的文件第一条命令是guide这是因为Formality启动时默认进入setup模式而只有使用guide命令进入guide模式才能执行guide类命令比如guide_environment命令。在SVF文件的最后使用setup命令重新回到了setup模式。这些guide类命令加载/执行后会在preverify模式进行处理不一定被接受并在match模式和verification模式考虑到这些信息。顺带一提用户可以使用fm_mk_script程序其实它是一个指向fm_shell的符号链接但fm_shell可以根据启动命令名判断执行哪部分程序将Design Compiler生成的SVF文件直接转换为等价性检查的脚本免去工程师手动编写设计读入、库加载和环境配置的繁琐工作快速完成环境搭建如下所示。$ fm_mk_script test.svf -output test.tclfm_mk_script程序的转换结果如下所示可以看到甚至不需要用户读取设计文件因为SVF文件中记录了这些信息利用guide_environment命令。######################################################################## # Formality Verification Script generated by: # fm_mk_script -o test.tcl test.svf # Formality (R) Version O-2018.06-SP1 -- Jul 18, 2018 # Copyright (C) 2007-2010 Synopsys, Inc. All rights reserved. ######################################################################## ######################################################################## # Synopsys Auto Setup Mode ######################################################################## set synopsys_auto_setup true # Note: The Synopsys Auto Setup mode is less conservative than the # Formality default mode, and is more likely to result in a successful # verification out-of-the-box. # # Setting synopsys_auto_setup will change the values of the variables # listed here below. You may change any of these variables back to # their default settings to be more conservative. Uncomment the # appropriate lines below to revert back to their default settings: # set hdlin_ignore_parallel_case true # set hdlin_ignore_full_case true # set verification_verify_directly_undriven_output true # set hdlin_ignore_embedded_configuration false # set svf_ignore_unqualified_fsm_information true ######################################################################## # Specify number of processes on the local machine to use in parallel # Default is 1 core ######################################################################## #set_host_options -max_cores 4 ######################################################################## # Read in the SVF file(s) ######################################################################## set_svf test.svf ######################################################################## # Read in the libraries ######################################################################## ######################################################################## ######################################################################## # Read in the Reference Design as verilog/vhdl source code ######################################################################## # No guide_environment analyze commands found in SVF # read_verilog -r \ /home/zhangchen/Desktop/formality/top_module.v # USER INTERVENTION REQUIRED HERE: # set_top top_module ######################################################################## # Read in the Implementation Design created from DC # # Choose the file that you wish to verify ######################################################################## read_verilog -i /home/zhangchen/Desktop/formality/top_module.mapped.v # USER INTERVENTION REQUIRED HERE: # set_top top_module ######################################################################## # Verify and Report # # If the verification is not successful, the session will be saved and reports # will be generated to help debug the failed or inconclusive verification. ######################################################################## if { ![verify] } { set DESIGN_NAME top_module ;# The name of the top-level design set FMRM_FAILING_SESSION_NAME ${DESIGN_NAME} set FMRM_FAILING_POINTS_REPORT ${DESIGN_NAME}.fmv_failing_points.rpt set FMRM_ABORTED_POINTS_REPORT ${DESIGN_NAME}.fmv_aborted_points.rpt set REPORTS_DIR reports file mkdir ${REPORTS_DIR} save_session -replace ${REPORTS_DIR}/${FMRM_FAILING_SESSION_NAME} report_failing_points ${REPORTS_DIR}/${FMRM_FAILING_POINTS_REPORT} report_aborted ${REPORTS_DIR}/${FMRM_ABORTED_POINTS_REPORT} }
)
