附录 BTcl 命令速查表
通用命令（所有 App）
| 命令 | 用途 |
|---|---|
analyze -verilog <files> | 分析 Verilog 源文件 |
analyze -vhdl <files> | 分析 VHDL 源文件 |
analyze -sva <files> | 分析 SVA 属性文件 |
elaborate -top <module> | 细化设计 |
clock <signal> | 声明全局时钟 |
reset <signal> | 声明全局复位 |
prove -all | 证明所有属性 |
prove -property <name> | 证明指定属性 |
report | 报告证明结果 |
get_design_info | 获取设计复杂度信息 |
set_max_trace_length <n> | 设置最大 trace 长度 |
set_engine_mode {K I N B L} | 设置引擎模式 |
set_prove_time_limit <time> | 设置证明时间限制 |
blackbox -module <name> | 将模块设为黑盒 |
save_setup_script <file> | 保存配置脚本 |
FPV App
| 命令 | 用途 |
|---|---|
abstract -signal <sig> | 抽象信号 |
create_session <name> | 创建新 Session |
set_prove_per_property_time_limit <t> | 单属性时间限制 |
CDC App
| 命令 | 用途 |
|---|---|
check_cdc -structural | CDC 结构分析 |
check_cdc -protocol -formal | CDC 协议检查（Formal） |
check_cdc -msi -formal | 亚稳态注入分析 |
cdc_synchronizer -module <m> ... | 定义用户同步器 |
waive_cdc -violation <id> | 豁免 CDC 违规 |
check_rdc -structural | RDC 结构分析 |
Superlint
| 命令 | 用途 |
|---|---|
run_superlint -extract | 提取 Lint 检查 |
run_superlint -prove | 形式证明 Lint 检查 |
set_superlint_check -rule <r> -enable | 启用规则 |
export_superlint_to_sva -output <f> | 导出为 SVA |
X-Prop
| 命令 | 用途 |
|---|---|
check_xprop | 运行 X-Prop 检查 |
CSR
| 命令 | 用途 |
|---|---|
read_csr_csv <file> | 读取 CSR CSV 配置 |
generate_csr_extension_template -output <f> | 生成扩展文件模板 |
UNR
| 命令 | 用途 |
|---|---|
read_coverage_db -sim <file> | 读取仿真覆盖率数据库 |
check_unr -type <types> | 运行 UNR 分析 |
SEC
| 命令 | 用途 |
|---|---|
check_interface | 检查 Golden/Revised 接口 |
add_mapping_alias -golden <p> -revised <p> | 添加映射别名 |
set_sec_strategy -basic|-bug_hunting | 设置 SEC 策略 |
ProofGrid
| 命令 | 用途 |
|---|---|
set_proofgrid_mode on | 启用 ProofGrid |
set_proofgrid_max_jobs <n> | 设置最大并行任务数 |
set_proofgrid_server_type <type> | 设置服务器类型（lsf/local） |
来源文档
jaspergold_command_reference.pdf