SystemVerilog Assertions（SVA）用法以及帕拉丁emulation对SVA的支持情况总结
一：SystemVerilog Assertions (SVA) 用法总结
- SVA 简介SVA 是 SystemVerilog 的一个子集，用于以声明式或过程式的方式指定断言（assertions）、假设（assumptions）和覆盖率（cover）规格。SVA 继承 SystemVerilog 的表达语言，可用于描述设计意图，并通过仿真或形式验证进行验证。主要优势：
- 与设计/测试平台紧密集成
- 支持时钟周期精度的时序描述
- 可嵌入设计或通过 binding 外部添加
- 支持动作块（action block）触发代码执行
- 断言类型
2.1 立即断言 (Immediate Assertion)
在过程代码中立即求值，类似 if 条件。
表达式为 0/x/z 时失败，否则成功。
示例：
always @(push or pop) begin a_underflow: assert (cnt != 0); end2.2 并发断言 (Concurrent Assertion）
基于时钟语义，仅在时钟边沿采样求值。
使用 assert property (property_name)。
可在 always/initial 块、模块、接口、程序块中定义。
示例：
property p_underflow; @(posedge clk) disable iff (!reset_n) ((push,pop)==2'b01) |-> (cnt != 0); endproperty a_underflow: assert property (p_underflow);- 基本操作符
| 操作符/关键字 | 说明 |
|---|---|
| disable iff (expr) | 异步复位，表达式为真时属性无条件成立 |
| not | 否定一个属性，表示禁止序列 |
| $past(expr [, n]) | 取过去 n 个时钟周期的值 |
| $rose(expr) | 表达式上升沿检测 |
| $fell(expr) | 表达式下降沿检测 |
| $stable(expr) | 表达式值保持稳定 |
| $onehot(expr) | 只有一位为高 |
| $onehot0(expr) | 最多一位为高 |
- 序列 (Sequence)
序列是布尔事件的有序列表，用 ## 分隔。
4.1 基本序列
req ##1 ack // req 后一个周期 ack 为真4.2 延时范围
req ##[2:3] ack // req 后 2~3 个周期内 ack 为真4.3 重复操作符
| 操作符 | 含义 |
|---|---|
| seq[*n] | 连续重复 n 次 |
| seq[*m:n] | 连续重复 m 到 n 次 |
| seq[->n] | 非连续 goto 重复（在最后一次匹配结束） |
| seq[=n] | 非连续重复（可继续扩展） |
示例：
wr[*4] ##1 !wr // 连续4个wr，然后一个非wr4.4 序列操作符
| 操作符 | 说明 |
|---|---|
| seq1 |-> seq2 | 重叠蕴含：seq1 匹配的同一时钟开始 seq2 |
| seq1 |=> seq2 | 非重叠蕴含：seq1 结束后一个时钟开始 seq2 |
| expr throughout seq | 在整个 seq 期间 expr 必须保持为真 |
| first_match(seq) | 只匹配第一个可能的序列 |
| seq.ended | 检测序列的结束点 |
- 属性 (Property) 和序列声明
property p_request; @(posedge clk) disable iff (!reset_n) (req && !busy); endproperty sequence s_start_trans; @(posedge clk) (req && !busy ##1 (!gnt)[*1:4] ##1 gnt); endsequence- 指令 (Directives)
| 指令 | 用途 |
|---|---|
| assert property | 验证属性必须成立 |
| assume property | 假设属性成立，用于约束输入 |
| cover property | 覆盖率目标，检查序列是否发生 |
- 绑定 (Bind)
将验证代码与设计分离，无需修改 RTL：
bind cpu p_mutex fpu_rules_1(clk, reset_n, a, b, c);- 编码建议
- 命名约定：S_ 序列，P_ 属性，AST_ 断言，ASM_ 假设，COV_ 覆盖。
- 保持范围延迟较小：##[m:n] 分支过多会降低性能。· 避免无限范围：##[n:$] 导致 liveness 属性，尽量转为 bounded。
- 避免过长的连续重复：[*n] 增大证明深度。
- 避免空迭代：##0 b[*0] 会引起问题。
- 分离大型属性：拆分为多个小属性。
- 延迟检查：复位后延迟 N 个周期再开始检查，使用 ##N 或 $past。
- 利用总线对称性：只验证一个 bit 减少状态空间。
- 使用 $past 代替不必要的序列：提高性能。
二：Emulator (Palladium / IXCOM) 支持的 SVA 语法与用法
- 编译与运行支持概述
- 工具：IXCOM 编译器 + Xcelium 仿真器 + Palladium 仿真器。
- 支持：SVA 并发断言、立即断言、bind、cover、assume 等。
- 映射：DUT 中的断言映射到硬件仿真器，测试台中的断言运行在软件仿真器中。
- 选项：编译时需加 +sv 启用 SystemVerilog，使用 -coverage functional 启用覆盖率。
- 支持与不支持的 SVA 构造（基于 LRM 1800-2005/2009/2017）
完全支持的主要构造
| 类别 | 构造 |
|---|---|
| 立即断言 | assert (不能在 always_comb 等中) |
| 并发断言 | assert property, assume property, cover property |
| 延时范围 | ##[m:n] (仅允许编译时常量，超过32不支持某些上下文) |
| 序列声明 | sequence, 带类型的形式参数 |
| 重复操作符 | 连续 [*], goto [->], 非连续 [=] |
| 采样值函数 | $sampled, $rose, $fell, $stable, $past, $changed |
| 序列操作 | and, intersect, or, first_match, throughout, within |
| 端点检测 | .ended, .triggered, .matched (多时钟) |
| 系统函数 | $onehot, $onehot0, $countones, $isunknown (仅在 swap 到 simulator 时) |
| 属性操作 | not, disable iff, |->, |=>, if-else |
| 多时钟支持 | 有限支持，不能与 first_match 混用，不支持局部 |
| 变量默认时钟 | 支持 |
| 绑定 | 支持 bind |
| expect 语句 | 支持（DUT 中需显式指定行为编译） |
| 控制任务 | $asserton, $assertoff, $assertkill (在特定位置) |
部分支持或不支持的构造
| 构造 | 状态 | 备注 |
|---|---|---|
| 属性 and / or | 不支持 | 属性 OR 可用序列 OR 替代（cover 指令下） |
| 递归属性 | 不支持 | |
| 多时钟与 first_match | 不支持 | |
| 局部变量 | 支持但有限制 | 不能与 first_match 一起使用；不能在属性操作符两边跨越；赋值左侧必须只能一种匹配方式 |
| 大范围延时（>32） | 有限支持 | 需使用 +assertMaxIter 选项，或自动行为编译 |
| 行为编译 | 支持 | 用于多时钟、局部变量、大延迟、expect 等，会降低性能 |
- 性能与容量建议（针对 Emulator）
- 使用 assert_status 特性：启用调试功能（启用/禁用断言，波形调试），但消耗更多资源。
- 使用 assert_cover：为 assert/assume 生成覆盖率计数器（默认仅 cover 有计数器）。
- 计数器宽度：可通过 feature file 设置 assert_counter_check, assert_counter_finish, assert_counter_fail 的位宽，节省硬件资源。
- 优化静态断言：常量表达式断言会在编译时求值并优化掉，如需运行时检查应改写为立即断言。
- X/Z 值检查：在 2-state 仿真中 X/Z 转为 0/1，此类断言会自动仅运行于软件仿真器，或使用 ifdef SIMONLY 条件编译。
- 避免大范围重复：##[m:n] 和 [*n] 会增大状态空间，尽量限制范围。
- 拆分大属性：将多个信号或长序列拆分为多个属性，提高证明效率。
- 启用/禁用断言的方式
| 方法 | 说明 |
|---|---|
| 命令行选项 | +sv, -assert, -noassert |
| 特性文件 | sva enable/disable, assert_status, assert_cover |
| HDL 控制任务 | $asserton, $assertoff, $assertkill (需 +assertStatus) |
| 运行命令 | assertion -on/off (xeDebug Tcl) |
- 调试与报告
- GUI：xeDebug 的 Assertions 标签页，可查看断言状态、启用/禁用、获取摘要。
- 波形：支持 SimVision 和 Verdi，需 probe 断言及 fanin 信号。
- 断言状态：off, failed, finished, active, inactive。
- 覆盖率报告：生成 cov_work/ 下的 UCD 文件，可用 IMC 查看。
- CSV 报告：使用 -assert_report 生成 assertion_inst.csv, assertion_mod_inst.csv 等，包含断言权重（门数估计）。
- 典型编译命令示例
# 分析 Verilog 设计vlan-assertdut.v test.v# 创建 feature file (assert_status.ff)# 内容: assert_status enable# IXCOM 编译ixcom-ua+sv +dut+top-featureFileassert_status.ff-coveragefunctional top.v# 运行 xeDebugxeDebug-gui- 注意事项
- 未标记的断言会生成自动标签，调试困难，建议总是为断言添加有意义的标签。
- 生成块（generate）中的断言层次命名与 Xcelium 可能不同（gblk_0_ vs gblk[0]）。
- 仿真结束时“飞行中”的断言（未完成）在 IXCOM 中算失败，Xcelium 默认不算。
- IXCOM 不支持空满足（vacuous pass）触发动作块。
以上总结涵盖了 SVA 的基础用法以及 Cadence Palladium 仿真器/IXCOM 编译器对 SVA 的支持情况。