极客工场

Appearance

共 2,516 字预计阅读约 8 分钟

计数器边界验证：使能/加载/回卷与上溢下溢怎么验 ​

更新时间：2026-09-25。计数器（counter）和定时器（timer）是芯片里数量最多的小模块——PWM、分频、FIFO 指针、超时检测、事件计数全靠它。逻辑简单到「不就是每拍加一」，但流片后关于计数的 bug 几乎都出在边界拍和控制信号组合上。本文是验证实操序列的长尾专题，假定你已经读过 SystemVerilog Testbench 实战，知道怎么搭自检平台。

本文要回答的问题 ​

  • 计数器边界验证到底要覆盖哪些输入组合，才不算「跑了几百万拍其实什么都没验到」？
  • 上溢回卷（MAX 加一变 0）和下溢回卷（0 减一变 MAX）那一拍，怎么用断言锁死？
  • 定向、随机、SVA、覆盖率、参考模型在这个小模块上各自负责什么，怎么拼起来？

一、先把验证对象的语义钉死 ​

一个稍完整的可加减计数器端口通常长这样：clk、rst_n、cen（clock enable，时钟使能）、load、clr、up_down、d[W-1:0]（加载值）、q[W-1:0]、carry/borrow。验证开始前必须从规格书确认三件模糊的事，因为它们恰恰是 bug 温床：

  1. 控制优先级：同一拍 clr 和 load 同时有效谁赢？常见约定是同步清零最高、加载次之、计数最低；也有设计清零是异步的。优先级错一个，激励就得重写。
  2. 使能语义：cen=0 时是保持不动，还是 load/clr 也被挡住？有些设计清零不受使能管辖。
  3. 回卷与标志：宽度 W 的计数器最大值 MAX = 2^W − 1。加计数到 MAX 再有效使能，下一拍必须回卷到 0 且 carry 只拉高那一拍；减计数在 0 再减，下一拍回卷到 MAX 且 borrow 有效一拍。标志是电平还是脉冲、提前一拍还是同拍输出，都要逐字对规格。
输入组合（cen / clr / load / up_down）次态 q说明
0 / x / x / x保持使能关闭，绝大多数控制被冻结
1 / 1 / x / x0同步清零优先级最高
1 / 0 / 1 / xd加载任意值，包括 0 和 MAX
1 / 0 / 0 / 1q+1（回卷）MAX 时次态为 0
1 / 0 / 0 / 0q−1（回卷）0 时次态为 MAX

这张表就是后面定向用例和参考模型的共同依据，也是计数器边界验证的「真相表」。

另外两个细节也值得在动工前问清楚：复位是异步还是同步、复位值是 0 还是某个预设初值（有的上电定时器从 MAX 倒数）；carry/borrow 是「到达极值那拍」就拉高，还是「极值且下一拍继续计数」才拉高。前者标志与 q=MAX 同拍，后者标志在回卷拍与 q=0 同拍，差一拍断言就完全相反。这类语义规格书常常写得含糊，与其猜，不如带着波形去和设计人员当面确认一次。

二、边界回卷波形：bug 只活在那一拍 ​

下图是一个 4 位加计数器在使能连续有效时的回卷过程，同时叠加了一次清零：

计数器边界验证：使能/加载/回卷与上溢下溢怎么验 示意图（第 2 张）

读图看三个细节：第 2 拍 q 停在 MAX，这一拍 carry 应当为 1；第 3 拍 q 翻成 0，回卷不是「MAX 之后停住」也不是「跳过 0 直接到 1」；第 5 拍 clr 有效后第 6 拍 q 为 0，且 clr 撤掉后不会自己跳回原来的值。真实的典型 bug 是：MAX 停两拍（多了一级寄存）、回卷到 1（比较值写成了 MAX−1）、carry 电平滞留、清零那一拍仍在加一。减计数方向把序列倒过来：1 → 0 → 15(MAX)，下溢点的判据完全对称。

三、定向打边界：少量用例锁住确定行为 ​

随机化之前先用定向用例把真相表每一行坐实。计数器边界验证的定向集合很小但缺一不可：复位后 q 是否为确定值（不是 X）；从 0 连加走到 MAX、再走一拍确认回卷 0 与 carry 脉冲；从 MAX 连减回 0、再走一拍确认下溢回卷；在 MAX-1 拍加载 MAX、下一拍加，专打「加载值恰好落在边界」；在 q=0 和 q=MAX 两拍分别拉低 cen，确认保持；clr 与 load、clr 与 cen 的冲突组合按优先级各打一次。

定向用例的写法就是 SystemVerilog Testbench 实战 里的 task 封装：把「发激励、等 N 拍、比对 q 和标志」包成 task，每个场景结尾统计 error。边界集合之外的取值空间不要用手补——那是随机的活。

定向阶段还应当顺手收一份「常见缺陷清单」当回归种子：加减方向接反、比较值写成 MAX−1 导致提前一拍回卷、carry 缺复位上电为 X、加载宽于 W 的值时符号处理错误（无符号计数器收到带符号 d）、cen 用门控时钟实现导致使能跳变带出毛刺。这些缺陷在真实项目里反复出现，把对应的反例固定成定向用例，每次改 RTL 都重跑，能挡住绝大部分返工。

四、随机逼近边界 + SVA 锁逐拍行为 ​

纯随机驱动一个 16 位计数器，均匀分布下恰好走到 MAX 的概率是 1/65536，回卷拍可能几万条用例都遇不到一次。所以随机激励要带约束、带「贴边」倾向，做法见 受约束随机验证 CRV：给 load 值加权，让 0、1、MAX、MAX−1 出现概率远高于中间值；控制信号用 solve...before 或每拍独立加权，保证 clr/load 偶尔打架但不永远打架；跑一段长使能窗口让计数器自己连续爬到边界，再随机插入停顿。

随机管「场景走到没走到」，SVA（SystemVerilog Assertion，立即/并发断言）管「每一拍行为对不对」。计数器边界验证最值钱的几条断言：

systemverilog
// 使能且无清零/加载时，加计数每拍严格 +1
a_up_step: assert property (
  @(posedge clk) disable iff (!rst_n)
  (cen && !clr && !load && up_down) |=> q == ($past(q) + 1))
  else $error("up step fail at %0t: %0d -> %0d", $time, $past(q), q);

// 上溢回卷：本拍在 MAX 且继续加，下一拍必须是 0
a_wrap_up: assert property (
  @(posedge clk) disable iff (!rst_n)
  (cen && !clr && !load && up_down && q == MAX) |=> q == 0);

// 下溢回卷：本拍在 0 且继续减，下一拍必须是 MAX
a_wrap_dn: assert property (
  @(posedge clk) disable iff (!rst_n)
  (cen && !clr && !load && !up_down && q == 0) |=> q == MAX);

// 使能关闭时无条件保持
a_hold: assert property (
  @(posedge clk) disable iff (!rst_n)
  !cen |=> $stable(q));

断言绑定在 DUT 上随仿真即时报错，错误时间点就是肇事拍，不用事后翻波形。更多绑定写法见 SVA 断言实战。

五、覆盖率回答「边界真的走到了吗」 ​

没有覆盖率，「跑了随机」只是心理安慰。计数器边界验证的功能覆盖至少要有：值域 coverpoint 分桶，把 0、1、MAX−1、MAX 单独立仓，中间值一个仓；控制组合 coverpoint 覆盖 {cen, clr, load} 的合法组合；方向 coverpoint；最关键的是 cross——把边界值与控制动作交叉：

systemverilog
covergroup cg_counter @(posedge clk);
  cp_val: coverpoint q {
    bins zero = {0}; bins one = {1};
    bins maxm1 = {MAX-1}; bins maxv = {MAX};
    bins mid = default;
  }
  cp_act: coverpoint {cen, clr, load} {
    bins hold   = {3'b000};
    bins count  = {3'b100};
    bins load_  = {3'b101};
    bins clear  = {3'b110, 3'b111};
  }
  cp_dir: coverpoint up_down;
  cx_boundary: cross cp_val, cp_act;   // MAX/0 上发生加载、清零、计数都要命中
  cx_wrap: cross cp_val, cp_dir {
    ignore_bins no_wrap = cp_act with (!(cp_act inside {count}));
  }
endgroup

cross 的意义在于：q=MAX 被覆盖过、load 也被覆盖过，不等于「在 MAX 那一拍执行加载」被覆盖过。回卷事件（MAX 且加使能、0 且减使能）建议再用 cover property 单独收，覆盖率模型与用法见 代码功能覆盖率实战。回归停止条件是这些边界仓和 cross 全部命中，而不是用例条数达标。

六、参考模型逐拍比对 ​

最后一道兜底是独立参考模型：在 TB 里用一个软件变量记录期望值，每拍按真相表更新，与 DUT 的 q、carry、borrow 逐拍比对。参考模型必须照规格重写，不能把 RTL 的 always 块抄一遍，否则设计理解错了两边一起错。

systemverilog
bit [W-1:0] exp_q;
always @(posedge clk) begin
  if (!rst_n)               exp_q <= '0;
  else if (cen && clr)      exp_q <= '0;
  else if (cen && load)     exp_q <= d;
  else if (cen && up_down)  exp_q <= exp_q + 1'b1;
  else if (cen)             exp_q <= exp_q - 1'b1;
end
a_score: assert property (
  @(posedge clk) disable iff (!rst_n) q === exp_q)
  else $error("q mismatch t=%0d exp=%0d got=%0d", $time, exp_q, q);

断言抓「局部规则被破坏」，参考模型抓「积分性偏差」——某拍只偏差了一点点、后面一直带着错走，单步断言未必触发，逐拍比对一定抓到。参考模型还要单独模拟 carry/borrow 的脉冲宽度，防止标志本身对、却多挂了一拍。两者叠加，加上覆盖率对场景的闭环，计数器这种小模块可以做到收敛后近乎零漏验。

这一篇在知识体系里的位置 ​

平台基础见 SystemVerilog Testbench 实战；加权随机与约束写法见 受约束随机验证 CRV；断言属性与 bind 见 SVA 断言实战；coverpoint/cross 的闭环方法见 代码功能覆盖率实战。同一套「真相表 + 边界定向 + 贴边随机 + 断言 + cross + 参考模型」的套路，原样可迁移到 FIFO 读写指针、PWM 占空比、时钟分频与各类硬件定时器模块。

总结 ​

计数器边界验证的核心是把火力集中在 0、MAX、MAX−1 这几个值与 clr/load/cen 组合的交叉拍上：先用真相表和定向用例坐实优先级与回卷（MAX+1→0、0−1→MAX），再用加权随机让激励主动贴边、用 SVA 死锁「使能时每拍严格 ±1、回卷次态确定、失能保持」，用 coverpoint 加 cross 证明边界事件真的被命中，最后用独立参考模型逐拍比分兜底；模块虽小，这套断言加覆盖率双闭环的流程就是更大子系统验证的缩影。