附录 BTcl 命令速查表

通用命令（所有 App）

下表命令对所有 App 通用，是每个脚本的骨架：分析 → 展开 → 声明时钟复位 → 证明 → 报告。

命令	用途
`clear -all`	清空当前会话的设计与设置，脚本开头常用
`analyze -verilog <files>`	分析 Verilog 源文件
`analyze -vhdl <files>`	分析 VHDL 源文件
`analyze -sv <files>`	分析 SystemVerilog 源文件
`analyze -sva <files>`	分析 SVA 属性文件
`elaborate -top <module>`	以指定模块为顶层展开设计
`elaborate -bbox_m <module>`	展开时把指定模块黑盒化
`elaborate -bbox_a <n>`	展开时按面积阈值自动黑盒化
`blackbox_assistant -config -connectivity_map <csv>`	按连接映射自动计算并黑盒化验证不需要的模块/实例（须在 `elaborate` 之前）
`clock <signal>`	声明全局时钟
`clock -rate {<ports>} <clock>`	把输入端口关联到指定时钟域
`clock -infer` / `clock -analyze`	自动推断 / 自动检测时钟
`reset <signal>`	声明全局复位（低有效写作 `reset ~rstN`）
`stopat <signal>`	切断信号的驱动逻辑，令其成为自由变量
`assume <expr> -env`	添加环境约束
`assert` / `cover`	添加断言 / 覆盖点，配合 `-disable`、`-enable` 选择性启停
`task -create <name> -source_task <t> -copy_assumes`	创建任务并从源任务拷贝约束
`task -set <name>` / `task -link <name>`	切换当前任务 / 链接任务
`prove -all`	证明所有属性
`prove -property <name>`	证明指定属性
`get_design_info`	获取设计复杂度信息
`get_install_dir` / `get_proj_dir`	取安装目录 / 工程目录路径
`set_max_trace_length <n>`	设置最大 trace 长度
`set_engine_mode {K I N B L}`	设置引擎模式（花括号内为引擎字母组合）
`set_prove_time_limit <time>`	设置整体证明时间限制
`set_prove_per_property_time_limit <t>`	设置单属性证明时间限制
`visualize -violation -property <prop> -new_window`	打开反例波形窗口
`save -jdb <file>` / `restore -jdb <file>`	保存 / 恢复数据库
`report`	报告证明结果

关于引擎字母：set_engine_mode 接受的是引擎字母（如 K、I、N、B、L、Ht、Hp、Bm、Tri）。各引擎的适用场景见《Engine Selection Guide》，例如 K 专门找有界证明、N 顺序证明并能给出完整证明、 B 只能给反例或有界证明而永不给出穷尽证明。

FPV App

命令	用途
`abstract -counter <reg>`	对计数器做抽象
`abstract -init_value <regs>`	对寄存器初值做抽象
`abstract -reset_value`	对复位值做抽象

FPV 的主体流程直接用上表的通用命令（analyze → elaborate → clock/reset → prove -all → report），没有独立的 check_fpv 命令。

CDC App

命令	用途
`check_cdc -clock_domain -find`	查找时钟域
`check_cdc -clock_domain -join <a> -into <b>`	合并时钟域（如分频域并入主域）
`check_cdc -pair -find`	查找 CDC 对（跨域路径）
`check_cdc -scheme -find`	查找同步器方案并跑结构检查
`check_cdc -scheme -add FIFO -map {...}`	添加用户定义的同步器方案
`check_cdc -group -find`	查找收敛点
`check_cdc -signal_config -add_constant {{<sig> <val>}}`	把信号配置为常量
`check_cdc -check -severity {fatal {no_scheme}}`	设置规则严重级别
`check_cdc -filter -add ...`	创建过滤器（供豁免引用）
`check_cdc -waiver -add -filter <id> -comment {...}`	添加豁免
`check_cdc -waiver -generate` / `-prove`	生成并验证豁免条件
`check_cdc -protocol_check -generate` / `-prove`	协议检查（功能检查）的生成与证明
`check_cdc -metastability -inject` / `-prove`	亚稳态注入（MSI）与证明
`check_cdc -reset -find`	识别复位同步器（RDC 结构分析的入口）。注意复位同步器只能用这条命令找，不能像其他同步器那样用 `check_cdc -scheme -find`
`check_cdc -report <type> -file <f>`	生成报告（pairs / violations / domains / signoff 等）

Superlint

命令	用途
`check_superlint -init`	初始化 Superlint App
`check_superlint -extract`	提取检查项
`check_superlint -prove -task {<SL_*}`	形式证明提取出的属性

X-Prop

命令	用途
`check_xprop -init_control <0\|1>`	启用 X 初始化控制模式
`check_xprop -create -outputs -no_bit_blast`	创建输出端口的 X 传播属性
`check_xprop -create -control`	创建控制信号的 X 传播属性
`check_xprop -create -clocks_and_resets`	创建时钟/复位的 X 传播属性
`check_xprop -prove -no_decompose -all`	证明所有 X-Prop 属性

CSR

命令	用途
`check_csr -load <csv> -instance <inst> -auto_hr_info`	加载寄存器映射表并指定 CSR PA 实例
`check_csr -load_ipxact -instance <inst>`	直接从 IP-XACT 加载 CSR 定义
`check_csr -prove`	证明 CSR 属性

UNR

命令	用途
`check_unr -init`	初始化 UNR
`check_unr -setup -coverage {block expr toggle fsm} -covdb <db>`	建立 UNR 环境并指定仿真覆盖率数据库
`check_unr -prove`	运行不可达性证明
`check_unr -list -type unreachable`	列出不可达覆盖项
`check_unr -enable_property` / `-disable_property`	启用 / 禁用属性
`database -export_unicov`	导出 unicov 格式覆盖率结果

SEC

命令	用途
`check_sec -setup -spec_top <m> -imp_top <m> ...`	设置 spec/imp 两侧的顶层、分析与展开选项
`check_sec -interface`	检查 spec 与 imp 之间的端口映射问题
`check_sec -map -spec {<sig>} -imp {<sig>}`	手动映射未自动匹配的信号
`check_sec -auto_map_reset_x_values on`	自动映射未初始化寄存器的 X 值
`check_sec -gen`	生成等价性验证环境
`check_sec -prove`	证明映射点对的等价性
`check_sec -signoff`	运行 signoff（可加 `-waive_category` 豁免类别）

SEC 的两侧在命令中一律称 spec（规格侧）和 imp（实现侧），对应 -spec_top / -imp_top。

Connectivity

命令	用途
`check_conn -load <csv>`	加载连接映射表
`check_conn -reverse -src {<insts>} -load`	反向提取连接关系并立即加载
`check_conn -validate`	COI 验证
`check_conn -generate_toggle_checks {}`	生成翻转检查
`check_conn -prove`	证明连接性属性

Coverage

命令	用途
`check_cov -init -model {branch statement expression toggle functional}`	初始化覆盖率模型（必须在 elaborate 之前）
`check_cov -measure -no_auto`	生成覆盖率指标

LPV

命令	用途
`check_lpv -load_upf <file>`	加载 UPF 电源意图文件
`check_lpv -generate_power_design`	自动生成电源感知 RTL
`check_lpv -verify <check>`	执行结构检查（如 `check_iso_connections`）
`check_lpv -create <assert>`	创建功能检查断言（如 `assert_iso_up_before`）

FSV

命令	用途
`check_fsv -init`	初始化 FSV App
`check_fsv -fault -add <list> -type SA0+SA1`	添加故障注入目标
`check_fsv -fault -remove <list>`	移除故障目标
`check_fsv -strobe -add <list> -functional` / `-checker`	添加功能 / 检查器观察点
`check_fsv -structural`	结构分析
`check_fsv -generate`	生成 FSV 属性
`check_fsv -prove -time_limit <t>`	证明 FSV 属性
`check_fsv -report -class dangerous`	按分类输出报告
`set_fsv_clock_cycle_time <t>`	设置 FSV 时钟周期
`set_fsv_engine_mode {Bm Ht Hp Tri}`	设置 FSV 引擎组合

SPV

命令	用途
`check_spv -create -from <src> -to <dst> -to_precond {<expr>}`	创建安全路径属性
`check_spv -prove`	证明 SPV 属性

ARCH / BPS / IP-XACT

命令	用途
`check_arch -load <xml>`	加载 XML 架构模型
`check_arch -prove`	证明架构模型属性
`check_bps -scan -trace -vcd <file>`	扫描 VCD 波形并综合属性候选
`check_bps -export -class <c> -type <t>`	导出属性候选到 FPV 证明
`export -bps -to_sva <f> -to_tcl <f>`	导出为 SVA / Tcl 连接脚本
`ipxact -load <xml> -lib <dir> -setup design`	加载 IP-XACT 并自动搭建设计
`ipxact -check_rtl_consistency`	检查 IP-XACT 声明与 RTL 的一致性
`ipxact -generate_connectivity_map <csv> <top>`	从 IP-XACT 生成连接映射表

ProofGrid

命令	用途
`set_proofgrid_mode (local \| shell \| lsf \| oge \| nc \| cluster)`	指定证明作业在哪种 grid 上运行。`local` 为默认值（在当前会话所在机器上跑）；`shell` 需配合 `set_proofgrid_shell`。注意没有 `on` 这个取值
`set_proofgrid_max_jobs <n>`	设置最大并行任务数
`set_proofgrid_max_local_jobs <n>`	设置本地最大并行任务数

来源文档

jaspergold_command_reference.pdf