前一阵子我验证一个 64×64 Booth 乘法器RTL 刚搭完第一版参考模型还停留在 C 语言里。常规做法是先写一大批断言再拿 C 模型跑随机对比测试但流水线乘法器的周期对齐和符号扩展细节很容易把人绕晕。后来我把 JasperGold 的 C2RTL 流程用上了工具直接拿 C 参考模型和 RTL 做形式化比对省掉了大量手写断言。这篇把整个过程从头捋一遍包含实际跑通的 TCL 脚本、环境组织方式以及几个我踩过之后觉得值得写下来的坑。无论你是刚开始碰 formality 验证还是已经在用 JasperGold 做数据通路 IP 检查这套流程都可以直接拿去当模板改。1. 为什么我坚持用 C2RTL 验证 Booth 乘法器1.1 Booth 乘法器的 RTL 验证痛点很多人一听说验证乘法器第一反应都是“不就是一个乘法器吗给一组输入比一下乘积就行”。真做起来才发现Booth 乘法器内部和普通组合逻辑乘法器差异非常大。以 radix-4 Booth 编码为例每三位一组产生一个部分积编码输出是 0、A、2A、-A、-2A 这五种取值原本要生成 64 个部分积的 64×64 乘法器可以压缩到 33 个左右。部分积数量减少了减法和符号扩展逻辑却大大增加了。问题恰恰出在符号扩展上。-A 和 -2A 在补码里需要取反加一加一的位置要落到部分积的最低位不同部分积的符号扩展位还会互相重叠。很多第一版 RTL 会在这里出错某个部分的符号位多打了半拍或者拼接位数差了 1 位。这类 bug 在仿真里不是完全测不出来而是问题长得太像“算法本来就这样”需要很强的 debug 经验才会去检查部分积里的具体式子而不是盯着最终结果看。另一个痛点是多拍流水。我遇到的这个 64×64 乘法器是四级流水线start_i 拉高之后中间经过编码、部分积求和、压缩树、最终加法四个阶段后才输出 valid_o。传统形式验证的写法通常是在 valid_o 拉高的那一拍把 p_o 和前级寄存器里的 a_i、b_i 拿出来做乘积比较。这要求断言模型精确复刻流水的周期关系一旦流水线深度调整或者中间插入一条旁路逻辑所有断言都要跟着改。这种维护成本我实在不想再背了。于是 C2RTL 成了很自然的选择参考模型在 C 里C 关心“什么时候输入什么时候输出”RTL 按自己的周期实现两边通过握手信号对齐中间流水过程交给形式化工具去证明而不是交给断言去锁周期。这才是这个流程最容易体现价值的地方。1.2 C2RTL 与传统断言式验证的本质区别我并不否定断言式验证反而觉得 C2RTL 和 SVA 是互补的但在“算法匹配”这件事上C2RTL 有天然优势。SVA 想要验证“乘积正确”必须先把“乘积正确”这四个字翻译成可计算表达式。对加法器来说很简单product a * b 不算难可换成 Booth 乘法器spec 级别的行为是数学上的乘法a * b 必须由 SystemVerilog 自己实现。如果我在断言里写 *编译出来就是一个乘法器模型这和 RTL 实现是完全无关的参考逻辑但会遇到位宽、符号扩展、仿真工具和形式化工具对乘号处理差异的麻烦。C2RTL 则把参考行为的翻译从手写断言变成了参考 C 函数的自动建模。C 模型里直接写(int128_t)a * (int128_t)b这是标准算术语义中间没有 SV 赋值和位宽的坑。工具把这段 C 语言的语义读进形式模型再同 RTL 在握手层做等价。证明目标的数量远少于人工断言体系推导链路的可信度反而更高。需要特别澄清一点C2RTL 不是把 C 翻译成可综合 RTL然后做“综合逻辑同 C 行为”的等价性检查这样做既不可维护又没法对付多周期。C2RTL 是在协议层抽象角度读取 C 行为把 C 里的输入输出关系转成形式化的契约最终由 prove 引擎检查“对任意满足契约的输入序列RTL 产生的结果都等于 C 的输出”。这也是为什么它对 C 模型的风格有要求这部分我放到第 2 节专门讲。1.3 什么场景下我会推荐用 C2RTL这个流程并不是万能的有些场景用了反而拖慢进度。我把自己的判断标准整理成了一个表场景建议原因单周期组合乘法器用 SVA 即可C2RTL 引入编译和映射成本收益低多周期流水乘法器强烈推荐 C2RTL周期对齐交给工具不再靠手写断言锁拍C 参考模型还没写完先别上 C2RTLC 模型自己不稳定时报错大半出在参考上RTL 还在频繁改流水结构可以提前部署 C2RTL映射只依赖握手信号不依赖内部流水细节还要同时查内部标志位或中断两者结合C2RTL 管数据面SVA 管控制面各干各的举一个实际例子。项目做到一半设计组把流水线从四级改成了五级在压缩树后面多插了一级寄存器。放在传统断言流程里这等于要把所有和 valid_o 对齐的乘积比较断言全部推开一拍。但在 C2RTL 里只需要把 C 模型里的延迟参数从 4 改成 5甚至可以直接写成可配置变量。整个改动量就只有一行。另外工具选型也要考虑扩展性。Booth 乘法器往上走可能就是带符号、带饱和、带舍入的 MAC 单元再往上走还有浮点乘法。C2RTL 一旦把“C 描述算法语义RTL 描述电路实现”这个框架搭好后续新增功能基本就是扩 C 函数和扩接口映射不需要推翻重来。2. 环境准备与 C 参考模型建模约束2.1 目录与文件组织C2RTL 验证环境和普通 JasperGold 工程差别不大但多了一个 C 参考模型的目录以及对应的编译脚本。我习惯按下面这种方式组织booth_mul_c2rtl/ ├── rtl/ │ ├── booth_mul_top.sv │ ├── booth_enc.sv │ └── booth_pp.sv ├── c_ref/ │ ├── booth_mul_ref.c │ └── booth_mul_ref.h ├── scripts/ │ └── run_c2rtl.tcl └── work/work 目录放 JasperGold 工程生成的文件每次跑完如果不干净直接删掉重建。scripts 目录只放 TCL 和 Makefile。C 模型单独放一个目录是因为它最好能独立编译成可执行程序先在自己的 testbench 里跑一遍确认参考行为本身没问题再交到 JasperGold 手里。这一步很多人省掉后果是后面分不清 bug 是在 C 模型里还是在 RTL 里。RTL 文件这里我特意列了 booth_enc 和 booth_pp因为 Booth 乘法器通常不会只有一个顶层文件。导入设计时要把所有相关模块都读进去set_top 指到 booth_mul_top 即可。2.2 让 C 参考模型能映射到 RTL 的四条硬规则C2RTL 对 C 代码有一定约束不满足的话工具要么直接报错要么给出完全没法收敛的证明结果。我总结下来有四条硬规则。第一条C 模型必须是没有外部副作用的纯函数。意思是你不能在里面调 printf、写文件、开 socket、malloc 大块内存。C2RTL 拿到的 C 函数是要被形式化引擎分析的任何外部依赖都会破坏可证明性。如果参考模型里有随机数函数那更要警惕那相当于给参考输入加了一组不可控输入。第二条位宽必须显式。C 语言里 int 本身是多少位取决于编译环境虽然大多数时候你本地跑 x86 上 int 是 32 位但形式化工具看的是抽象算术语义如果不显式写明类型可能在位宽推导上产生和 RTL 不一致的假设。我通常会全项目只用定长类型比如int8_t、uint8_t、int64_t、uint128_t。需要 128 位中间积时用编译器内置的__int128但这部分要自己封装一下因为不同工具链对__int128的支持程度不完全一样。第三条不能有未定义行为。有符号整数溢出在 C 标准里是未定义行为但 Booth 乘法器本身天天在处理有符号数溢出。做法很简单C 模型里所有中间量都显式转成__int128再做乘法再把结果转回输出位宽。这样就不存在 undefined behavior也不存在工具和你本地编译器解释不一致的风险。第四条接口抽象要能对得上握手协议。C 函数不是写一个纯数学函数就完事如果 RTL 是start_i / valid_o多周期握手C 这边也需要用状态变量或者参数把“从请求到响应经过了几拍”表达出来否则工具没法判断应该在 RTL 的哪一拍拿参考结果去对比。最简单的建模方法是把一个“cycle accurate process”写成一个 switch case 状态机后面我会给出示例。我见过有人把 C 里所有变量都定义成volatile理由是防止编译器优化掉某些计算这个做法在 C2RTL 里没有必要反而可能让工具无法分析。C2RTL 有自己处理 C 语义的方式你只要保证代码是可编译、无副作用、位宽明确的普通 C剩下的交给工具。2.3 时钟复位与握手信号映射时钟和复位设置在 TCL 脚本里占的篇幅很小但影响很大。Booth 乘法器里有大量中间寄存器复位值如果处理不好形式化工具会认为寄存器初始状态是一组任意值证明就会去覆盖一些实际芯片上不可能出现的状态浪费不少时间。我的做法是在 TCL 里先定义主时钟再定义异步复位set_clock clk -period 10 set_reset rst_n -active low -asynchronous如果你的设计是同步复位就把-asynchronous去掉。复位信号命名要留意大小写uvm 环境里经常写成rst_n而 RTL 内部可能是arst_n这里必须按 RTL 实际端口名来不能拍脑袋。握手信号映射是 C2RTL 配置的核心。在我的工程里start_i是请求a_i和b_i是请求边上的数据valid_o是响应p_o是响应数据。这个映射关系要明确告诉工具工具才知道 C 函数的参数和 RTL 端口怎么对齐。下面第 3 节的脚本里会有完整写法。很多 C2RTL 脚本跑不动不是工具问题而是复位和握手映射没有定义清楚。你在报 bug 之前先把这两段配置打出来人眼确认一遍。3. 从工程创建到证明完整 TCL 脚本逐段拆解3.1 可以直接保存运行的完整脚本下面这个脚本是我把项目里实际用的 run_c2rtl.tcl 简化后得到的命令基于目前 JasperGold 的通用流程整理具体小版本号可能略有差异但骨架一致。保存为scripts/run_c2rtl.tcl即可# run_c2rtl.tcl # 用途JasperGold C2RTL 验证 64x64 Booth 乘法器 # 输入RTL :: rtl/booth_mul_top.sv 等 # 参考模型 :: c_ref/booth_mul_ref.c set PROJ_NAME booth_mul_c2rtl set RTL_TOP booth_mul_top set C_REF_FILE ../c_ref/booth_mul_ref.c set WORK_DIR ./work # ---- 1. 创建工程 ---- new_project -name $PROJ_NAME -path $WORK_DIR create_mode -name CONV -top $RTL_TOP # ---- 2. 读入 RTL ---- read_file -format sverilog ../rtl/booth_mul_top.sv read_file -format sverilog ../rtl/booth_enc.sv read_file -format sverilog ../rtl/booth_pp.sv # ---- 3. 时钟 / 复位 ---- set_clock clk -period 10 set_reset rst_n -active low -asynchronous # ---- 4. C2RTL 配置指定参考 C 模型 ---- c2rtl_setup -c_ref $C_REF_FILE -c_cycle_accurate yes # ---- 5. C2RTL 映射握手信号和数据 ---- # 请求信号start_i 拉高时采样 a_i b_i # 响应信号valid_o 拉高时输出 p_o c2rtl_map -clk clk -reset rst_n \ -req {start_i} \ -req_side {a_i[63:0] b_i[63:0]} \ -rsp {valid_o} \ -rsp_side {p_o[127:0]} # ---- 6. 抽象选项割点与符号扩展 ---- c2rtl_config -cutpoint {pp_tree[*] partial_sum[*] cpa_sum[*]} c2rtl_config -auto_symext yes c2rtl_config -abstract_limit 1024 # ---- 7. 证明 ---- c2rtl_prove -engine all -effort medium -timeout 1200 # ---- 8. 结果输出 ---- report_proofsummary report_cone -unproven exit这段脚本里有一个地方需要根据你实际工程修改pp_tree、partial_sum、cpa_sum这些内部信号名必须替换成你 Booth 乘法器 RTL 里真实存在的中间信号。割点设置选得准不准直接影响证明能不能收敛。3.2 工程创建和设计导入段脚本前两段做的事情和普通 JasperGold 形式验证完全一样。new_project指定工程名和路径create_mode指定顶层。这里有一个细节-top $RTL_TOP这个名字要和 RTL 模块名完全一致包括大小写。我之前因为顶层写成了booth_Mul_top工具在 link 阶段直接报 “top module not found”排查了半天还以为是 C2RTL 环境坏了。read_file要按依赖关系把 RTL 文件全部读进来。Booth 乘法器如果分成 booth_enc、booth_pp、booth_mul_top 三个文件三个都要读漏一个都不行。形式化分析和仿真一样都需要完整连通的 RTL 模型不是说形式化工具能自动补全某个黑盒。这个阶段最容易忽略的是编译选项。如果 RTL 里用了 SystemVerilog 的 interface、covergroup、assert property 这些结构read_file -format sverilog后面可能还需要加编译宏定义。我的脚本里没有写但实际工程中如果出现 “cant parse” 或者 “unresolved macro”就要回到这一步去加-define或者指定 include 目录。3.3 C2RTL 映射和抽象段脚本第 4 段到第 6 段是这个流程的核心。c2rtl_setup告诉工具 C 参考模型在哪个文件并且声明这是一个 cycle accurate 的 C 模型。如果 RTL 和 C 是纯组合关系可以把这个选项关掉但多周期流水乘法器必须打开。c2rtl_map是人和工具之间最重要的“翻译协议”。这里定义了什么信号代表一次新的乘法请求start_i拉高。请求时采样哪些数据a_i[63:0]和b_i[63:0]。什么信号代表结果返回valid_o拉高。返回时输出哪个数据p_o[127:0]。这个映射关系表面上简单但代表了 C2RTL 验证的核心思想C 模型并不关心 RTL 内部什么时候做编码、什么时候过压缩树它只关心一个更高层次的契约——你发一个请求我等若干个周期结果必须对。正是这个特点让 C2RTL 能扛住 RTL 流水结构调整。c2rtl_config里的-cutpoint是抽象配置。Booth 乘法器里部分积压缩树的信号位宽非常大如果不加割点直接证明BDD 很容易爆掉。给pp_tree[*]、partial_sum[*]或者cpa_sum[*]设割点相当于告诉工具这些中间节点不需要在证明里完全展开可以把它们当作自由变量做抽象。割点选多了会掩盖电路内部 bug选少了又可能超时需要结合 RTL 结构试几轮。-auto_symext yes表示让工具自动处理符号扩展。Booth 乘法器里符号扩展位处理是最容易出错的地方如果 RTL 和 C 模型在符号扩展上不一致打开这个选项后工具通常能更快地把反例定位到具体位而不是报一个“待选择”的模糊结果。3.4 证明和结果输出段c2rtl_prove的-engine all表示让 JasperGold 自动选引擎。实际验证中Booth 乘法器这种纯算术运算BDD 引擎通常比 SAT 表现更好因为算术逻辑展开成 BDD 时结构比较规则。我设了 1200 秒超时如果一轮跑不完会先看反例再决定是要加割点还是换引擎。report_proofsummary会输出每个证明目标的状态应该有 proven、disproven、aborted 三种结果之一。report_cone -unproven会把没有证明出来的目标对应的锥体逻辑打出来方便你去看是哪一段 RTL 导致的。这里有一个容易被忽略的点C2RTL 证明的是 RTL 和 C 模型的一致性不是 RTL 和一个绝对数学含义的一致性。所以 C 模型本身错了工具会报告 prove 成功但实际上参考就是错的。C 模型在上工具之前自己先用纯 C testbench 测一遍这一步省不得。4. 实测64×64 Booth 乘法器第一轮验证的完整过程4.1 第一次运行接口映射错在哪我第一轮跑的时候脚本是按照上面模板写的结果c2rtl_prove启动后不到一分钟就打印了一个反例。反例里 start_i 拉高后 valid_o 对应周期输出的 p_o和 C 参考模型给出的乘积差了很远而且所有 bit 看起来都没有规律。第一反应是 RTL 的 Booth 编码写错了但 debug 后发现问题出在映射上。我的 RTL 里a_i和b_i都是有符号 64 位但c2rtl_map里写的是a_i[63:0]这个写法本身没问题。可问题在于 C 模型形参用的是uint64_t两个有符号数被解释成了无符号数。C2RTL 的映射工具不会自动帮你做“RTL 端 signed 和 C 端 uint64_t”的语义统一它默认按位宽对齐然后以 C 模型里的类型去解释数据。这个差异在普通仿真里很难发现因为仿真向量只要没有跑到最高位为 1 的情况结果就都对。但形式化工具会穷举所有输入最高位为 1 是必然会被覆盖到的。看到反例里 p_o 差得离谱的时候我第一反应是 RTL bug最后定位到是映射类型白白浪费了半天。解决方式很直接把 C 模型参数改成int64_t输出用__int128封装的结构体。类型对齐之后一跑就过了。建议大家在写 C 参考模型和 c2rtl_map 的接口时把 RTL 端口的 signed/unsiged 和 C 函数形参类型列成一张对照表逐条核对。4.2 调整割点后把超时变成收敛接口类型问题解决后第二轮证明直接跑到超时。这是正常现象64×64 乘法意味着部分积加法和压缩树的状态空间非常大不做抽象裸跑基本不可能收敛。我加了割点配置c2rtl_config -cutpoint {pp_tree[*] partial_sum[*] cpa_sum[*]}但第一次跑还是超时。后来我排查了 JasperGold 的抽象报告发现abstract_limit默认值太小很多中间节点没有被自动抽象。把-abstract_limit 1024加上后有一部分目标开始证明出来了但还剩一个目标超时。这个剩余目标正好对应压缩树到最后一级超前进位加法器的路径也就是cpa_sum相关的逻辑。我把cpa_sum[*]单独拎出来再试了一轮最终在 600 秒内收敛。这里想提醒一个经验割点不是越多越好。如果给partial_sum[*]全加割点证明引擎会把所有中间点都当自由变量反而容易导致反例被过度抽象成假反例。更合理的做法是只对纯算术压缩树上的中间节点加割点对有控制逻辑参与的点保持展开。这个火候需要跑两三轮去试。4.3 证明结果和覆盖率观察最终一轮跑完报告显示所有 C2RTL 目标全部 proven另外加上我手写的两个 SVA 断言一个是复位后输出应为 0一个是 valid_o 拉高时 p_o 不能为 X。这两个断言和 C2RTL 证明是正交的分别覆盖“复位行为正确”和“输出不存在无定义态”。覆盖率方面C2RTL 本身不做传统行覆盖率统计它给的是“证明目标是否覆盖了全部输入空间”。只要 proven就说明在握手协议约束下所有可能的 a_i/b_i 输入组合都已经被证明等价。这比仿真到 100 万组随机向量还要扎实。比较有意思的是在我引入 C2RTL 之前团队已经做了两星期的定向仿真没有发现可疑点。C2RTL 跑完反而在第一轮就给了三个反例除接口类型那个以外还有一个是指定边界值下符号扩展位差一位的 bug另一个是压缩树最末级进位被截断的问题。这两个都是随机测试很难测到的场景尤其在输入向量分布偏向“常规值”的时候。C2RTL 的价值不是替代仿真回归而是把“算法和实现之间的语义鸿沟”这件事交给工具。仿真继续做它的覆盖率和系统级验证C2RTL 负责证明每一拍握手结果都符合 C 参考模型。两者合在一起才算完整的验证闭环。5. 最容易翻车的五个点以及我怎么处理5.1 符号扩展位拼接错误Booth 乘法器里-A 和 -2A 的负部分积是通过取反加一得到的多个部分积要按各自的权重对齐到压缩树。符号扩展位往往要扩展成多位才能保证求和不溢出。这类 bug 的表现是小数值正数全部正确大数值和负数偶尔错误。处理办法是先让 C2RTL 跑一轮如果反例集中在符号位高的输入上去 RTL 里看 booth_enc 的输出位宽尤其是符号扩展 bit 的拼接表达式。把 C 参考模型里的扩展逻辑和 RTL 里实际拼接的向量位宽做逐位对照基本都能定位。常见症状可能原因排查方向小数值漂亮大数值偶尔错部分积符号扩展位拼接差 1 bitbooth_enc 输出位宽与压缩树输入负数结果整体系统性偏移-A 编码的取反加一位置错误部分积最低位进位位置只有 radix-4 中 2A 路径错误左移一位逻辑在边界溢出编码选择的移位实现5.2 C 模型数据类型和 RTL 端口类型不一致这个问题我第 4 节已经踩过一次这里单独列出来是因为太容易犯。RTL 端口是logic signedC 模型形参却是uint64_tC2RTL 默认按位宽对齐不会帮你判断补码解释是否一致。一旦出现负输入形式化工具会立刻给出反例。我的经验是在 C 模型头文件里做一组宏封装把端口类型固定避免不同人维护时混用typedef int64_t booth_a_t; typedef int64_t booth_b_t; typedef __int128 booth_p_t;映射到 RTL 时a_i、b_i都要对应到booth_a_t、booth_b_t。这样类型不一致的问题在编译阶段就会暴露而不是等到证明阶段出反例。5.3 部分积压缩树的中间节点没有加割点Booth 乘法器内部有大量部分积相加的中间结果如果不加割点BDD 引擎可能要花大量时间在中间和值的展开上。尤其是 64×64 乘法部分积数量接近 33 个每一位中间和的 BDD 规模会非常大。但割点也不能乱加建议只加在满足下面条件的位置该节点是纯算术组合逻辑不包含控制分支。该节点的输出只是被后续加法器消费。该节点不会影响握手信号 valid_o 何时拉高。如果某个节点和控制逻辑有关给它加割点可能会生成假反例你永远无法收敛。5.4 寄存器初值不一致多周期流水线乘法器里中间流水寄存器在复位后会是 0。但 C 参考模型的状态机如果忘了初始化状态变量工具可能认为寄存器初值是一个自由变量从而把所有可能的初始状态都证明一遍。这样不仅跑得慢还有可能得到错误的反例。解决办法是让 C 模型的每个状态变量都有明确的初始值并且和 RTL 的复位行为保持一致。比如流水寄存器复位为 0状态机停在 IDLE那 C 变量也要这样初始化。不能只在 RTL 里做了复位同步C 模型里却没对应。5.5 握手信号 valid_o 存在不确定周期有些乘法器为了省功耗valid_o 不会像固定延迟流水线那样稳定输出它可能受多周期握手、反压或低功耗门控影响。C2RTL 对协议的假设是请求和响应具有可证明的时序关系如果 valid_o 被门控信号遮挡工具会在某些周期看到 valid_o 拉低而不知道是否要采样结果。这种场景下我建议先在 RTL 里加一个辅助断言valid_o一旦拉高在下一个请求之前不允许拉低或者至少要保证采样窗口不重叠。这不是限制设计而是帮 C2RTL 把协议边界定义清楚让证明目标更容易收敛。6. 验证之外的一点心得我这套流程跑完之后最大的体会是C2RTL 真正解决的不是“验证数学算对了没有”而是“验证模型和 RTL 实现之间有没有被工程化过程引入错误”。Booth 乘法器的数学原理很成熟难点全在把算法变成电路的过程里符号扩展、部分积对齐、流水时序每一个环节都可以偷偷埋下 bug。如果你正准备拿这个流程去验证自己项目里的乘法器我的建议是先花半天把 C 参考模型写好单独跑一遍纯 C 测试然后才去碰 TCL。C 模型如果不稳后面所有证明结果都会失去意义。脚本里的命令可以按你的工具版本微调但目录结构、接口映射、割点思路这三个核心骨架不要省。后面我会再写一篇关于 radix-8 Booth 编码下压缩树割点选择的文章那个场景比 radix-4 更考验抽象粒度。
