相关阅读
Design Compilerhttps://blog.csdn.net/weixin_45791458/category_12738116.html?spm=1001.2014.3001.5482
SVF文件简介
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开始为Formality（Synopsys的逻辑等价性检查工具）记录信息。通过使用自动生成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} }
