第二章环境搭建

分析设计（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 命令解析设计层次、解析参数、构建证明数据库：

# 基本用法
elaborate -top top_module

# 带参数
elaborate -top top_module -parameter WIDTH=32

# 重置设计（清除之前的 elaborate 结果）
elaborate -reset

指定全局时钟

# 单时钟
clock clk

# 多时钟（gated clock）
clock clk -module submodule
clock clk2

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

指定全局复位

# 高有效复位
reset rst

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

# 指定复位周期数
reset ~rstN -n 2

复位信号定义了设计的初始状态。JasperGold 会在复位期间不检查断言，复位结束后开始证明。

证明参数设置

基本引擎设置

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

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

# 选择引擎模式
set_engine_mode {K I N}
# K = K-Induction, I = Interpolation, N = Bmc

高级引擎设置

# 为特定属性设置引擎
set_prove_per_property_time_limit 30s

# 启用/禁用特定引擎
set_engine_mode {B L}  # B=Bmc, L=Pdr

# 设置多线程
set_prove_threads 4

配置捕获与复用

完成环境配置后，可以将设置保存为 Tcl 脚本，供后续复用：

# 在 GUI 中：File → Save Setup Script
# 或使用命令
save_setup_script setup.tcl

多 Session 管理

JasperGold 支持在同一个数据库中创建多个 Session（会话），每个 Session 可以有不同的证明配置：

# 创建新 Session
create_session session2

# 启动新 Session（带已细化的设计）
launch_session -elaborated

界面截图

时钟复位建模原则

时钟选择原则

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

• 声明所有时钟：每个时钟域都要用 clock 命令声明，遗漏时钟会导致该域的 flop 不被正确识别
• 多时钟设计：FPV 中可以声明多个时钟，工具使用 clock -rate 关联信号到时钟域（CDC App 中更系统化）
• 生成时钟：分频/倍频时钟也需要声明，使用 clock clk_div 2 1 表示分频关系
• 门控时钟：被门控的时钟在形式验证中通常不需要特殊处理，工具自动处理；但要确保时钟声明在门控逻辑之前

复位建模

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

• 同步复位：reset rst（高有效）或 reset ~rstN（低有效），工具自动在复位期间施加约束
• 异步复位：同上声明，工具处理异步复位的解除同步
• 复位周期：默认复位持续 1 个周期，工具自动驱动复位信号
• 未初始化寄存器：复位后未被显式初始化的寄存器，工具默认设为 X 值。可使用 reset -non_resettable_regs 0 控制此行为

黑盒策略

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

• 什么时候黑盒：
  • 模块内部逻辑与当前验证目标无关（如验证仲裁器时黑盒掉 PLL）
  • 模块过于复杂导致证明超时
  • 模块是第三方 IP，没有 RTL 源码
  • 存储器/SRAM/FIFO 通常黑盒化（用替代模型或约束）
• 黑盒错了会怎样：
  • 黑盒不足（该黑没黑）→ 复杂度太高，引擎超时
  • 黑盒过度（不该黑的黑了）→ 关键逻辑被替换为自由变量，可能产生假反例或假 proven
• 黑盒命令：
  • elaborate -bbox_m <module>：黑盒指定模块的所有实例
  • elaborate -bbox_a <gate_count>：自动黑盒超过指定门数的模块
  • blackbox_assistant：工具自动推荐最优黑盒策略