第七篇官方示例工程详解

# 设置路径变量
set ROOT_PATH ../designs/reference_design/verilog_sva
set RTL_PATH ${ROOT_PATH}/source/design
set PROP_PATH ${ROOT_PATH}/source/properties

# 分析 RTL 设计文件（Verilog 格式）
analyze -verilog \
  ${RTL_PATH}/arbiter.v \
  ${RTL_PATH}/port_select.v \
  ${RTL_PATH}/bridge.v \
  ${RTL_PATH}/egress.v \
  ${RTL_PATH}/ingress.v \
  ${RTL_PATH}/top.v

# 分析 SVA 属性文件
analyze -sva \
  ${PROP_PATH}/bindings.sva \
  ${PROP_PATH}/v_arbiter.sva \
  ${PROP_PATH}/v_bridge.sva \
  ${PROP_PATH}/v_ingress.sva \
  ${PROP_PATH}/v_egress.sva \
  ${PROP_PATH}/v_port_select.sva

# Elaborate：展开设计层次、连接属性、建立形式模型
elaborate -top top

# 声明时钟和复位
clock clk
reset ~rstN

# 获取设计复杂度信息（状态空间、信号数量等）
get_design_info

# ---- 第一轮证明：快速浅层验证 ----
set_max_trace_length 10
prove -all

# ---- 第二轮证明：深度证明 ----
set_max_trace_length 50
set_prove_per_property_time_limit 30s
set_engine_mode {K I N}
prove -all

# 报告结果
report

// 断言1：授权信号始终是 one-hot 或全零（互斥授权）
property grant_is_onehot0;
  @(posedge clk) $onehot0(gnt);
endproperty
a_grant_is_onehot0: assert property (grant_is_onehot0);

// 断言2：授权只持续一个周期
property grant_is_one_cycle;
  @(posedge clk) (gnt!=4'b0) |=> (gnt==4'b0);
endproperty
a_grant_is_one_cycle: assert property (grant_is_one_cycle);

// Cover 点：每个请求端口和授权端口都被覆盖
c_req0: cover property (@(posedge clk) (req[0]));
c_gnt0: cover property (@(posedge clk) (gnt[0]));

# 黑盒化寄存器堆（不需要验证其内部）
elaborate -bbox_m modreg_bank

# 声明 4 个时钟域
clock clock_control1
clock clock_control2
clock clock_fsm
clock clock_fsm clock_fsm_aux 2 1  # 分频时钟（2:1）

# 用 clock -rate 将输入端口关联到对应时钟域
clock -rate {en_control clock_control_sel ...} clock_control1
clock -rate {en_fsm proc_int_code ...} clock_fsm
clock -rate counter_en clock_fsm_aux

# 声明复位（3个异步复位，低有效）
reset ~reset_n_control1 ~reset_n_control2 ~reset_n_fsm

# 信号配置：将使能信号设为常量 1
check_cdc -signal_config -add_constant {{en_fsm 1'b1} {en_control 1'b1} ...}
check_cdc -signal_config -add_static {{conv_br1_reg}}

# 设置规则严重级别
check_cdc -check -severity {fatal {no_scheme}}
check_cdc -check -severity {error {cdc_pair_logic sync_chain_logic}}

# 核心 CDC 流程
check_cdc -clock_domain -find          # 查找时钟域
check_cdc -clock_domain -join jg_clock_fsm_aux -into jg_clock_fsm  # 合并分频域
check_cdc -pair -find                  # 查找 CDC 对（跨域路径）
check_cdc -scheme -find                # 查找同步器方案

# 添加用户定义的 FIFO 同步器方案
check_cdc -scheme -add FIFO -map {...}

# 添加豁免（waiver）
check_cdc -waiver -add -filter [...] -comment {Input to be synchronized externally}

# 查找收敛点
check_cdc -group -find

# 验证豁免条件
check_cdc -waiver -generate
check_cdc -waiver -prove

# 协议检查（验证同步器功能正确性）
check_cdc -protocol_check -generate
check_cdc -protocol_check -prove

# 亚稳态注入（MSI）
check_cdc -metastability -inject
check_cdc -metastability -prove

# 生成报告
check_cdc -report pairs -file .../pairs.csv
check_cdc -report violations -file .../violations.csv
check_cdc -report signoff -file .../signoff.csv

# SEC 设置：指定 spec 和 imp 的顶层、分析选项、展开选项
check_sec -setup -spec_top uart_top \
            -imp_top uart_top \
            -spec_analyze "-sv -f ${SPEC_RTL_PATH}/sec_spec.vfile" \
            -imp_analyze  "-sv -f ${IMP_RTL_PATH}/sec_imp.vfile" \
            -spec_elaborate_opts "-bbox_m uart_tfifo" \
            -imp_elaborate_opts "-bbox_m uart_tfifo"

# 时钟声明
clock wb_clk_i
clock -rate wb_cyc_i wb_clk_i   # 将 Wishbone 接口信号关联到时钟域
clock -rate wb_stb_i wb_clk_i
# ... 其他接口信号

# 复位
reset wb_rst_i

# 自动映射未初始化寄存器的 X 值
check_sec -auto_map_reset_x_values on

# 接口检查：报告 spec 和 imp 之间端口不匹配
check_sec -interface

# 手动映射自动映射未覆盖的地址端口
check_sec -map -spec {wb_adr_i[4:0]} -imp {uart_top_imp.wb_address_i[4:0]} \
  -respect_connections_during_reset -global

# 生成等价性验证环境（创建映射点对和等价检查属性）
check_sec -gen

# 证明
set_prove_time_limit 30s
check_sec -prove

# Signoff
check_sec -signoff

# setup 过程在 elaborate 后调用
proc setup {} {
    clock clk
    reset reset
    assert -disable *::*         # 禁用所有自动断言
    cover -disable *::*
    assert -enable "<embedded>::top.efficiency"  # 只使能 efficiency 相关
    assume -env { vdd_net } -name vdd_net_always_on  # vdd 电源常开
}

clear -all
set PATH "../designs/lpv_design"
set_engine_mode {Ht Hp B N}        # 多引擎组合
set_prove_time_limit 100s          # 较长时间限制

analyze -sv {*}[glob $PATH/*.v]
elaborate -clear
elaborate -top top

# 加载 UPF 电源意图
check_lpv -load_upf top.upf

# 自动生成电源感知 RTL
check_lpv -generate_power_design

setup

# ---- 结构检查（10项）----
check_lpv -verify check_iso_clk_all          # 隔离单元时钟
check_lpv -verify check_iso_inputs           # 隔离输入
check_lpv -verify check_iso_outputs          # 隔离输出
check_lpv -verify check_iso_ctrl_rst         # 隔离控制/复位
check_lpv -verify check_iso_connections      # 隔离连接
check_lpv -verify check_ret_connections      # 保持寄存器连接
check_lpv -verify check_iso_default_value    # 隔离默认值
check_lpv -verify check_ret_ctrl_rst         # 保持控制/复位
check_lpv -verify check_power_switch_connections  # 电源开关连接
check_lpv -verify check_power_switch_ctrl_rst     # 电源开关控制/复位

# ---- 功能检查（12项）----
check_lpv -create assert_iso_up_before       # 电源开启前隔离
check_lpv -create assert_iso_supply          # 隔离供电
check_lpv -create assert_iso_up_after        # 电源开启后隔离
check_lpv -create assert_ret_supply_on_save  # save 时保持供电
check_lpv -create assert_ret_supply_on_restore  # restore 时保持供电
check_lpv -create cover_power_switch_ctrl    # 电源开关控制覆盖
# ... 更多功能检查

prove -property <LowPower>::lpv::*

# 查看隔离输出的反例波形
visualize -violation -property <LowPower>::lpv::iso_up_after_iso_output__PD_MEM -new_window

clear -all
check_xprop -init_control 1    # 启用 X 初始化控制模式

# 分析 RTL
set RTL_PATH ../designs/reference_design/verilog_sva/source/design
analyze -verilog \
  ${RTL_PATH}/arbiter.v ${RTL_PATH}/port_select.v ${RTL_PATH}/bridge.v \
  ${RTL_PATH}/egress.v ${RTL_PATH}/ingress.v ${RTL_PATH}/top.v

elaborate -top top
clock clk
reset ~rstN
get_design_info

# 创建三类 X-Prop 属性
check_xprop -create -outputs -no_bit_blast         # 检查输出端口的 X 传播
check_xprop -create -control -no_bit_blast          # 检查控制信号的 X
check_xprop -create -clocks_and_resets -no_bit_blast  # 检查时钟/复位的 X

set_max_trace_length 10
check_xprop -prove -no_decompose -all
report

# 配置 Blackbox Assistant 自动优化黑盒
blackbox_assistant -config -connectivity_map conn.csv
elaborate -top top

clock clk
reset ~rstN

# 加载连接映射表（CSV 格式定义了源→目的连接）
check_conn -load conn.csv

# COI 验证：连接的信号在彼此的影响锥内
check_conn -validate

# 翻转检查：翻转源端看目的端是否翻转
check_conn -generate_toggle_checks {}

check_conn -prove
report

blackbox_assistant -config -max_depth 0
elaborate -top top

clock clk
reset ~rstN

# 自动从 RTL 提取连接关系
# -src 指定源模块列表，工具追踪所有从这些模块出发的连接
check_conn -reverse -src {ing0 ing1 ing2 ing3 eg brdg arb p_sel} -load

check_conn -validate
check_conn -generate_toggle_checks {}
check_conn -prove

# 在 elaboration 之前初始化 COV
check_cov -init -model {branch statement expression toggle functional} \
  -toggle_ports_only -exclude_bind_hierarchies

# analyze + elaborate ...
# clock + reset ...

# 先证明所有属性
set_max_trace_length 9
prove -all

# 生成覆盖率指标
check_cov -measure -no_auto

set CSR_MAP uart_top_JasperCSR.csv

# 分析 UART RTL
analyze +define+DATA_BUS_WIDTH_8 -sv +incdir+${RTL_PATH} \
       ${RTL_PATH}/uart_top.v ${RTL_PATH}/uart_receiver.v \
       ${RTL_PATH}/uart_regs.v ${RTL_PATH}/uart_tfifo.v \
       ${RTL_PATH}/uart_transmitter.v ${RTL_PATH}/uart_wb.v ...

# 分析 Wishbone 总线约束文件
analyze -sv +incdir+${RTL_PATH} ${PROP_PATH}/wishbone_cons.sv

# 连接 CSR PA 实例
analyze -sv09 jasper_CSR_PA_inst.sv

elaborate -top uart_top

# 加载寄存器映射表
check_csr -load $CSR_MAP -instance i_jasper_csr.jasper_csr_checker0 -auto_hr_info

clock wb_clk_i
reset wb_rst_i -non_resettable_regs 0

# Task 机制：建立总线约束任务并链接到 CSR 任务
task -create IF_CONS -source_task <embedded> -copy_assumes
task -set CSR
task -link IF_CONS

set_engine_mode {Ht N}
set_prove_time_limit 30s

check_csr -prove

clear -all
set_visualize_auto_check_props on

# 加载 XML 格式的架构模型
check_arch -load L1L2.xml

set_prove_per_property_time_limit 10s
set_prove_time_limit 30s

check_arch -prove
report

# 查看 L1 比较失败的反例
visualize -violation -property {<embedded>::L1L2.AST_table_L1_CMP_full} -new_window

# 分析 RTL + SVA
analyze -verilog ${RTL_PATH}/design/arbiter.v
analyze -verilog ${RTL_PATH}/design/bridge.v
# ... 其他 RTL 和 SVA 文件

elaborate -bbox_a 1024     # 黑盒阈值 1024 门
clock clk
reset {rstN == 1'b0}
waveform -reset rstN==0

# 提取关注点（POI = Points of Interest）
scope -extract all         # 自动提取所有信号
scope -add ready0 ready1 ready2 ready3   # 手动添加 ready 信号
scope -add eg.cur_state eg.read_write brdg.current_read_write  # 添加状态信号

# ---- 第一轮 VCD 扫描 ----
check_bps -scan -trace -vcd ${VCD_PATH}/vcd/e154.vcd
database -set_baseline -bps    # 设置基线

# ---- 第二、三轮扫描 ----
check_bps -scan -trace -vcd ${VCD_PATH}/vcd/e155.vcd
check_bps -scan -trace -vcd ${VCD_PATH}/vcd/e156.vcd

# 导出 cover 类候选到 FPV 证明
check_bps -export -class unclassified -type cover
set_current_gui fpv
prove -task <synthesized> -time_limit 30s

# 导出为多种格式
export -bps -to_sva [get_proj_dir]/example.sva \
    -to_tcl [get_proj_dir]/connect_sva.tcl \
    -type coverage_hole -type exercised_cover \
    -class certified -class unclassified
export -bps -to_html [get_proj_dir]/example.htm \
    -type coverage_hole -type exercised_cover \
    -class certified -class unclassified

check_fsv -init
source fsv_utils.tcl             # 加载 fsv_summary 等工具过程

analyze -sv ${RTL_PATH}/rtl/can_counter.v \
            ${RTL_PATH}/rtl/coin_counter.v \
            ${RTL_PATH}/rtl/drink_machine.sv \
            ${RTL_PATH}/rtl/drink_machine_top.v \
            ${RTL_PATH}/rtl/test_drink.v \
            ${RTL_PATH}/rtl_safe/drink_machine_top_safe.v

elaborate
clock -infer                      # 自动推断时钟
reset top.reset

set_fsv_clock_cycle_time 200ns    # 时钟周期 200ns（5MHz）
set_fsv_engine_mode {Bm Ht Hp Tri}
set_fsv_regs_mapping_optimization on
set_fsv_strobe_optimization on

# ---- 故障注入配置 ----
# SA0+SA1（stuck-at-0/1）：所有信号
check_fsv -fault -add [get_design_info -instance top -list signal -silent] -type SA0+SA1
# SEU（单粒子翻转）：所有 flop，全时段
check_fsv -fault -add [get_design_info -instance top -list flop -silent] -type SEU -time_window 0:$
# SET（单粒子瞬态）：所有信号，500ns 建立保持时间
check_fsv -fault -add [get_design_info -instance top -list signal -silent] -type SET -time_window 0:$ -set_hold_time 500ns
# 移除 checker 输出信号（*_failure）不作为故障目标
check_fsv -fault -remove [check_fsv -fault -list -node {.+_failure} -regexp -silent]

# ---- Strobe 配置（观察点）----
check_fsv -strobe -add [get_design_info -instance top -list output -include_hier_path -silent] -functional
check_fsv -strobe -add [check_fsv -strobe -list -node {*_failure} -silent] -checker

# ---- 三阶段分析 ----
check_fsv -structural          # 结构分析：快速排除不可达故障
check_fsv -generate            # 生成形式验证属性
check_fsv -prove -time_limit 1m  # 证明

# ---- 报告 ----
check_fsv -report -class dangerous
check_fsv -report -force -text ~/fsv.rpt
fsv_summary                     # 按 A/P/D 分类汇总

analyze -sv -f $RTL_PATH/hash.f
analyze -sv $RTL_PATH/sva/hash_checker.sv

elaborate -top hash
clock clk
reset ~rst_n

# stopat：将密钥信号设为自由变量（不受设计逻辑驱动）
stopat otp_key custom_key
stopat hash_core.out_hash

# SPV 属性 1：非安全状态下 otp_key 不能流向 s_rdata
check_spv -create \
          -from otp_key \
          -to s_rdata \
          -to_precond {~s_secure}

# SPV 属性 2：非安全读操作时 custom_key 不能流向 s_rdata
check_spv -create \
          -from custom_key \
          -to s_rdata \
          -to_precond {s_req && ~s_write && s_ack && ~s_secure}

check_spv -prove

# 失败时查看泄露路径波形
visualize -violation -property <embedded>::spv_prop:1 -new_window

# 自动设置分析（从目录结构推断 RTL 文件和顶层）
auto_setup -sv -path ../designs/reference_design/verilog_sva \
  -top_file ../designs/reference_design/verilog_sva/source/design/top.v

# 结构分析并设为基线
database -structural_analysis -batch
database -structural_analysis -set_baseline

# 可视化源码行行为
visualize {arb.shift="1000"}
visualize -save_recipe {Visualizing arbiter shift} -task <embedded> ...

# 捕获传输开始事件作为 Behavior
cover -name Transfer_Start {(arb.trans_started == 0) ##1 (arb.trans_started == 1)} ...

# 探索 FSM
visualize -explore eg.cur_state
visualize -save_recipe "Exploring main FSM" ...

# 行为分析并设为基线，保存数据库
database -behavioral_analysis -set_baseline
save -jdb [get_proj_dir]/example.jdb -capture_setup

# 恢复数据库
restore -jdb [get_proj_dir]/example.jdb

# 结构分析 → 导出结构差异报告
database -structural_analysis -batch
database -export_report "Structural Differences" [get_proj_dir]/sa.csv

# 行为分析 → 导出行为差异报告
database -behavioral_analysis -include_behaviors -batch
database -export_report "Behavioral Differences" [get_proj_dir]/ba.csv

# 对比行为变化（replot）
visualize -property {<embedded>::behavior:0}
visualize -replot
visualize -save_recipe {Another recipe} ...

check_superlint -init

# 分析 RTL
analyze -verilog ${RTL_PATH}/arbiter.v ${RTL_PATH}/bridge.v ...
elaborate -bbox_a 1024

clock clk
reset {rstN == 1'b0}

# 提取检查项（Lint + Auto Formal）
check_superlint -extract

# 添加设计约束（FIFO 指针范围约束）
assume {brdg.wr_ptr < 4'b1111}
assume {brdg.rd_ptr < 4'b1111}

# Task 机制：将约束链接到 Superlint 任务
task -create design_assumptions -copy_assumes -copy_related_covers -source_task <embedded>
task -link design_assumptions -to <SL_AUTO_FORMAL_ARITHMETIC_OVERFLOW>

set_max_trace_length 50
check_superlint -prove -task {<SL_*}

analyze -verilog {./design/fifo.v}
analyze -verilog -req ./jasper_req/FIFO_datapath.v

elaborate -bbox_a 512

# 连接 PA 端口到 DUT
connect FIFO_datapath req \
  -connect clk       clk \
  -connect rstN      hresetn \
  -connect valid_in  fifo_write \
  -connect valid_out fifo_read \
  -connect data_in   fifo_datain \
  -connect data_out  fifo_dataout

clock clk
reset {~hresetn}
assume -env {~fifo_reset}

task -set {<req.dp_PACKET_SANITY>}
assume {(~fifo_empty_s && ~fifo_read) == 1'b0}

set_engine_mode engineG
prove -all

# ... 同上 ...

# 防止 overflow 和 underflow 条件
assume -env {(fifo_empty && fifo_read) == 1'b0}
assume -env {(fifo_full && fifo_write) == 1'b0}

set_engine_mode engineG
prove -all

analyze -verilog {./design/universal_asynchronous_receiver.v}
analyze -verilog -req {./jasper_req/datapath.v}

elaborate -bbox false -top {uar}

connect datapath dp \
  -connect {clk}       {clk}  \
  -connect {rstN}      {~gl_reset}  \
  -connect {tx_error}  {dError}  \
  -connect {valid_in}  {count8}  \
  -connect {data_in}   {dIn}  \
  -connect {valid_out} {dReady}  \
  -connect {data_out}  {dOut}

clock {clk}
reset {gl_reset}

assert -disable <dp.dp_PACKET_INTEGRITY>::sanity_reset_activated
assert -disable <dp.dp_PACKET_INTEGRITY>::sanity_reset_toggle_once

set_engine_mode engineG
prove -all

# 加载 IP-XACT 并自动设置设计
ipxact -load ipxact/top.xml -lib ipxact -setup design

# 检查 IP-XACT 声明与 RTL 的一致性（端口/参数/实例）
ipxact -check_rtl_consistency

# 从 IP-XACT 生成连接映射表
ipxact -generate_connectivity_map [get_proj_dir]/conn.csv orpsoc_top
check_conn -load [get_proj_dir]/conn.csv

clock -analyze
reset -analyze
clock clk_pad_i
reset ~rst_n_pad_i

check_conn -prove

analyze -sv jasper_bind_csr.sv
ipxact -load ipxact/or1k.xml -lib ipxact -setup design

# 直接从 IP-XACT 加载 CSR 定义
check_csr -load_ipxact -instance jasper_csr_checker0

clock clk_i
reset rst_i
check_csr -prove

# jg.tcl — JasperGold 端形式验证
check_unr -setup
clock -none
reset -none

check_unr -prove -prove_opts { -verbosity 4}
check_unr -list -type unreachable    # 列出不可达覆盖项
database -export_unicov              # 导出 unicov 格式

report -summary
run
exit