SystemVerilog语法(16)-断言（SVA）基础

文章目录 本篇导读1 断言概述1.1 断言的价值1.2 五类断言语句2 立即断言Immediate Assertion2.1 延迟立即断言Deferred Immediate Assertion3 并发断言基础3.1 基本语法3.2 嵌入时钟的写法3.3 采样值函数r o s e 、 rose、rose、fell、s t a b l e 、 stable、stable、past4 sequence可复用的时序片段5 蕴含操作符|- 与 |6 空满足Vacuous Satisfaction—— 重要陷阱7 序列的端点ended 与 matched8 组合操作符and、or、intersect9 时间窗约束throughout、within throughout —— “全程保持” within —— “区间包含” 对比10 cover property覆盖属性11 序列局部变量与匹配项赋值12 断言的动态控制13 完整示例AHB 总线断言14 强属性与弱属性形式验证专用DV 可跳过15 assume 与 restrict形式验证专用DV 可跳过 核心区别速览15.1 assume —— “环境必须满足的假定”15.2 restrict —— “仅用于形式验证的约束” 三者对比16 常见错误与编码建议17 综合说明 主要参考 本篇导读知识点难度实战价值典型场景断言概述⭐⭐⭐⭐⭐⭐设计意图的形式化描述立即断言assert⭐⭐⭐⭐⭐⭐⭐过程块中的条件检查延迟立即断言assert #0/final⭐⭐⭐⭐⭐⭐避免组合逻辑毛刺、最终状态检查并发断言基础⭐⭐⭐⭐⭐⭐⭐⭐时序关系验证property与sequence⭐⭐⭐⭐⭐⭐⭐⭐可复用的时序描述常用操作符$rose、$fell、$stable、$past⭐⭐⭐⭐⭐⭐⭐边沿检测、稳定性、历史值蕴含操作符|-与|⭐⭐⭐⭐⭐⭐⭐⭐条件触发与延迟空满足Vacuous Satisfaction⭐⭐⭐⭐⭐⭐⭐避免前件永假导致断言失效ended与matched⭐⭐⭐⭐⭐⭐序列端点同步throughout、within等⭐⭐⭐⭐⭐⭐⭐复杂时序约束cover属性⭐⭐⭐⭐⭐⭐功能覆盖率序列局部变量⭐⭐⭐⭐⭐⭐⭐复杂数据相关性检查断言的动态控制⭐⭐⭐⭐⭐⭐仿真中启用/禁用/终止断言强属性与弱属性strong/weak⭐⭐⭐⭐⭐⭐⭐形式验证中的有限时间证明DV 可跳过assume与restrict⭐⭐⭐⭐⭐⭐形式验证约束DV 可跳过常见误区混淆立即断言与并发断言的采样时机|-与|的延迟语义差异忘记时钟导致并发断言不工作序列跨越多个时钟边界时采样不稳定$past未考虑初始时刻忽略蕴含操作符的空满足导致断言永远无法发现错误。 本文中立即断言可用于设计综合时被忽略并发断言主要面向验证与形式验证。综合工具通常只支持简单的并发断言子集用于仿真不变式。1 断言概述断言是描述设计应该遵守的行为的语句。在仿真或形式验证中工具检查断言是否被违反。1.1 断言的价值捕获错误更早当违反发生时立即报错而非等到输出出错。文档化设计意图断言就是可执行的注释。提升验证质量形式验证可以证明断言永远为真覆盖所有输入。1.2 五类断言语句根据 IEEE 1800-2017 标准SystemVerilog 提供了以下五类断言语句语句关键字适用场景仿真行为形式验证行为立即断言assert过程块内即时检查立即检查被忽略并发断言assert property时序关系验证时钟沿采样检查证明属性假定assume property输入环境约束✅ 也会检查违反作为输入约束约束restrict property仅形式验证的输入约束❌ 不检查作为输入约束覆盖cover property时序场景覆盖率记录是否触发验证是否可达2 立即断言Immediate Assertion与if语句类似在仿真当前时刻检查条件。always_comb begin assert (a ! b) else $error(a and b should not be equal); end initial begin assert (rst_n ! 1b0) else $display(Reset is active at start); end严重性控制assert (condition) else $fatal; // 终止仿真 assert (condition) else $error; // 报错继续 assert (condition) else $warning; // 警告 assert (condition) else $info; // 普通信息立即断言的局限无法描述时序如“在请求之后 3 个时钟内必须响应”在时钟沿之外评估可能采样到组合逻辑毛刺2.1 延迟立即断言Deferred Immediate Assertion为解决组合逻辑毛刺问题标准提供了延迟立即断言在当前时间步的末尾评估类似非阻塞赋值的效果。// 观察延迟断言在当前时间步末尾评估避免毛刺 always_comb begin assert #0 (a ! b) else $error(a and b should not be equal); end // 最终延迟断言在仿真结束时评估用于检查最终状态一致性 final begin assert (final_count expected_count) else $error(Final count mismatch); end3 并发断言基础并发断言在时钟边沿统一采样信号值描述跨时钟周期的行为。3.1 基本语法property name; (posedge clk) expression; endproperty assert property (name);最简单的并发断言assert property ((posedge clk) !(rst_n en (cnt 0)));3.2 嵌入时钟的写法// 方式一property 内部带时钟 property p_never_both; (posedge clk) !(req1 req2); endproperty assert property (p_never_both); // 方式二property 外部指定时钟推荐复用 property property p_no_overlap; !(req1 req2); endproperty assert property ((posedge clk) p_no_overlap);3.3 采样值函数r o s e 、 rose、rose、fell、s t a b l e 、 stable、stable、past这些系统函数检测信号相对于前一采样点的变化或获取历史值。函数条件$rose(sig)上次采样为 0本次为 1$fell(sig)上次采样为 1本次为 0$stable(sig)两次采样值相同$past(sig, n)n 个时钟周期前的 sig 值默认 n1property p_ack_after_req; (posedge clk) $rose(req) |- ##[1:4] $rose(ack); endproperty assert property (p_ack_after_req); // 使用 $past 检查当前数据必须与 2 周期前不同 property p_not_repeat; (posedge clk) (data ! $past(data, 2)); endproperty4 sequence可复用的时序片段sequence定义一系列连续的时钟周期行为可在多个property中复用。sequence s_req_ack; $rose(req) ##[1:4] $rose(ack); endsequence property p_req_ack; (posedge clk) s_req_ack; endproperty assert property (p_req_ack);带参数的 sequencesequence s_request_ack(int min_delay, int max_delay); $rose(req) ##[min_delay:max_delay] $rose(ack); endsequence5 蕴含操作符|- 与 |蕴含用于表达前提与结果的关系。操作符含义示例|-前提满足的同一时钟周期检查结果req |- ack|前提满足的下一个时钟周期开始检查req | ack关键区别|-req在时钟沿成立结果从同一个沿开始计算常用|req在时钟沿成立结果从下一个时钟沿开始计算等价于|- ##1// 请求的下一拍 must 为高 property p_req_must; (posedge clk) $rose(req) |- ##1 must; endproperty // 请求后 2 到 5 拍内 data_valid 为高 property p_data_valid; (posedge clk) req |- ##[2:5] data_valid; endproperty6 空满足Vacuous Satisfaction—— 重要陷阱当蕴含操作符的前件永远为假时整个属性会被视为空满足自动通过这可能导致设计错误被掩盖。// 如果 req 信号在整个仿真中从未变为高电平这个断言永远不会失败 property p_ack_after_req; (posedge clk) $rose(req) |- ##[1:4] $rose(ack); endproperty解决方案使用cover property检查前件是否真的被触发过。cover property ((posedge clk) $rose(req)); // 确保 req 至少出现一次7 序列的端点ended 与 matched用法含义seq.ended序列在当前时钟周期结束单时钟域常用于序列终点对齐seq.matched用于跨时钟域时检测序列结束存储结束事件直到目标时钟域sequence s_req; $rose(req) ##2 ack; endsequence property p_req_then_data; (posedge clk) s_req.ended |- ##1 data_valid; endproperty多时钟域示例matchedsequence s_fast; (posedge clk_fast) a ##1 b; endsequence property p_cross; (posedge clk_slow) s_fast.matched |- c; endproperty8 组合操作符and、or、intersect// and: 两个序列同时开始各自匹配整体匹配结束于较晚完成的那个序列的结束点 sequence s1; (posedge clk) a ##2 b; endsequence sequence s2; (posedge clk) c ##3 d; endsequence property p_and; (posedge clk) s1 and s2; endproperty // intersect: 两个序列必须同时开始并且同时结束长度必须相同 property p_intersect; (posedge clk) s1 intersect s2; endproperty // or: 任一满足即可 property p_or; (posedge clk) s1 or s2; endproperty⚠️ 注意intersect要求两个序列长度相同。示例中s1##23 拍和s2##34 拍长度不同intersect永远无法匹配实际使用时应确保长度一致。9 时间窗约束throughout、within// 在 seq 的整个持续时间内条件一直成立 property p_throughout; (posedge clk) $rose(req) |- (busy 1) throughout (req ##[1:5] ack); endproperty // seq1 完全包含在 seq2 的时间窗内 property p_within; (posedge clk) seq1 within seq2; endproperty throughout —— “全程保持”含义在右边序列匹配的每一个时钟周期左边的条件都必须为真。简单说条件 throughout 序列 “序列跑多久条件就得撑多久。”检查机制序列的每一拍开始、中间、结束都检查条件任何一拍条件为假 → 失败。 within —— “区间包含”含义左边的序列必须完全落在右边序列的时间窗口之内。简单说seq1 within seq2 “小序列不能比大序列早开始也不能比大序列晚结束。”检查机制seq1开始 ≥seq2开始seq1结束 ≤seq2结束边界可重合。 对比操作符关注点一句话人话throughout信号的值“这段时间里这信号必须一直为 1”within区间的边界“这小动作必须完全在大窗口内完成”10 cover property覆盖属性用于衡量某个序列在仿真中是否出现过功能覆盖率的重要补充。sequence s_scenario; $rose(enable) ##[1:10] (addr 32h1000) ##1 write; endsequence cover property ((posedge clk) s_scenario);与covergroup相比cover property更擅长描述时序场景。实战建议每个assert property中的关键前件都应配套一个cover property来检测空满足。11 序列局部变量与匹配项赋值可以实现复杂的数据相关性检查。// 检查写地址和读地址对应的数据一致 property p_read_correct; logic [31:0] addr, data; // 局部变量 (posedge clk) ($rose(wr_en), addr wr_addr, data wr_data) // 匹配项赋值 |- ##[1:10] $rose(rd_en) (rd_addr addr) ##1 (rd_data data); endproperty assert property (p_read_correct);关键点局部变量在property内部声明匹配项赋值(sequence, v expr)在序列匹配成功时执行变量作用域仅限于该property12 断言的动态控制在仿真中可以使用系统任务动态启用/禁用/终止断言。任务作用$asserton(level, scope)启用断言$assertoff(level, scope)禁用断言$assertkill(level, scope)终止所有正在进行的断言检查initial begin $assertoff(0, top.dut); // 复位期间禁用所有断言 wait (rst_n 1b1); $asserton(0, top.dut); end final begin $assertkill(0, top.dut); // 仿真结束前终止未完成的并发断言 endlevel 0作用于指定层级及以下所有断言level 1仅作用于当前层级不包含子模块level 2仅作用于指定模块本身不包含子模块和内部语句13 完整示例AHB 总线断言module ahb_assertions ( input logic hclk, input logic hreset_n, input logic hsel, input logic [1:0] htrans, input logic hwrite, input logic hready, input logic [2:0] hburst, input logic [31:0] haddr, input logic [31:0] hwdata ); // 1. 地址在数据传输期间必须稳定仅限 SINGLE 传输 property p_addr_stable; (posedge hclk) disable iff (!hreset_n) (hburst 3b000 htrans ! 2b00 hready) |- $stable(haddr); endproperty assert property (p_addr_stable) else $error(addr changed during transfer); // 2. 写数据应在 hready 有效时稳定 property p_wdata_stable; (posedge hclk) disable iff (!hreset_n) (hwrite hready) |- $stable(hwdata); endproperty assert property (p_wdata_stable); // 3. AHB 传输类型约束非连续传输后不能直接跟另一个非连续 property p_valid_htrans; (posedge hclk) disable iff (!hreset_n) (htrans inside {2b10, 2b11}) | (htrans inside {2b00, 2b01, 2b11}); endproperty assert property (p_valid_htrans); // 4. 覆盖场景写操作后跟读操作 property p_write_then_read; (posedge hclk) $rose(hwrite) ##[1:5] $fell(hwrite); endproperty cover property (p_write_then_read); // 5. 确保非空满足使用 cover 检查前件是否出现 cover property ((posedge clk) (htrans inside {2b10, 2b11})); endmodule⚠️注意这是一个断言模块需要绑定到 DUT 或由 Testbench 驱动才能生效。单独编译不会产生有效验证。14 强属性与弱属性形式验证专用DV 可跳过本节受众主要面向形式验证Formal Verification用户。如果您的日常工作仅涉及仿真验证可直接跳过本节不影响其他内容的理解。在形式验证中需要区分属性是否要求有限时间内必须完成。类别关键字语义仿真行为弱属性weak(P)允许无限延迟不需要匹配检查已发生的匹配若未匹配不报错强属性strong(P)要求存在一个非空匹配同弱属性仅检查已发生的匹配// 形式验证中证明 ack 最终一定会出现 assert property ((posedge clk) strong($rose(req) |- ##[1:$] $rose(ack)));strong要求“终将到来”形式验证会证明这一点仿真中weak和strong没有区别因为仿真时间有限在形式验证工具如 JasperGold中strong要求序列必须在有限时间内匹配否则属性失败15 assume 与 restrict形式验证专用DV 可跳过本节受众主要面向形式验证用户。DV 工程师只需记住assume仿真会检查restrict仿真不检查。assume和restrict在形式验证中用于约束环境输入的行为。它们不检查设计本身而是告诉验证工具“外部输入会怎样”。 核心区别速览关键字仿真行为形式验证行为assume✅会检查违反会报错作为输入约束限制验证空间restrict❌不检查完全忽略作为输入约束限制验证空间一句话总结assume 仿真的环境断言 形式验证的输入约束restrict 纯形式验证的输入约束。15.1 assume —— “环境必须满足的假定”含义告诉工具“外部环境保证会这么做如果违反了那是环境的问题不是设计的问题”。两个身份仿真中像assert一样检查。如果假设被违反比如rst_n在时钟沿变化了仿真报错。形式验证中作为有效约束。工具只在满足这些假设的输入序列中搜索反例。// 假设复位信号在时钟沿稳定不会在边沿变化 assume property ((posedge clk) $stable(rst_n)); // 假设有效请求最少间隔 2 个周期 assume property ((posedge clk) $rose(req) | !req ##1 !req);15.2 restrict —— “仅用于形式验证的约束”含义告诉形式验证工具“在这些输入模式之外的情况我不关心”。仿真中完全忽略不检查。典型场景某些输入组合在真实系统中永远不会出现但仿真时可能因为激励不完整而出现 → 用restrict告诉形式验证工具排除这些情况。你不想在仿真中检查这些条件避免误报但形式验证需要知道。// 仅用于形式验证告知工具输入不会出现某些模式仿真中忽略 restrict property ((posedge clk) !(req ack)); 三者对比assertassumerestrict检查谁设计本身环境输入环境输入仿真行为检查失败报错检查失败报错❌ 忽略形式验证行为作为证明目标作为输入约束作为输入约束反例意义设计有 bug环境假设被违反输入超出范围16 常见错误与编码建议并发断言中遗漏时钟→ 每个 property 或assert property必须有(posedge clk)或其他时钟事件。|-与|混淆导致延迟错误→ 记住|相当于|- ##1。$rose/$fell在初始时刻未定义→ 使用disable iff (reset)避免复位时误报。忽略空满足导致断言形同虚设→ 对关键前件配合cover property确保被触发过。property 中使用了阻塞赋值风格的时序→ 并发断言不能包含#延迟或过程语句。序列过长导致仿真性能下降→ 合理拆分sequence避免深度嵌套。断言密度适中太多断言拖慢仿真太少遗漏 bug。→ 优先写关键时序关系、状态机不变式、接口协议。误用assume以为仿真不检查→ 记住assume在仿真中也会报错如需纯形式验证约束请用restrict。$past初始周期误报→ 使用##1延迟第一拍或disable iff (rst_n)保护。17 综合说明简单并发断言如$rose、|-、##可以被某些综合工具转换为仿真监控逻辑但一般不推荐依赖综合产生实际硬件。立即断言在综合时被忽略只用于仿真。形式验证工具如 JasperGold完全支持并发断言可以不施加激励直接证明。 主要参考IEEE Standard for SystemVerilog (1800-2017)关于文章原创深度实战分享转载需注明出处。 点击关注第一时间收到后续教程推送。参考文档IEEE Standard for SystemVerilog