Mice on USB

Chapter 15.2 built a device that reports state. A keyboard says these keys are down right now, and the deepest property of that design is the one that made it forgiving: a lost report is immediately superseded by the next one, because the next one describes the same thing.

A mouse reports something else, and the difference is not a detail. A mouse says I moved this far since you last asked. Two reports never describe the same interval, so a report that is lost is distance that no later report contains. Nothing supersedes it. Nothing repairs it.

That one property forces three hardware decisions that a keyboard never has to make, and this chapter is those three decisions.

1. A Relative Report Cannot Be Resent

Put the two device classes side by side at the only place that matters — what happens when a report does not reach the host.

The last row is the whole design. Because a mouse's reports partition time into intervals, and because the device has no way to resend an interval it has already described, the device's only defence is to not lose motion in the first place — which means motion must be held in hardware from the moment the sensor produces it until the moment the host actually takes it.

2. The Boot Mouse Report Is Three Bytes

The HID boot protocol mouse report is deliberately tiny, and every field in it is chosen:

Byte 0 and bytes 1–2 are different kinds of thing in the same report, and confusing them is a real design error rather than a pedantic distinction.

The buttons are state. Whether the left button is down is a fact about now, exactly like a key being down. It is not accumulated, it is not cleared by being read, and a lost button report is repaired by the next one.

The displacements are motion. They are accumulated, they are cleared by being read, and a lost one is gone.

One three-byte report carries a self-repairing field and a non-self-repairing field side by side, and the hardware must treat them differently even though they travel together.

The signed encoding is the second decision. Motion has direction, so the field must represent negative values, and it does so in two's complement. That makes the range −128 to +127 — deliberately asymmetric, because two's complement is, and §4 shows that the asymmetry is not merely cosmetic.

3. Why the Device Must Accumulate

Chapter 15.1 established the property that makes accumulation mandatory: the device does not know when the next poll will arrive. It knows its endpoint's requested interval, but the interval is an upper bound on the gap the host promised, not a schedule the device can see.

So consider the sensor producing motion between two polls:

• The optical sensor produces displacement at its own rate — typically far faster than the polling rate.
• The host asks at the schedule's rate.
• The two rates are unrelated, and the fast one is the sensor.

Between two polls the sensor may produce many displacements, and the report has room for exactly one. The device therefore has only two choices, and one of them is wrong:

Report the most recent displacement and discard the rest. The pointer moves less far than the hand did. Every discarded displacement is distance the user produced and the screen never showed. This is not a rounding error; at a 125 Hz poll and a 1000 Hz sensor it discards roughly seven eighths of the motion.

Sum the displacements and report the sum. The report describes the whole interval, which is exactly what a relative report claims to describe. The sum is the only answer consistent with the encoding's own meaning.

4. Saturate, Never Wrap

The accumulator is eight bits signed, so a sufficiently fast hand overflows it. What the hardware does at that boundary is the chapter's sharpest design decision, and the two candidates produce opposite errors.

Wrap is what an ordinary adder does for free: +127 plus +1 becomes −128. In a mouse that means a fast rightward flick reports a large leftward motion. The pointer does not lag — it jumps backwards, hard, in the direction opposite to the hand.

Saturate clamps at the limit: +127 plus +1 stays +127. The reported motion is less than the true motion, so the pointer lags the hand and arrives short.

The decisive row is direction, not magnitude. A saturating error is an underestimate of a correct-direction motion, and a human closing a loop by hand corrects it without noticing, because moving further produces more motion in the same direction. A wrapped error is a correct-magnitude motion in the wrong direction, and the user's correction — moving further the same way — produces another wrap.

Saturation degrades; wrapping inverts. A control loop with a human in it absorbs the first and is destabilised by the second.

And the asymmetry of two's complement is now load-bearing. Saturation limits are +127 and −128, not ±127. Writing the clamp symmetrically is a real bug: it makes −128 — a value the encoding can represent and the sensor can produce — unreachable, so a full-speed leftward motion reports one count less than a full-speed rightward one. §12's mutation M1 is the wrap-versus-saturate choice measured directly.

5. The Collision: Motion and Poll in the Same Cycle

Here is the case that does not exist in a keyboard at all, and it is where this design is most often wrong.

The host's poll takes the report. In the same clock cycle, the sensor delivers new motion. The accumulator must be cleared, because what it held has now been sent. The new motion must be kept, because it has not. Both are true simultaneously, and a design that writes the clear and the accumulate as two arms of the same if will do only one of them.

There are three possible behaviours and only one is correct:

The third is the only one consistent with what the two events actually mean. The poll is a statement about the interval that just ended; the motion belongs to the interval that just began. They do not conflict — they belong to different intervals, and the hardware's job is to put each in the right one.

6. The Hardware, Before Any Language

Three registers and a rule. Written out plainly, before any syntax:

State retained: two signed 8-bit accumulators, acc_x and acc_y, and one sticky flag sat recording that a clamp occurred since the last report.

On reset, or on a USB bus reset: all three clear. A bus reset ends the device's relationship with the host, and motion accumulated for a host that is no longer listening is not motion for the next one.

On a poll that takes the report, with simultaneous motion: the accumulators load the new motion, and sat clears. The report already on the output carried the old value.

On a poll that takes the report, with no motion: the accumulators clear, and sat clears.

On motion with no poll: the accumulators take the saturating sum of their current value and the new displacement, and sat sets if either axis clamped.

On neither: hold.

The outputs are combinational: the report's displacement fields are the accumulators themselves, and the buttons pass straight through from the input, unaccumulated and unlatched.

7. Verilog

The RTL contract

• What it models: the delta accumulator behind a HID boot-mouse interrupt endpoint.
• Why it exists: because a relative report must describe a whole interval (§3) and must not lose motion to a simultaneous poll (§5).
• Inputs: motion_valid with signed motion_dx / motion_dy from the sensor; report_taken, one cycle, asserted when the endpoint's data has actually been accepted; buttons; bus_reset.
• State retained: acc_x, acc_y, sat_r.
• Outputs: rpt_dx, rpt_dy, rpt_buttons, saturated.
• Hardware implied: two 8-bit registers, two 9-bit adders with clamp logic, one flag flop, one mux layer for the collision case.
• Reset: asynchronous active-low rst_n; bus_reset is a synchronous equivalent.
• Assumptions: report_taken is a single-cycle pulse asserted once per delivered report, and it means delivered, not attempted — see §16.
• Omissions: no wheel, no report-protocol mode, no descriptor logic, no clock-domain crossing from the sensor.
• What DV should verify: that motion is never lost and never double-counted across every alignment of motion_valid and report_taken; that both clamp limits are reachable and correct; that saturated reports clamping and only clamping.

module hid_mouse_delta (
  input  wire              clk,
  input  wire              rst_n,
  input  wire              bus_reset,
  input  wire              motion_valid,
  input  wire signed [7:0] motion_dx,
  input  wire signed [7:0] motion_dy,
  input  wire              report_taken,
  input  wire [2:0]        buttons,
  output wire [2:0]        rpt_buttons,
  output wire signed [7:0] rpt_dx,
  output wire signed [7:0] rpt_dy,
  output wire              saturated
);
  // The boot mouse report carries SIGNED 8-bit deltas: -128 .. +127.
  localparam signed [7:0] DMAX =  8'sd127;
  localparam signed [7:0] DMIN = -8'sd128;

  reg signed [7:0] acc_x, acc_y;
  reg              sat_r;

  assign rpt_buttons = buttons;   // buttons are STATE: never accumulated
  assign rpt_dx      = acc_x;
  assign rpt_dy      = acc_y;
  assign saturated   = sat_r;

  // Saturating signed add, in 9 bits so the overflow is visible before it
  // is discarded. Written as a function so both axes use the SAME logic.
  function signed [7:0] sat_add;
    input signed [7:0] a;
    input signed [7:0] b;
    reg signed [8:0] sum;
    begin
      sum = {a[7], a} + {b[7], b};
      // NOTE the SIGNED literals. Writing {1'b0, DMAX} here would make the
      // comparison UNSIGNED -- a concatenation is unsigned in Verilog, and
      // one unsigned operand poisons the whole expression. Section 11 is
      // the account of getting this wrong.
      if (sum > 9'sd127)       sat_add = DMAX;
      else if (sum < -9'sd128) sat_add = DMIN;
      else                     sat_add = sum[7:0];
    end
  endfunction

  function would_saturate;
    input signed [7:0] a;
    input signed [7:0] b;
    reg signed [8:0] sum;
    begin
      sum = {a[7], a} + {b[7], b};
      would_saturate = (sum > 9'sd127) || (sum < -9'sd128);
    end
  endfunction

  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      acc_x <= 8'sd0; acc_y <= 8'sd0; sat_r <= 1'b0;
    end else if (bus_reset) begin
      acc_x <= 8'sd0; acc_y <= 8'sd0; sat_r <= 1'b0;
    end else begin
      // THE COLLISION RULE. A report and a motion in the same cycle: the
      // report carries what was accumulated, and the new motion starts the
      // NEXT accumulation. Motion is never discarded -- a relative delta
      // that is dropped is distance the host can never recover.
      if (report_taken && motion_valid) begin
        acc_x <= motion_dx;
        acc_y <= motion_dy;
        sat_r <= 1'b0;
      end else if (report_taken) begin
        acc_x <= 8'sd0; acc_y <= 8'sd0; sat_r <= 1'b0;
      end else if (motion_valid) begin
        acc_x <= sat_add(acc_x, motion_dx);
        acc_y <= sat_add(acc_y, motion_dy);
        if (would_saturate(acc_x, motion_dx) ||
            would_saturate(acc_y, motion_dy)) sat_r <= 1'b1;
      end
    end
  end
endmodule

Two details are worth naming.

The 9-bit intermediate. sum is one bit wider than either operand, which is what makes the overflow observable. Adding two 8-bit values into an 8-bit result destroys the very information the clamp needs. The sign-extension {a[7], a} is explicit because the widening must preserve the value, not the bit pattern.

would_saturate recomputes the sum. That is deliberate redundancy for readability, and synthesis shares the adder. Writing the flag from sat_add's internals would require the function to return two things, which Verilog makes ugly; §8 shows SystemVerilog does not make it much better.

8. SystemVerilog

Same hardware. What changes is that the report becomes a type rather than three separate wires, and the intent of each block is stated rather than inferred.

package hid_mouse_pkg;
  // The boot mouse report: a button bitmap and two SIGNED 8-bit deltas.
  typedef struct packed {
    logic signed [7:0] dy;
    logic signed [7:0] dx;
    logic        [7:0] buttons;
  } mouse_report_t;

  localparam logic signed [7:0] DMAX =  8'sd127;
  localparam logic signed [7:0] DMIN = -8'sd128;
endpackage

module hid_mouse_delta_sv
  import hid_mouse_pkg::*;
(
  input  logic              clk,
  input  logic              rst_n,
  input  logic              bus_reset,
  input  logic              motion_valid,
  input  logic signed [7:0] motion_dx,
  input  logic signed [7:0] motion_dy,
  input  logic              report_taken,
  input  logic        [2:0] buttons,
  output mouse_report_t     report_o,
  output logic              saturated
);
  logic signed [7:0] acc_x, acc_y;
  logic              sat_q;

  assign report_o.buttons = {5'b0, buttons};  // buttons are STATE
  assign report_o.dx      = acc_x;
  assign report_o.dy      = acc_y;
  assign saturated        = sat_q;

  function automatic logic signed [7:0] sat_add(input logic signed [7:0] a,
                                                input logic signed [7:0] b);
    logic signed [8:0] sum;
    begin
      sum = 9'(a) + 9'(b);
      if      (sum > 9'sd127)  return DMAX;
      else if (sum < -9'sd128) return DMIN;
      else                     return sum[7:0];
    end
  endfunction

  function automatic logic would_saturate(input logic signed [7:0] a,
                                          input logic signed [7:0] b);
    logic signed [8:0] sum;
    begin
      sum = 9'(a) + 9'(b);
      return (sum > 9'sd127) || (sum < -9'sd128);
    end
  endfunction

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      acc_x <= '0; acc_y <= '0; sat_q <= 1'b0;
    end else if (bus_reset) begin
      acc_x <= '0; acc_y <= '0; sat_q <= 1'b0;
    end else if (report_taken && motion_valid) begin
      acc_x <= motion_dx;
      acc_y <= motion_dy;
      sat_q <= 1'b0;
    end else if (report_taken) begin
      acc_x <= '0; acc_y <= '0; sat_q <= 1'b0;
    end else if (motion_valid) begin
      acc_x <= sat_add(acc_x, motion_dx);
      acc_y <= sat_add(acc_y, motion_dy);
      if (would_saturate(acc_x, motion_dx) ||
          would_saturate(acc_y, motion_dy)) sat_q <= 1'b1;
    end
  end
endmodule

What the packed struct actually buys, and what it does not.

It buys one name for the thing that crosses the interface. The testbench compares report_o against a predicted mouse_report_t in a single expression, and §11 shows that this changes the shape of a failure message. It also documents the byte order of the report in the type itself rather than in a comment.

It does not buy correctness. The struct is packed, so it is a bit vector with a name; nothing in it prevents the signedness error of §11, because dx is declared signed but an expression that reads it can still be evaluated unsigned.

9'(a) replaces {a[7], a}. The cast widens by the operand's own signedness rather than by an explicit sign bit, so it cannot disagree with the declaration. This is a genuine improvement: the Verilog version is correct but its correctness depends on the author having written a[7] rather than 1'b0.

9. VHDL

Same hardware again, and the language differs from both the others in a way that matters to §11.

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

entity hid_mouse_delta_vhdl is
  port (
    clk          : in  std_logic;
    rst_n        : in  std_logic;
    bus_reset    : in  std_logic;
    motion_valid : in  std_logic;
    motion_dx    : in  signed(7 downto 0);
    motion_dy    : in  signed(7 downto 0);
    report_taken : in  std_logic;
    buttons      : in  std_logic_vector(2 downto 0);
    report_btn   : out std_logic_vector(7 downto 0);
    report_dx    : out signed(7 downto 0);
    report_dy    : out signed(7 downto 0);
    saturated    : out std_logic
  );
end entity;

architecture rtl of hid_mouse_delta_vhdl is
  constant DMAX : signed(7 downto 0) := to_signed(127, 8);
  constant DMIN : signed(7 downto 0) := to_signed(-128, 8);

  signal acc_x, acc_y : signed(7 downto 0) := (others => '0');
  signal sat_q        : std_logic := '0';

  -- resize() to 9 bits makes the overflow visible before it is discarded;
  -- both comparison operands are SIGNED, so no signedness question arises.
  function sat_add (a : signed(7 downto 0); b : signed(7 downto 0))
    return signed is
    variable sum : signed(8 downto 0);
  begin
    sum := resize(a, 9) + resize(b, 9);
    if    sum > to_signed(127, 9)  then return DMAX;
    elsif sum < to_signed(-128, 9) then return DMIN;
    else  return sum(7 downto 0);
    end if;
  end function;

  function would_saturate (a : signed(7 downto 0); b : signed(7 downto 0))
    return boolean is
    variable sum : signed(8 downto 0);
  begin
    sum := resize(a, 9) + resize(b, 9);
    return (sum > to_signed(127, 9)) or (sum < to_signed(-128, 9));
  end function;
begin
  report_btn <= "00000" & buttons;   -- buttons are STATE, never accumulated
  report_dx  <= acc_x;
  report_dy  <= acc_y;
  saturated  <= sat_q;

  process (clk, rst_n)
  begin
    if rst_n = '0' then
      acc_x <= (others => '0');
      acc_y <= (others => '0');
      sat_q <= '0';
    elsif rising_edge(clk) then
      if bus_reset = '1' then
        acc_x <= (others => '0');
        acc_y <= (others => '0');
        sat_q <= '0';
      elsif report_taken = '1' and motion_valid = '1' then
        -- THE COLLISION RULE: the report carries what was accumulated, and
        -- the simultaneous motion STARTS the next accumulation.
        acc_x <= motion_dx;
        acc_y <= motion_dy;
        sat_q <= '0';
      elsif report_taken = '1' then
        acc_x <= (others => '0');
        acc_y <= (others => '0');
        sat_q <= '0';
      elsif motion_valid = '1' then
        acc_x <= sat_add(acc_x, motion_dx);
        acc_y <= sat_add(acc_y, motion_dy);
        if would_saturate(acc_x, motion_dx) or
           would_saturate(acc_y, motion_dy) then
          sat_q <= '1';
        end if;
      end if;
    end if;
  end process;
end architecture;

resize instead of concatenation. resize(a, 9) on a signed value sign-extends — the function is defined for the type, so widening cannot silently become zero-extension. In Verilog the author chooses the extension bit and can choose wrong; in VHDL the type chooses it.

signed is a type here, not an attribute of a declaration. motion_dx is not "a vector the designer intends to read as signed" — it is signed, and numeric_std defines arithmetic and comparison operators for that type and not for mixtures of it with unsigned. §10 is precisely about what that does and does not prevent.

10. Comparing the Three

The third row is the one to read twice, and it is the reason this chapter's real bug (§11) has three different lives in three languages.

11. The Testbenches, and the Bug One of Them Found

Each language has its own bench, and all three share one structural decision: the reference model does not use the design's method.

The design saturates by widening to nine bits and clamping. Every bench instead accumulates in a wide integer and clamps at the end — Verilog in an integer, SystemVerilog in an int, VHDL in an integer. That is not a stylistic preference. A model that reproduced the 9-bit clamp would reproduce a 9-bit clamp's bugs, and the divergence that follows is the proof that it does not.

  // SystemVerilog bench: a DIFFERENT method, not a transcription of the RTL.
  int model_x = 0, model_y = 0;

  function automatic int clamp(input int v);
    if (v >  127) return  127;
    if (v < -128) return -128;
    return v;
  endfunction

  task automatic move(input logic signed [7:0] dx, input logic signed [7:0] dy);
    begin
      motion_dx=dx; motion_dy=dy; motion_valid=1;
      @(posedge clk); #1; motion_valid=0; #1;
      model_x = clamp(model_x + dx);      // wide add, clamp afterwards
      model_y = clamp(model_y + dy);
    end
  endtask

  task automatic move_and_take(input logic signed [7:0] dx,
                               input logic signed [7:0] dy);
    begin
      motion_dx=dx; motion_dy=dy; motion_valid=1; report_taken=1;
      @(posedge clk); #1; motion_valid=0; report_taken=0; #1;
      model_x = dx;   // the collision: the new motion STARTS the next report
      model_y = dy;
    end
  endtask

Each bench drives the same scenario list: accumulation, report-clears, button pass-through, positive and negative saturation, the exact limits, one count beyond each limit, the §5 collision, bus reset, and then 1500 randomised operations in which polls, motions and collisions are drawn at random so that every alignment occurs many times.

What happened on the first run

The Verilog design failed with 731 errors, on the very first check after reset.

The bench was right and the RTL was wrong, and the wrong line was this one:

      if (sum > {1'b0, DMAX})       sat_add = DMAX;   // WRONG
      else if (sum < {1'b1, DMIN})  sat_add = DMIN;   // WRONG

A concatenation in Verilog is unsigned. Always — regardless of the signedness of what goes into it. And in Verilog, one unsigned operand makes the entire expression unsigned, so sum, declared reg signed [8:0], was being read as an unsigned 9-bit number. Every negative accumulation became a large positive one and clamped instantly to +127.

Rather than reason about it, I isolated it:

  // sum is reg signed [8:0], set to -200
  s > 9'sd127        -> 0    // signed literal: correct
  s > {1'b0, DMAX}   -> 1    // concat: UNSIGNED, -200 reads as 312
  s > $signed({1'b0, DMAX}) -> 0    // concat, signedness restored

The third line is the fix that does not change the value — $signed() re-interprets the same bits — which is what confirms the diagnosis is about interpretation and not about arithmetic.

The fix was the signed literals now shown in §7, after which the Verilog bench reported 0 errors, and the SystemVerilog and VHDL designs — written afterwards — never carried the defect.

12. Mutation Testing

Six mutations, each applied to both the Verilog and the SystemVerilog design and run against that language's own bench. The baseline is clean in both, which is what makes the numbers mean anything.

M6 is the real bug, put back deliberately so its detectability is measured rather than assumed. Its Verilog count of 733 is within two of the 731 originally observed — the small difference is the two extra checks the bench gained afterwards.

M1, M2, M3 and M6 all produce three-figure counts because they corrupt a value the randomised loop checks 1500 times. That is what a well-covered defect looks like, and it is worth contrasting with the next two.

13. The Mutation That Barely Died

M4 and M5 were killed by 3 and 2 failures out of more than 1500 checks. They passed, but only just, and why is a finding.

M4 removes the saturation flag while leaving the clamp correct. The clamped values are checked 1500 times by the randomised loop; the flag that reports the clamping is checked four times, all of them in directed tests. The randomised stimulus exercises saturated constantly and verifies it never.

Worse, look at which of the four fired:

  FAIL: saturation must be reported            (t=87000)
  FAIL: negative saturation must be reported   (t=127000)
  FAIL: one beyond the limit is saturation     (t=177000)

Three, not four. The missing one is the check that reaching +127 exactly is not saturation — and a flag stuck at zero satisfies it perfectly.

A check written to catch a false positive is structurally blind to a permanent false negative. It can only ever fail when the flag is set, so a flag that is never set can never fail it.

M5 latches the buttons instead of passing them through and dies on a single check, because the buttons are driven once and never randomised. The randomised loop varies the deltas — the interesting part — and holds the boring part constant, so the boring part is nearly unverified.

And a third defect, in the bench's own reporting

While reading M4's output, the original messages came out as tive saturation must be reported and e beyond the limit is saturation.

The Verilog bench was truncating its own diagnostics. A string argument in Verilog is a fixed-width vector — the task declared input [255:0] msg, which is 31 characters — and a longer message is silently clipped from the left, discarding exactly the beginning that says which check it was.

  // NOTE: 80 characters. A Verilog string argument is a fixed-width vector,
  // and a message longer than the declared width is truncated FROM THE LEFT
  // with no warning -- the bench quietly lies about which check failed.
  task check(input cond, input [639:0] msg);

Nothing detected this, because nothing checks the reports. The pass/fail verdict was always correct; only the explanation was wrong. It surfaced solely because a mutation run produced failures and the failures were read.

This is the printed-not-checked quantity blind spot from Chapter 14 appearing in the verification code rather than the design — and it is worse there, because a bench that misreports which check failed sends the next engineer to the wrong module.

14. Assertions

The properties worth asserting are the ones §5 and §4 make non-obvious.

  // A1. The collision rule: motion arriving with a poll is never discarded.
  property p_collision_keeps_motion;
    @(posedge clk) disable iff (!rst_n || bus_reset)
      (report_taken && motion_valid) |=>
        (acc_x == $past(motion_dx)) && (acc_y == $past(motion_dy));
  endproperty
  a_collision_keeps_motion: assert property (p_collision_keeps_motion);

  // A2. A poll without motion always empties the accumulator.
  property p_report_clears;
    @(posedge clk) disable iff (!rst_n || bus_reset)
      (report_taken && !motion_valid) |=> (acc_x == 0) && (acc_y == 0);
  endproperty
  a_report_clears: assert property (p_report_clears);

  // A3. Saturation, not wrap: an accumulation NEVER reverses sign unless the
  //     applied delta could account for it. This is the property that
  //     distinguishes the two candidate behaviours of section 4 directly.
  property p_no_sign_inversion;
    @(posedge clk) disable iff (!rst_n || bus_reset)
      (motion_valid && !report_taken && $past(acc_x) > 0 && motion_dx > 0)
        |=> (acc_x > 0);
  endproperty
  a_no_sign_inversion: assert property (p_no_sign_inversion);

  // A4. The flag means what it says, in BOTH directions -- the second
  //     implication is the one section 13 found missing from the bench.
  //     The two helpers are computed HERE, from the interface, and must
  //     NOT call the design's would_saturate() -- a property that asks the
  //     design whether it should have clamped cannot detect a design that
  //     is wrong about when to clamp. Wider signed arithmetic, as in the
  //     reference model of section 11.
  wire signed [8:0] nx = $signed({rpt_dx[7], rpt_dx}) +
                         $signed({motion_dx[7], motion_dx});
  wire signed [8:0] ny = $signed({rpt_dy[7], rpt_dy}) +
                         $signed({motion_dy[7], motion_dy});
  wire would_sat_x = (nx > 9'sd127) || (nx < -9'sd128);
  wire would_sat_y = (ny > 9'sd127) || (ny < -9'sd128);

  property p_sat_iff_clamped;
    @(posedge clk) disable iff (!rst_n || bus_reset)
      (motion_valid && !report_taken) |=>
        (saturated == ($past(saturated) ||
                       $past(would_sat_x) || $past(would_sat_y)));
  endproperty
  a_sat_iff_clamped: assert property (p_sat_iff_clamped);

Assertion contracts

A3 is the one to study. It does not test the clamp's value — it tests that the sign cannot invert, which is §4's distinction stated as a temporal property. Under M1 (wrap), +127 plus +1 gives −128 and A3 fires immediately. It is a weaker claim than checking the clamped value and a far more targeted one: it catches wrapping and nothing else, so when it fires you already know what happened.

A4 states the biconditional that §13 found the bench missing. The bench checked only that the flag sets when it should; A4 also requires that it does not set when it should not, and that it persists until a report. Written as one equality, both directions come for free.

15. Verification: Does UVM Earn Its Place Here?

Chapter 15.2 §13 argued that UVM starts to pay for itself when the transaction is not the pins — a keyboard's pins are a bit vector while the transaction is a set.

A mouse makes a different and stronger case, and it is worth being precise about which.

The argument that does not work: "the report is a struct, so it needs a transaction class." It does not. A three-byte packed struct compared against a predicted struct is one line of SystemVerilog, and wrapping it in a uvm_sequence_item buys nothing.

The argument that does work: the property being verified spans an unbounded number of transactions. §1's requirement is not this report is correct — it is "the sum of all reported motion equals the sum of all sensor motion, for every interval, forever." That is a claim about a stream, and it needs an agent that observes the whole stream and a scoreboard that maintains a running total.

The monitor must observe, not predict. If the mouse monitor is handed the driver's motion values, the scoreboard compares the driver against itself and the entire §11 signedness bug is invisible — the model and the design would both be fed the same numbers and asked only whether the design copied them. The monitor's input must be the report pins, decoded as a host would decode them.

And the reference model must not be the RTL again. §11 is the evidence: the bench caught a real defect because it accumulated in a wide integer instead of nine bits. A scoreboard that models saturation the way the design implements it would have clamped identically and reported zero divergences against a design that was clamping every negative value to +127.

The scoreboard's independence is not a code-quality preference. It is the mechanism that found this chapter's bug, and §12's M6 measures exactly how much it was worth: 733 failures the shared-method model would have scored as zero.

16. Debugging: The Mouse That Jumps Backwards

A mouse works perfectly in normal use. Under fast movement — a quick flick across a large screen — the pointer occasionally jumps far in the opposite direction. It is intermittent, it correlates with speed, and the sensor tests clean on its own bench.

Read the symptom against §4 before touching anything. Opposite direction is the signature. A lost report makes the pointer lag; a double-counted report makes it overshoot; only an overflow makes it reverse, because only an overflow turns a large positive into a large negative.

And "correlates with speed" confirms it, because speed is what fills the accumulator. The bug is not in the sensor, which is why the sensor's own bench is clean: the sensor is producing correct displacements and something downstream is summing them into eight bits without a clamp.

Where to look, in order:

The accumulator's clamp. Is there one at all? An adder written as acc <= acc + delta wraps by construction and is the single most likely cause.

The clamp's limits. If it clamps at ±127, the negative direction still has a reachable value the design refuses to produce — less dramatic than a wrap but still wrong.

The clamp's signedness. §11's defect, which produces the opposite symptom — everything pinned to +127, a pointer that only ever drifts one way — so if the symptom is reversal rather than drift, this is not it. The distinction is diagnostic, and knowing both failure signatures tells the two apart before opening the source.

The report_taken qualifier. The subtler cause, and it fails the RTL contract in §7 rather than the arithmetic. If report_taken is asserted when a poll is attempted rather than when the data is accepted, then a NAKed or errored transaction clears an accumulator whose contents were never delivered. The pointer then loses motion under load — which is lag, not reversal, but the two can coexist and the lag is easy to blame on the sensor.

17. Tooling, Honestly

The VHDL was not executed, and that is stated rather than implied. No VHDL analyser or simulator is present in this environment — ghdl, nvc, vcom, xvhdl and vsim were each checked and none exists — and installing one was out of scope. No claim is made anywhere in this chapter that the VHDL simulated cleanly, because it was never run.

What was done instead is a structural review against the properties a compiler would check: every entity has an architecture; the instantiation's positional association matches the port declaration in count and order; every input port is driven and every output port is actually checked by the bench; no deprecated arithmetic package is used anywhere and numeric_std is used in both files; the asynchronous-reset process is sensitive to both clk and rst_n; every signal the process assigns has a reset value; and every saturation comparison uses to_signed on both sides.

The review script had a blind spot of its own, which is worth recording in the same spirit: it flagged would_saturate as lacking a return on every path, because it searched for an else. The function is a single return (a) or (b); with no branches at all. A heuristic checker that assumes structure finds fault with code that has none — the checker was wrong and the VHDL was right.

One real defect was fixed by the review: the VHDL bench originally kept its error count and its model in signals, and a signal assignment does not take effect until the process waits. Two checks failing before the next wait would each compute errors + 1 from the same stale value, and the second would overwrite the first — the count would silently under-report. They are process variables now.

18. Common Misconceptions

"The accumulator is an optimisation for slow hosts." It is what makes the report true (§3). Without it the device reports one sensor sample and claims it is an interval's total.

"Saturation and wrapping differ only in accuracy." They differ in direction (§4). One produces a short move; the other produces a move the user did not make, the opposite way.

"Clamping at ±127 is close enough." −128 is representable, reachable and legitimate. Refusing to produce it makes leftward motion measurably weaker than rightward.

"Declaring the accumulator signed makes the arithmetic signed." It does not, in Verilog. §11 is a working design with a correct declaration and an expression that read it unsigned anyway.

"A struct in SystemVerilog would have prevented the signedness bug." It would not. §8 says so explicitly: a packed struct is a named bit vector, and the field's declared signedness does not govern how an expression elsewhere is evaluated.

"A simultaneous poll and motion is too rare to matter." At 125 polls per second it happens several times a minute (§5), and the mutation that breaks it costs 284 and 701 failures (§12).

"The buttons need the same treatment as the deltas." They are the opposite kind of field (§2) — state, not motion — and latching them is mutation M5.

19. Exercises

1. Extend the design with a scroll wheel as a fourth signed byte. The wheel's range is much smaller in practice — decide whether it needs its own saturation limits or shares the deltas', and justify the answer from §4's argument rather than from convenience.

2. Implement the §13 fix: make the reference model predict saturated and buttons on every cycle, then re-run M4 and M5. Predict the new failure counts before running, then compare.

3. Implement A4 from §14 as a procedural check in the SystemVerilog bench — the biconditional, both directions — and find a mutation that A4 kills and no existing check does.

4. Build the §5 collision deliberately wrong in the other direction (the accumulate wins, so the motion is counted twice) and measure it. Compare its failure count to M2's and explain why the two differ.

5. Write the report_taken-means-attempted defect from §16 and determine what stimulus is required to expose it. Note that it cannot be produced by this bench at all, and say what must be added.

6. Take the VHDL design and hand-simulate the §5 collision on paper for three cycles. Confirm that the elsif chain's order — collision, then report, then motion — is the order that makes it correct, and show what the other two orderings produce.

20. Summary

A relative report cannot be resent, so a mouse must retain motion in hardware from the sensor to the host (§1), and the accumulator is what makes the report's own claim true (§3).

Saturation and wrapping are not two accuracies, they are two failure directions (§4). Wrapping inverts the motion, which a human control loop cannot correct because the correction wraps too. Saturation merely shortens it, which the user absorbs without noticing.

The collision between a poll and a motion is the design's hardest cycle (§5), because both events are legitimate and they belong to different intervals. Getting it wrong loses distance permanently or invents distance that never existed.

All three languages describe identical hardware, and they differ in exactly one place that mattered: what a concatenation does to signedness (§10). Verilog silently converts the enclosing expression to unsigned; VHDL's concatenation carries the operand's type, so the same construct is correct there — not because VHDL catches the bug, but because VHDL does not have it.

The bug was real and the bench found it on its first check (§11) — 731 failures — because the reference model accumulated in a different width than the design did. A model built the design's way would have reported nothing wrong. M6 measures that at 733 failures against zero.

Six mutations, all killed in both languages (§12). Four died by hundreds of failures; two died by three and by two (§13), which exposed a blind spot in the bench rather than in the design: the randomised stimulus varies the primary data and leaves the derived signals to a handful of directed checks. One of those four directed checks turned out to be structurally incapable of catching a stuck-at-zero flag at all.

And the bench was quietly lying about which check failed (§13), because a Verilog string argument is a fixed-width vector that truncates from the left. Nothing detected it, because nothing checks the reports — it surfaced only because a mutation produced failures and somebody read them.

VHDL was written and reviewed but not executed (§17), and no claim to the contrary appears anywhere above.

21. What Comes Next

This chapter and 15.2 built the two canonical interrupt devices and both took the schedule from 15.1 as given — a poll arrives, eventually, within the interval the device asked for.

Chapter 15.4 asks what that interval actually buys, and the answer is smaller than most engineers expect. The endpoint's bInterval bounds one link in a chain that runs from the sensor's own sampling period, through the accumulator built here, through the host controller's schedule, through the driver, to the application that finally reacts.

The interval bounds one link. The user feels the chain. The next chapter takes that budget apart term by term and shows which terms the device controls, which the host controls, and which nobody controls — and why a device that asks for 1 ms does not thereby get a 1 ms response.

Browse the full path on the USB tutorials index.