1.  设置环境变量

setenv VC_STATIC_HOME xx/synopsys/vc_static/U-2023.03-SP2-2
module load synopsys/vcs_U-2023.03-SP2-2
setenv PATH xx/bin:xx/bin:PATH
others

   note: setenv PATH中:为路径分隔符.

2. run.tcl脚本文件内容

set ENV_DIR ..
set SVA_DIR ../02_sva
set ::env(SVA_DIR) $SVA_DIR   //将 Tcl 变量$SVA_DIR的值赋值给环境变量SVA_DIR，以便在当前脚本或后续调用的程序中使用该环境变量

set_flm_appmode FRV           //一条用于配置工具工作模式为 形式化寄存器验证的 命令
frv_config -generate_backdoor_checks 1 //是控制是否生成 “后门访问检查” 的选项，1 表示启用（0 表示禁用）
frv_load -ral xx/.ralf -top core_top -auto_load   //将寄存器的抽象规范（.ralf 文件）与实际硬件设计（顶层模块 core_top）自动关联，确保验证工具能对比 “理想模型” 和 “硬件实现”, -top 选项指定硬件设计的顶层模块名,-auto_load 自动关联选项，开启后工具会根据 .ralf 文件中的寄存器名称、地址等信息，自动在 core_top 模块的层级下搜索匹配的硬件寄存器实例
read_file -top core_top_reg -formal sverilog -sva -vcs "-f ../00_filelist/filelist.f $SVA_DIR/bind_frv.sv"        //用于加载设计文件和断言文件的核心操作，目的是将寄存器相关的 RTL 代码、SVA 断言以及绑定逻辑导入到验证环境中，为后续的形式化验证（尤其是寄存器验证）做准备

set_constant -value 'h0 -hierarchical signal   //将指定信号固定为常量，通常是与当前验证目标无关的信号。
sim_force signal -applay 0   //动态仿真中用到.

create_clock clk -period 100    //声明时钟，为之前frv_load/read_file -top中的设计文件下的信号
create_reset rst_n -sense low   //声明复位，低有效，为之前frv_load/read_file -top中的设计文件下的信号

fvdisable {*.cov_out_addr_read_before_first_write}
fvdisable {*.cov_out_addr_read_before_first_read}
fvdisable {*.cov_out_addr_read_between_write_read}
fvdisable {*.cov_out_addr_write_before_first_read}
fvdisable {*.cov_out_addr_write_between_write_read} 
fvdisable {*.cov_diff_addr_read_before_first_write}  
fvdisable {*.cov_diff_addr_read_before_first_read}  
fvdisable {*.cov_diff_addr_read_between_write_read}  
fvdisable {*.cov_diff_addr_write_before_first_read}  
fvdisable {*.cov_diff_addr_write_between_write_read} 
fvdisable {*.cov_first_read_before_write} 
fvdisable {*.cov_read_after_read_before_write} 
fvdisable {*.cov_first_read_after_read_before_write}   fvdisable{*.cov_first_read_after_read_and_write} 
fvdisable{*.cov_read_only_write}    
fvdisable{*.cov_write_only_read}  
fvdisable{*.ast_rw_bdr_write_check} 
fvdisable{core_top_reg.i_snps_frv_generic.i_snps_frv.i_core_top.i_core_top_blk.xx_signal.RX.CHKBDR.CHKWR.ast_rw_bdr_write_check}

sim_run -stable //是用于执行仿真并等待设计达到稳定状态的命令，主要作用是让仿真工具运行到 “设计中所有信号值不再随时间变化（稳定）” 后自动停止，而无需手动指定仿真结束时间
sim_save_reset //是一个用于保存复位状态快照的命令，主要作用是在仿真过程中记录设计在复位状态下的所有信号值，以便后续快速恢复到该状态，无需重新执行复位序列
check_fv //是用于启动形式化属性验证流程的核心命令，其主要作用是让工具对已加载的设计、属性（Properties）和约束（Assumptions）进行数学逻辑分析，验证设计是否满足所有指定的形式化属性

3. bind设计与frv

bind core_top_reg snps_frv_gen_wrapper i_snps_frv_generic(
 .clk(clk),
 .resetn(rst_n),
 .addr(i_cfg_addr),
 .wren(wren),
 .xx(xx)
);

4.启动

  bsub -Is vcf -f run.tcl -verdi&

5.调试

  执行run.tcl后，会打开verdi，结果会显示到VCF.GoalList(FRV)中，会明确列出property 的name，失败的用例可以根据这个name去搜索看看是哪里出错.

6. 简单理解

 对于reg的formal验证，就是工具会根据ralf文件中的属性，自动生成很多的property检查，比如reset值的检查，只读只写的检查等，工具根据这些属性来生成property，而不需要像uvm验证中那样给定激励，然后给定clk和rst，tb就会自动执行，property检查不通过就会fail.