4. 组合逻辑属性验证

组合逻辑属性验证的核心难点不在“写不写断言”，而在于“断言在什么时刻被求值”。在 SystemVerilog 断言（SVA）中，立即断言与并发断言是两套完全不同的求值机制：前者像过程块中的 if 判断，在语句执行的那一刻立即求值；后者则绑定到时钟，在采样时刻对表达式进行采样并沿时间轴推进。若把两者混用，或忽略采样语义，就会出现“仿真通过、形式验证失败”或“断言永远不触发”的典型问题。

立即断言：过程块中的即时判断

立即断言使用 assert (表达式) else $error(...) 语法，出现在 always_comb、initial 或 function 等过程上下文中。它在执行到该语句的瞬间对表达式求值，不涉及时钟沿，也不产生采样。例如对组合逻辑的互斥检查：

always_comb begin
  assert (!(req0 && req1))
    else $error("req0 and req1 asserted simultaneously");
end

这段代码在 req0 或 req1 任一变化后重新执行 always_comb 时立即检查。它的优点是直观、无时钟依赖；缺点是只能覆盖仿真中实际执行到的时刻，形式验证工具通常不会把过程块中的立即断言作为时序属性来证明，因此它更适合仿真自检，而非形式收敛的主力。

并发断言：绑定时钟的采样语义

并发断言使用 assert property (...)，必须绑定时钟。其求值遵循“采样—推进”模型：在每个时钟沿（默认 posedge clk）对表达式中的变量进行采样，采样值在随后的时间步中用于判断。关键点在于：采样发生在时钟沿之前的一个极小时间片（preponed 区域），因此断言看到的是时钟沿到来前的稳定值，而不是沿之后被组合逻辑重新计算的值。

例如检查一个组合选择器输出：

property p_mux_sel;
  @(posedge clk) disable iff (!rst_n)
    (sel == 1'b0) |-> (dout == din0);
endproperty
assert property (p_mux_sel);

这里 |-> 是重叠蕴含：当 sel==0 在当前采样点成立时，同一采样点的 dout 必须等于 din0。注意 dout 是组合输出，它在时钟沿前已经由 sel 和输入稳定下来，因此采样到的 dout 与采样到的 sel 属于同一时刻的组合关系，这正是组合逻辑属性验证想要表达的“同一时刻约束”。

采样语义带来的三个常见陷阱

陷阱一：把组合延迟写进断言。 若写成 sel |-> ##1 (dout==din0)，则断言要求下一个时钟沿的 dout 满足条件。对于纯组合逻辑，下一沿的 dout 可能因输入变化而不同，导致断言在形式验证中被反例推翻。组合属性应使用重叠蕴含 |->，而非 |=> 或 ##1。

陷阱二：在并发断言中引用未采样变量。 若在 property 中直接使用 $past 或阻塞赋值变量，可能读到仿真器的当前值而非采样值。正确做法是让所有被检查信号都处于时钟采样域内，必要时用 $sampled 显式采样。

陷阱三：disable iff 与复位语义不一致。 disable iff (!rst_n) 表示复位有效时断言被禁用，但复位释放后的第一个时钟沿，采样值可能仍处于不确定状态。形式验证中若复位序列未约束，工具会从任意状态开始，导致断言在复位释放瞬间产生假反例。通常需要配合 assume property 约束复位行为，或使用 $rose(rst_n) 限定检查起点。

形式验证中的组合属性收敛要点

在形式验证工具中，组合逻辑属性通常被建模为“无状态”或“单周期”属性。工具会尝试证明：对于所有可能的输入组合，断言在任意采样点都成立。若属性中混入了跨周期依赖（如 ##1），工具会引入状态空间展开，可能造成证明不收敛。因此，组合逻辑验证应尽量保持属性在单周期内闭合。

另一个实践要点是：组合逻辑的输入空间可能非常大。例如一个 32 位加法器的进位链，若直接对全加器输出写断言，工具需要枚举 2^64 种输入组合。此时应通过 assume 约束输入范围，或将属性分解为多个局部断言（如逐位进位检查），降低单次证明的复杂度。

最后需要强调：立即断言与并发断言并非互斥。在组合逻辑验证中，可以用立即断言做仿真期间的快速自检，用并发断言做形式验证的收敛目标。两者配合，才能既保证仿真可见性，又保证形式证明的完备性。