4. SVA断言工程化编写

在形式验证中，SVA 断言不是“仿真里能过就行”的检查语句，而是被工具展开成状态机、参与证明或反例搜索的约束与目标。因此，断言工程化的核心目标是：让每条断言在形式语义下边界清晰、时钟明确、可被证明或可被证伪。本节围绕序列、属性、时钟域、禁用条件、局部变量与递归属性六个要素，说明如何写出面向 VC Formal 的可证明断言。

一、序列与属性：先分清“描述什么”与“断言什么”

序列（sequence）描述一段时间窗内的波形模式，属性（property）则把序列与蕴含、时钟、禁用等组合成可判定的断言。工程上建议：序列只负责“波形长什么样”，属性负责“在什么条件下必须成立”。例如一个请求到应答的握手：

sequence s_req_ack;
  req ##[1:3] ack;
endsequence

property p_req_ack;
  @(posedge clk) disable iff (!rst_n)
  req |-> s_req_ack;
endproperty

a_req_ack: assert property (p_req_ack);

这里 ##[1:3] 表示 1 到 3 个时钟周期内出现 ack。形式工具会把该窗口展开为多周期路径，若窗口过宽，状态空间会显著增大。因此序列窗口应尽量收紧到设计真实允许的范围，而不是用 ##[1:$] 这类无界窗口。

二、时钟域：每条断言只绑定一个采样时钟

SVA 的采样语义由断言所在时钟块决定。跨时钟域断言若直接写两个时钟，形式工具通常无法有效证明。正确做法是：每条断言绑定单一采样时钟，跨域关系用同步器后的稳定信号表达。例如从 clk_a 到 clk_b 的脉冲传递，应在 clk_b 域对同步后的 req_sync 断言，而不是在一条属性里同时写 @(posedge clk_a) 和 @(posedge clk_b)。

三、禁用条件：复位与模式必须显式、可证明

disable iff 用于在复位、扫描模式、低功耗保持等条件下关闭断言。工程化写法要求：禁用条件必须是可综合、可被形式工具识别的单比特条件，且与设计复位语义一致。例如：

property p_data_stable;
  @(posedge clk) disable iff (!rst_n || scan_en)
  valid |=> $stable(data);
endproperty

若禁用条件写成复杂表达式或含未初始化寄存器，形式工具可能无法收敛。建议把禁用条件抽成独立信号，并在断言文件中集中定义，便于复用与审查。

四、局部变量：用 $past、$stable 与局部变量表达历史关系

局部变量（local variable）用于在序列中捕获某时刻的值，并在后续周期比较。典型场景是“请求发出时的地址，在应答时必须一致”：

property p_addr_match;
  logic [31:0] addr_q;
  @(posedge clk) disable iff (!rst_n)
  (req, addr_q = addr) |=> (ack |-> (rdata == addr_q));
endproperty

这里 addr_q 是局部变量，只在本次匹配中有效。形式验证中，局部变量会引入额外状态，若断言数量多、变量位宽大，会明显增加证明难度。因此应只捕获必要字段，避免在断言中做复杂运算。历史关系也可用 $past、$stable 表达，但要注意 $past 的周期数与复位后的无效窗口。

五、递归属性：谨慎使用，优先展开为有限深度

递归属性适合描述“持续保持直到某事件”的协议，例如总线锁定、仲裁保持。但形式工具对递归的展开深度有限，容易导致证明不收敛。工程上建议：能用有限窗口表达就不用递归；必须递归时，显式给出终止条件与最大深度。例如：

property p_hold_until_ready;
  @(posedge clk) disable iff (!rst_n)
  hold |-> (ready or ##1 p_hold_until_ready);
endproperty

该属性在 ready 出现时终止。若 ready 可能长期不出现，形式工具会持续展开，此时应增加超时约束或改用 ##[1:N] 的有限窗口。

六、面向形式验证的可证明性写法

可证明性取决于断言是否“有界、确定、无歧义”。以下检查表可直接用于断言评审：

此外，断言应与设计层次对应：模块级断言只引用本模块端口与内部信号，跨模块协议在集成层单独编写。这样在 VC Formal 中可按模块划分证明任务，避免全局状态爆炸。

最后给出一个可直接复用的断言模板，覆盖上述六要素：

// 模块级断言模板：单时钟、有界窗口、显式复位、精简局部变量
property p_handshake;
  logic [31:0] addr_q;
  @(posedge clk) disable iff (!rst_n)
  (req, addr_q = addr) |-> ##[1:3] (ack && rdata == addr_q);
endproperty

a_handshake: assert property (p_handshake)
  else $error("handshake failed at %t", $time);

在 VC Formal 中加载该断言后，应先在 elaborate 阶段确认无多时钟警告，再用 prove 任务观察证明结果。若出现 inconclusive，优先检查窗口是否过宽、局部变量是否过多、递归是否有终止条件，而不是直接放宽断言。断言工程化的本质，是让每条断言都成为形式工具能够理解并给出确定结论的“可证明命题”。