← 全部教程

高阶 SVA

深入 sequence 与 property：蕴含操作符、协议级断言与 bind。

  1. 01越过 |-> 和 ##[m:n]：这个赛道从哪里接着讲SV 第 15 章已经教过 immediate assertion、property/sequence、|-> 蕴含操作符和 ##[m:n] 范围延迟。这一章找出那套工具集精确的边界——一个它真的表达不出来的真实需求——并且用它来铺开这个赛道剩下要补的全部内容。
  2. 02为什么用断言，不用 if 语句：SVA 的价值在学更多 SVA 语法之前，先做一个公平的比较：第 15 章的 req_ack_p property，对上一个手写的 always_ff 检查器，检查的是同一条规则——放进 Icarus 里跑出来，不是空谈出来的——把真实的好处和真实的代价都摆在一起权衡。
  3. 03深入 Sequence 操作符固定周期延迟、两大类重复操作符、throughout、within、first_match，以及 sequence 级别的 and/or/intersect——第 1 章承诺过的词汇，顺带补上它自己那个 req/ack 缺口，并搭出 axil_regfile 真实的 AW/W 独立性规则。
  4. 04Property 与蕴含|-> 对比 |=>、disable iff，以及 property 级别的 not/and/or——把 axil_regfile 那条 VALID 不能等 READY 的规则，第一次在这个网站上写成一个真正的 property，而不只是停留在文字描述里。
  5. 05协议合规性断言：检查那些从未被测过的场景回报章节：针对 axil_regfile 三个真实的、至今仍未闭合的缺口分别写出 property——AW/W 独立性、A7 单笔未完成事务限制，以及 uvm-advanced 第 4 章那次竞争依赖的、COUNT 和 irq 之间确切的同边沿关系——全部搭建在第 1 到第 4 章已经建好的基础上，不是凭空造出来的场景。
  6. 06bind：不改动 DUT 也能检查它bind 到底是怎么工作的——把一个检查器模块的实例，放进目标模块自己的作用域内部，而写这条语句的文件从头到尾都碰不到 DUT 的源码——围绕着把第 5 章那三个真实的 property 从外部接进 axil_regfile 搭建起来。
  7. 07断言覆盖率：闭合回 Coverage 模块cover property 和 expect，然后是这个赛道真正的收尾：A5 那三个真实的、至今仍未测过的到达顺序场景，靠第 5 章自己的 property 变成一个覆盖率条目，重新走一遍 Test-Planning 第 5 章的四环追溯链，让断言覆盖率成为它的第五个指标。