第二章环境搭建

分析设计（Analyze）

analyze 命令读取并编译 HDL 源文件和属性文件：

# 分析 Verilog 文件
analyze -verilog rtl_file1.v rtl_file2.v

# 分析 VHDL 文件
analyze -vhdl rtl_file1.vhd rtl_file2.vhd

# 分析 SystemVerilog（含 SVA）
analyze -sv {rtl_file.sv}
analyze -sva {bindings.sva}

# 分析 PSL 属性
analyze -psl {properties.psl}

# 混合语言：Verilog + VHDL + SVA 可在同一项目中使用

细化设计（Elaborate）

elaborate 才是真正综合并读入网表的一步，同时为已经 analyze 过的文件提取验证任务：

# 基本用法
elaborate -top top_module

# 带参数：参数名与参数值之间用空格分隔，该开关可重复多次
elaborate -top top_module -parameter WIDTH 32

# 清除 elaborate 结果
elaborate -clear

指定全局时钟

# 单时钟
clock clk

# 多时钟：分别声明即可
clock clk
clock clk2

# 声明派生（分频）时钟：clock <基准时钟> <派生时钟列表> [factor [phase]]
# factor = 基准时钟频率与派生时钟频率之比，phase = 相对相位
clock clk clk_div 2 1

时钟信号是同步设计的基础。JasperGold 使用时钟来确定采样边沿，所有断言都在时钟边沿评估。

指定全局复位

# 高有效复位
reset rst

# 低有效复位（使用 ~ 或 !）
reset ~rstN

# 复位分析默认运行到寄存器值不再变化、或达到 100 次迭代为止
# 用 -max_iterations 修改这个默认值
reset -expression ~rstN -max_iterations 50

复位信号定义了设计的初始状态。reset 指定的是一组引脚：工具复位设计时把它们置为有效，正式做形式验证时再解除。

证明参数设置

基本引擎设置

# 设置最大 trace 长度（时间边界）
set_max_trace_length 20

# 设置证明时间限制
set_prove_time_limit 60s

# 选择引擎模式
set_engine_mode {K I N}
# K：专门用于找有界证明，只搜索 trace，一般不会给出完整证明
# I：一次处理一个属性，从 COI 中迭代地引入逻辑，尽量减少证明所需的逻辑量
# N：顺序地证明属性，能给出完整证明，不像 B/J/K/L 那样局限于找 trace

高级引擎设置

# 限制每个属性上花费的时间
set_prove_per_property_time_limit 30s

# 设置每个引擎最多使用的线程数（默认 1）
set_engine_threads 5

# 换一组偏"找 bug"的引擎
set_engine_mode {B L}
# B：不并发处理属性，永远不会给出穷尽证明，只能给出反例或有界证明
# L：bug-hunting 引擎，在状态空间中做深度搜索，
#    用于找反例、或命中常规形式引擎难以到达的覆盖点

配置复用：把环境写成 Tcl 脚本

环境配置的复用方式是直接把命令写成 Tcl 脚本文件——官方示例工程本身就是这么组织的（见 example_jaspergold_apps/FPV/*.tcl）。写好之后用 include 命令读入并执行：

# 读取并执行一个 Tcl / JasperGold 命令脚本
include setup.tcl

设计的保存与恢复

已分析（analyze）的结果可以保存下来供后续复用，避免每次重新编译：

# 保存 analyze 结果
analyze -save -dir <dir_name>

# 恢复 analyze 结果
analyze -restore -dir <dir_name>

界面截图

时钟复位建模原则

时钟选择原则

时钟声明告诉形式引擎设计的同步边界，直接影响状态空间的构建。以下是关键原则：

• 声明所有时钟：每个时钟都要用 clock 命令声明。也可以用 clock -infer 显式执行一次时钟推断，让工具声明并返回推断出的所有时钟
• 控制输入的变化速率：clock -rate <input_tcl_list> <clock_signal> 指定这些边界输入按该时钟信号的速率变化。-rate 的时钟可以是设计中的任意信号，甚至是一个被驱动的、此前没有声明为 clock 的信号；用 -default 则对所有未驱动信号统一定速
• 生成时钟：派生时钟用 clock <基准时钟> <派生时钟列表> [factor [phase]] 声明，例如 clock clk clk_div 2 1——注意基准时钟不能省略
• 时钟的三个类别：文档把时钟分为——Simple clocks（输入、environment hard stopat）、Gated clocks（连接到 AND 或树状结构的 simple clock）、Complex clocks（不属于前两类的，例如分频器和 clock-mux）
• 门控时钟：门控时钟的输入同样需要有时钟声明；"某个门控时钟的输入没有时钟声明"是工具会报出来的错误之一

复位建模

复位建模决定了形式验证的初始状态：

• 同步复位：reset rst（高有效）或 reset ~rstN（低有效），工具自动在复位期间施加约束
• 异步复位：同上声明，工具处理异步复位的解除同步
• 复位分析的迭代次数：复位分析会一直运行到寄存器值不再变化、或达到 100 次迭代为止，而不是固定跑一个周期。用 -max_iterations <N> 改这个默认值，用 -clock 指定按哪个时钟计迭代次数
• 未初始化寄存器：未初始化寄存器（可综合的变量数据类型，即 reg、integer、logic）的默认值是 X，因此可能成为 X 的来源——在 X-Propagation 检查中，工具默认就把未初始化寄存器当作 X 源
• 不可复位的寄存器：用 reset -non_resettable_regs <value> 把不可复位的寄存器初始化为指定的常数（例如 0）
• 从快照恢复初始状态：reset -init_state <file_name> 可以用一个复位快照文件来设定初始状态

黑盒策略

黑盒（Blackbox）将模块替换为接口完全自由的壳，是控制复杂度的重要手段：

• 什么时候黑盒：
  • 模块内部逻辑与当前验证目标无关（如验证仲裁器时黑盒掉 PLL）
  • 模块过于复杂导致证明超时
  • 模块是第三方 IP，没有 RTL 源码
  • 存储器/SRAM/FIFO 通常黑盒化（用替代模型或约束）
• 黑盒错了会怎样：
  • 黑盒不足（该黑没黑）→ 复杂度太高，引擎超时
  • 黑盒过度（不该黑的黑了）→ 关键逻辑被替换为自由变量，可能产生假反例或假 proven
• 黑盒命令：
  • elaborate -bbox_m <string>：按模块名黑盒（-no_bbox_m 排除，且 -no_bbox_m 优先级高于 -bbox_m）
  • elaborate -bbox_i <string>：按实例黑盒（对应的排除开关是 -no_bbox_i）
  • elaborate -bbox_a <value>：黑盒数组——当数组的位宽超过指定值时将其黑盒。工具默认把数组 bit-blast 到 2048 位，超过则黑盒；这个开关用于设定不同的阈值。注意它针对的是数组尺寸，不是模块门数
  • elaborate -bbox (0 | 1)：控制缺失模块的处理——0 表示缺失模块报错（默认），1 表示自动黑盒。analyze 也支持这个开关，有时在流程更早的阶段用它更合适
  • blackbox_assistant -config -connectivity_map <csv>：由连接性映射表驱动的自动黑盒——配置之后，后续的 elaborate 会自动触发它，把所有不在"验证这些连接所需路径"上的实例黑盒掉。用 -export 把结果导出成兼容 elaborate -f 的文件以便复用，用 blackbox_assistant -clear 清除。它需要你提供连接性映射表，并不是一个通用的"最优黑盒策略推荐器"