The handshake contract

A transfer happens on any cycle where valid and ready are both high. Once valid rises, the producer holds valid and the payload steady until ready accepts.

The top two rows make the offer; the multi-bit row carries the data word.

• Slot 0: idle: valid 0, ready 1, no offer.

• Slot 1: valid rises with data 5; ready 0, so the offer waits.

• Slot 2: stall continues; valid and data hold their values.

• Slot 3: ready rises; data 5 is accepted.

• Slot 4: valid drops; the bus idles for one cycle.

• Slot 5: back-to-back traffic starts: data 6 accepted at once.

• Slot 6: data 7 accepted; the throughput case the covers must record.

The checker module

The cover writes ready == 1'b0 inside the repetition: Verilator 5.048 rejects a unary ! inside a sequence, although IEEE 1800 allows it.

The listing is one file you can paste into the Code Lab: the checker first, then a small design and a bench that runs legal traffic before planting one bug at a time. Every rule reports through fail(), which counts and prints the report and lets the run go on; Verilator 5.048 stops at the first $error, and production checkers often count the same way.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46

module vr_checker #(
  parameter int  DW          = 32,
  parameter int  MAX_STALL   = 64
)(
  input logic           clk,
  input logic           rst_n,
  input logic           valid,
  input logic           ready,
  input logic [DW-1:0]  data,
  input logic           last
);
  // Every rule reports through fail(): it counts and prints, and the run goes on.
  // (Verilator stops at the first $error, so a counting report keeps one bench
  // able to plant several bugs. Production checkers often do the same.)
  int n_fail = 0, n_b2b = 0, n_stall = 0;
  function automatic void fail(string msg);
    n_fail++;
    $display("[%0t] vr_checker: %s", $time, msg);
  endfunction

  // R1: valid holds until accepted (covers retraction too)
  a_valid_stable: assert property (@(posedge clk) disable iff (!rst_n)
    (valid && !ready) |-> ##1 valid)
    else fail("valid retracted before ready");

  // R2: payload frozen while the offer is pending
  a_payload_stable: assert property (@(posedge clk) disable iff (!rst_n)
    (valid && !ready) |-> ##1 ($stable(data) && $stable(last)))
    else fail("payload changed during stall");

  // R3: no X on payload while it is being offered (fires on 4-state simulators only)
  a_no_x: assert property (@(posedge clk) disable iff (!rst_n)
    valid |-> (!$isunknown(data) && !$isunknown(last)))
    else fail("X on payload while valid");

  // R4: bounded liveness, accepted within MAX_STALL cycles
  a_accepted: assert property (@(posedge clk) disable iff (!rst_n)
    valid |-> ##[0:MAX_STALL] ready)
    else fail("transfer not accepted within bound");

  // Cover the scenarios that prove the checker saw real traffic
  c_b2b:   cover property (@(posedge clk)
    (valid && ready) ##1 (valid && ready)) n_b2b++;
  c_stall: cover property (@(posedge clk)
    (valid && ready == 1'b0) [*3] ##1 (valid && ready)) n_stall++;
endmodule

legal traffic: 0 failures; covers: back-to-back 1, stall-then-accept 1
[165] vr_checker: valid retracted before ready
[185] vr_checker: payload changed during stall
after one retraction and one payload change: 2 failures
[275] vr_checker: transfer not accepted within bound
[285] vr_checker: transfer not accepted within bound
[295] vr_checker: transfer not accepted within bound
after a 9-cycle stall against a bound of 6: 5 failures (3 reports for one late offer)
PASS: legal traffic passed with both covers hit, and the checker reported each planted bug

The producer-side dependency rule is not checkable from the wires. A producer that waits for ready before raising valid makes traces that also read as legal, so the checker covers valid rising first and relies on the bounded rule to flag the deadlock symptom.

Simulation uses the bounded window form. The unbounded s_eventually form belongs in formal tools, where it is a genuine liveness obligation.

Common mistakes

What the run shows

Legal traffic, including the diagram's stall and a back-to-back run, gives no reports and hits both covers. A retraction and a payload change each give one report, from the rule that owns them. The late offer gives three: R4's antecedent is the level valid, so each stalled cycle opened its own window, and the first three ran out of time. That is the level-antecedent cost from the Implication lessons, seen on a real checker.

R3 never fires on Verilator, which is 2-state: an X on data becomes 0 or 1 before any check sees it. Keep R3; it earns its place on a 4-state simulator.