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)2b01) |- (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 匹配的同一时钟开始 seq2seq1 | seq2非重叠蕴含seq1 结束后一个时钟开始 seq2expr 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)将验证代码与设计分离无需修改 RTLbind 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 混用不支持局部变量默认时钟支持绑定支持 bindexpect 语句支持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_coverHDL 控制任务$asserton, $assertoff, $assertkill (需 assertStatus)运行命令assertion -on/off (xeDebug Tcl)调试与报告GUIxeDebug 的 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-uasv duttop-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 的支持情况。