📚 课程目录第3章并发断言与即时断言

3. 并发断言与即时断言

在 SystemVerilog 断言体系中，并发断言（concurrent assertion）与即时断言（immediate assertion）是两条并行的语法路径，而 assert、assume、cover、restrict 则是四种属性（property）应用类型。很多初学者把它们混为一谈，结果在 Xcelium 仿真中看到断言既不报错也不覆盖，却找不到原因。本节先把这两组概念拆开，再用一个接口协议断言把四类属性全部用上。

并发断言与即时断言的区别

即时断言写在过程块（always、initial、function、task）内部，像一条 if 语句一样在当前仿真时刻立即求值。它只能描述组合逻辑或当前采样值的布尔条件，例如 assert (req !== 1'bx)。即时断言没有时钟概念，也不支持 |->、## 这类时序算子。

并发断言写在模块、接口或 program 中，基于采样时钟工作。它在时钟边沿对表达式采样，可以描述跨周期行为，例如“请求拉高后 1~3 个周期内必须收到应答”。并发断言的核心是 property，而 assert、assume、cover、restrict 决定这条 property 被如何使用。

四类属性应用类型的语义

类型	语义	仿真行为	典型用途
`assert`	检查设计是否满足属性	失败时报错，计入断言覆盖率	协议时序检查
`assume`	约束环境/输入的合法行为	在形式验证中作为约束；仿真中默认按 assert 检查	输入激励合法性
`cover`	统计属性是否被触发	不报错，只记录命中次数	场景覆盖、激励到达性
`restrict`	强制约束，禁止违反	形式验证中作为硬约束；仿真中通常被忽略	形式验证环境建模

关键点：assume 和 restrict 的主要价值在形式验证。在 Xcelium 的纯仿真流程里，assume 默认按 assert 处理（可用 -assert_assume 等选项调整），而 restrict 一般不参与仿真检查。因此做仿真验证时，真正会“报错”的是 assert，真正会“统计覆盖”的是 cover。

编写一个接口协议断言

下面以一个简化的握手接口为例。接口信号：clk、rst_n、req、ack。协议约定：req 拉高后，ack 必须在 1 到 3 个时钟周期内拉高；req 与 ack 不能同时为 X。我们把这四类属性全部写进一个 interface 中。

interface handshake_if (input logic clk, input logic rst_n);
  logic req;
  logic ack;

  // 1) assert：协议时序检查，失败报错
  property p_req_ack;
    @(posedge clk) disable iff (!rst_n)
      $rose(req) |-> ##[1:3] ack;
  endproperty
  a_req_ack : assert property (p_req_ack)
    else $error("[ASSERT] req 拉高后 1~3 周期内未收到 ack");

  // 2) assume：约束输入激励合法，req 不应为 X
  property p_req_known;
    @(posedge clk) disable iff (!rst_n)
      !$isunknown(req);
  endproperty
  a_req_known : assume property (p_req_known);

  // 3) cover：统计“req 与 ack 同时为高”的握手场景
  property p_handshake;
    @(posedge clk) disable iff (!rst_n)
      req && ack;
  endproperty
  c_handshake : cover property (p_handshake);

  // 4) restrict：形式验证中禁止 req 与 ack 同时为 X
  property p_no_x;
    @(posedge clk) disable iff (!rst_n)
      !($isunknown(req) || $isunknown(ack));
  endproperty
  r_no_x : restrict property (p_no_x);
endinterface

注意 disable iff (!rst_n) 的位置：它必须写在时钟事件之后、属性表达式之前，否则复位期间断言会误报。这是 Xcelium 中最常见的断言误报来源之一。

在 Xcelium 中调试断言

编译时启用断言支持：xrun -sv -assert。仿真时若断言失败，Xcelium 会打印类似 "a_req_ack" failed at time 125ns 的信息，并给出属性名和失败时刻。要观察 cover 命中情况，可在仿真结束后查看 cover property 的统计报告，或在波形中观察 c_handshake 对应的内部信号。

调试建议：先用 cover property 确认激励真的能触发目标场景，再打开 assert property 检查时序。如果 cover 从未命中，说明激励没到位，此时断言失败往往不是设计问题，而是测试平台问题。

assume 在纯仿真中默认按 assert 检查，若激励本身可能产生 X，会导致误报。若只想在形式验证中约束，可考虑用 restrict，或在仿真时通过工具选项关闭 assume 的检查行为。

四类属性的选择依据

要检查设计是否违反协议 → 用 assert，失败即报错。
要约束输入/环境的合法取值范围 → 用 assume，形式验证中作为约束，仿真中谨慎使用。
要统计某个场景是否被激励覆盖 → 用 cover，不报错，只记录命中。
要在形式验证中强制禁止某些行为 → 用 restrict，仿真中通常不生效。

把四类属性放在同一个接口里，可以让协议检查、激励约束、场景覆盖和形式约束共享同一套信号定义，避免重复声明，也便于在 Xcelium 中统一管理断言覆盖率。实际项目中，建议按“一个协议一组属性”的方式组织，属性名用 a_、c_、r_ 前缀区分类型，便于在覆盖率报告中快速定位。