断言(assertion)
想象在你的设计里接了一个烟雾报警器。你只需把规则声明一次——"这个警报永远不能响",或者"每个请求都必须在三个时钟节拍内得到回应"——从那以后就有一个小小的看守者守在那里,睁大眼睛,每个周期都核对这条规则。一旦现实违反了规则,它就尖叫起来,并径直指向出问题的地方。断言正是如此:它是一种嵌入设计内部的检查,一旦被声明的属性遭到违反就立即触发。于是你不必再盯着成千上万个波形周期苦苦猜测哪里出了错,仿真器会直接把你带到规则第一次被打破的那个确切时刻和信号上。
更确切地说,断言是关于硬件必须如何行为的一种意图陈述,它的写法让工具能够持续地监视它。最常见的形式是 SystemVerilog 断言(SVA),分为两种风格。立即断言在过程代码中的某一时刻检查一个简单条件,就像一句守卫语句。并发断言则描述一种随时间针对时钟而展开的关系——"如果 grant 拉高,那么在两个周期内 busy 必须随之而来"——它在每个时钟边沿都被求值,并在边沿到来之前就采样它的信号,因此读取的是稳定的值,而不会与这些信号竞争。由于规则就紧贴在 RTL 旁边,它以一种永远不会悄悄过时的形式记录下设计者的假设:一旦设计不再遵守这条假设,断言就会失败。
好处有两方面。在仿真中,断言把那些悄无声息、波及深远的错误,变成在源头就被抓住的响亮失败——这是"输出错了"与"漏洞就在这里,在这条信号上、在这个周期"之间的区别。而且因为它们是关于意图的精确数学陈述,同一批断言可以交给形式化工具,由它尝试对所有合法输入证明这些断言为真,而不仅仅是你的测试平台碰巧尝试过的那些激励。覆盖率工具还能追踪每条断言中那些有意思的情形究竟被触发了多少次,于是你了解到的不只是"什么都没出错",还有你是否真的曾经测试过这条规则。
// If req is asserted, ack must arrive within 1 to 3 cycles. property p_req_ack; @(posedge clk) req |-> ##[1:3] ack; endproperty assert property (p_req_ack);
一条并发断言:在每次 `req` 之后,工具检查 `ack` 是否在一到三个时钟周期内随之而来——一旦没有,它立刻报错。
这里的"断言"是设计做出的一种承诺,而不是用于调试的 `print`。一条通过的断言会在整个运行过程中默默无声、毫无存在感;只有当出了问题时你才会听到它的动静——这正是为什么一套周全的断言是硬件设计中最廉价的保险之一。