Protocol Verification

Module 17 · Chapter 17.1 · CHI Verification

Project thread — Module 16 built the RTL. 17.1 is per-flit protocol checking; 17.2 checks coherence invariants.

1. Learning Outcomes

By the end of this chapter you should be able to:

• Explain that protocol verification checks each flit is legal on its channel, independent of coherence.
• Name the per-channel rules — legal opcode, legal field combinations, correct handshake.
• State that a flit's fields must be stable across the valid-until-ready window.
• Explain why an accept-only checker misses a mid-hold field mutation.
• Diagnose the escaped violation from a checker that watches only the accept beat.
• Implement a representative protocol checker in SystemVerilog, Verilog-2001, and VHDL.

2. Why Should I Learn This?

Verification is where a design is proven — or where bugs escape. CHI is uniquely hard to verify because correctness lives at three levels: each flit must be legal (protocol), the caches must stay coherent (invariants), and events must order correctly. This chapter is the bottom layer: per-channel protocol checking, which confirms every flit is well-formed before any coherence reasoning. If a flit is malformed, no coherence check above it is meaningful.

The lesson that matters most is about the checker, not the design. A CHI handshake asserts valid and holds the flit until the receiver accepts it (ready), and the protocol requires the flit's fields to be stable for that whole window — the receiver may sample them at any point. A checker that only validates fields at the accept beat is looking at one instant and misses a bug where a field mutates during the hold. That escaped violation then corrupts the transaction downstream (the receiver sampled the wrong value). This chapter teaches the per-channel monitor and the discipline of checking the whole handshake window — the first way a verification environment either catches bugs or silently lets them through.

3. Key Terms

4. Previous Chapter Connection

This chapter verifies what Module 16 built. Every pipeline there — request (16.1), snoop (16.2), directory (16.3), cache (16.4) — emits flits on the channels of Chapter 6.1, and this monitor checks those flits are well-formed. It is the first gate: legality per flit, before the coherence invariants of Chapter 17.2 or the ordering of Chapter 12.

The handshake and stability rules come from the credit/flow-control mechanics of Module 14. There, a flit was sent against a credit and held in a buffer; here, the verification concern is that while the flit is held (valid asserted, awaiting accept), its fields must not change — because the receiver is entitled to sample them across the whole window (Chapter 14.1). This chapter turns that flow-control property into a checkable rule, and shows the classic way a checker fails to check it. It is the verification counterpart of the RTL discipline the whole prior module built.

5. Core Concept — check the whole handshake, not just accept

Protocol verification flags any flit that is illegal on its channel, and the checker must verify field stability across the entire valid-until-ready window — not only at the accept beat.

• Per-channel legality. Each channel (REQ/RSP/SNP/DAT) has rules: a legal opcode, legal field combinations (e.g. a data-bearing response actually carries data), and a well-formed handshake.
• The handshake holds the flit. Valid is asserted and the flit is held until ready accepts it. The transfer happens at the accept beat (valid AND ready).
• Fields must be stable while held. The protocol requires the flit's fields to stay unchanged from valid-assert to accept — the receiver may sample them at any cycle in the window.
• Check the whole window. The checker must verify stability across valid && !ready (the hold), not just legality at valid && ready (accept). An accept-only check sees one cycle and misses a mid-hold change.

The synthesis:

Protocol verification flags flits that are illegal on their channel — bad opcode, bad field combination, malformed handshake. The subtle checker requirement is field stability: the protocol holds a flit (valid asserted) until accept (ready), and the fields must be stable across that whole window. A checker that validates only at the accept beat misses a field that mutates during the hold — a real violation escapes, and a mis-sampled field corrupts the transaction downstream.

6. Engineering Mental Model — signing a contract that keeps changing

Think of handing someone a contract to sign (the flit), where valid means "here is the contract" and ready/accept means "I have signed it."

• You hold the contract out (valid asserted) and wait for them to read and sign it (ready). The moment they sign is the accept beat.
• The rule: the contract's terms must not change while it is held out for signing. Whatever they read at any moment must be what they eventually sign.
• A careful witness (the checker) watches the whole time the contract is held out, and objects if a clause changes mid-hold — because the signer might have read the old clause.
• A lazy witness only glances at the contract at the instant of signing. If a clause was swapped before the signature but after the signer read it, the lazy witness sees only the final version and certifies it clean — while the signer actually agreed to something else. The tampering escaped.

The careful witness checks the whole hold window; the lazy one checks only the signing instant. The lazy witness is the accept-only checker — it misses the mid-hold field change that the receiver may have already sampled.

7. Engineering Diagram — the per-channel protocol monitor

Three checks per flit; the stability check is the one that spans the whole hold window. Opcode and field-combination checks are single-cycle; stability is temporal. The DebugLab drops the stability check (or applies it only at accept), leaving the mid-hold mutation unseen.

8. The Per-Channel Rule Classes

The categories of protocol rule a monitor checks.

The rule to carry: some rules are instantaneous and some are temporal, and the temporal ones are where checkers fail. Opcode and field-combination legality can be checked in one cycle. But stability and handshake rules are multi-cycle — they constrain how signals behave over the hold window. A checker that treats every rule as instantaneous (checking only at accept) will verify the instantaneous rules correctly and silently skip the temporal ones. The escaping bug is always a temporal one — a field that was legal at accept but changed on the way there.

9. Why Accept-Only Checking Misses the Bug

The hole, made explicit.

• The receiver samples across the window. The receiving RTL may latch a field on any cycle valid is high — not necessarily the accept beat. So the value it uses could be a mid-hold value.
• A mid-hold change is a real violation. If a field is value A early in the hold and value B at accept, the protocol is violated — and a receiver that sampled early used A, while a receiver that sampled at accept used B. The two disagree.
• Accept-only checking sees only B. A checker sampling at the accept beat sees the field as B, finds it a legal value, and passes — never noticing it was A earlier.
• So the violation escapes. The bug (a field that mutated mid-hold) is not flagged, ships, and manifests as an occasional corruption when a receiver happens to sample the early value.

The point to carry:

The deepest lesson of verification is that a passing checker is only as good as what it looks at, and a checker that samples at the wrong time — or too few times — gives false confidence that is worse than no checker at all. An accept-only protocol checker will show green on a design with a real mid-hold field bug, and the green is actively misleading: it tells the team the protocol is clean when it is not, so they stop looking. The failure mode is not that the checker is wrong about what it checks — it correctly verifies the accept-beat value — but that it checks the wrong thing: a single instant where the rule is about a window. This is the recurring theme of the whole verification module: the dangerous bugs are not in the design's happy path but in the checker's blind spots, and a blind spot in a checker is invisible precisely because the checker reports success. The discipline is to make every checker's temporal scope match the rule's — a window rule needs a window check — and to be suspicious of any checker that only ever samples at one convenient edge.

10. Checking a Held Flit — accept-only vs full-window

A request flit whose address field mutates during the hold.

1. Valid asserted, address = A. The requester asserts valid with address A; ready is low (the receiver is busy). The flit is held.
2. Mid-hold: address changes to B. While still held (valid high, ready low), a design bug changes the address field to B. This is a stability violation — the field changed mid-hold.
3. Accept: valid AND ready, address = B. The receiver asserts ready; the flit transfers with address B. The accept-beat value is B — a legal address.
4. Accept-only checker — passes. The checker samples at accept, sees address B (legal), and passes. It never saw the change from A to B. Violation escaped.
5. Full-window checker — fails. A checker verifying $stable across valid && !ready sees the address change from A to B during the hold and flags it. Violation caught.

The full-window checker caught the mid-hold mutation; the accept-only checker saw only the final legal value and passed. The DebugLab is step 4.

11. Checker / Monitor View — a protocol checker with stability

The checker verifies opcode legality, field-combination legality, and field stability across the hold. Representative.

// Representative per-channel protocol checker (educational).
// Checks: (1) opcode legal for the channel, (2) field combination legal, (3) FIELDS
// STABLE across the whole valid-until-ready window. The stability check must span the
// hold (valid && !ready), not just the accept beat -- else a mid-hold field change
// escapes. Raises `violation` on any failure.
module chi_proto_check #(parameter AW = 44) (
  input  logic          clk, rst_n,
  input  logic          valid, ready,     // handshake
  input  logic [3:0]    opcode,           // channel opcode
  input  logic [AW-1:0] addr,             // a field that must be stable while held
  input  logic          op_legal,         // opcode is legal for this channel (precomputed)
  input  logic          fields_legal,     // field combination is legal
  output logic          violation
);
  logic held_q;                // was the flit held (valid && !ready) last cycle?
  logic [AW-1:0] addr_q;       // its field value last cycle
  logic stable_viol;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      held_q <= 1'b0; addr_q <= '0;
    end else begin
      held_q <= valid && !ready;   // remember we were mid-hold
      addr_q <= addr;
    end
  end
 
  // A field must NOT change while the flit is held awaiting accept.
  assign stable_viol = held_q && valid && (addr != addr_q);   // mid-hold mutation
  // Any failure -- illegal opcode/fields at the flit, OR a mid-hold field change.
  assign violation   = (valid && (!op_legal || !fields_legal)) || stable_viol;
endmodule

The same behavior in Verilog-2001:

// Representative per-channel protocol checker (Verilog-2001).
module chi_proto_check #(parameter AW = 44) (
  input              clk, rst_n, valid, ready,
  input  [3:0]       opcode,
  input  [AW-1:0]    addr,
  input              op_legal, fields_legal,
  output             violation
);
  reg held_q; reg [AW-1:0] addr_q;
  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin held_q <= 1'b0; addr_q <= {AW{1'b0}}; end
    else begin held_q <= valid & ~ready; addr_q <= addr; end
  end
  wire stable_viol = held_q & valid & (addr != addr_q);
  assign violation = (valid & (~op_legal | ~fields_legal)) | stable_viol;
endmodule

And in VHDL:

-- Representative per-channel protocol checker (VHDL).
library ieee;
use ieee.std_logic_1164.all;
 
entity chi_proto_check is
  generic ( AW : integer := 44 );
  port (
    clk, rst_n   : in  std_logic;
    valid, ready : in  std_logic;
    opcode       : in  std_logic_vector(3 downto 0);
    addr         : in  std_logic_vector(AW-1 downto 0);
    op_legal, fields_legal : in std_logic;
    violation    : out std_logic
  );
end entity;
 
architecture rtl of chi_proto_check is
  signal held_q  : std_logic := '0';
  signal addr_q  : std_logic_vector(AW-1 downto 0) := (others => '0');
  signal stable_viol : std_logic;
begin
  process (clk, rst_n)
  begin
    if rst_n = '0' then
      held_q <= '0'; addr_q <= (others => '0');
    elsif rising_edge(clk) then
      held_q <= valid and (not ready);      -- mid-hold last cycle
      addr_q <= addr;
    end if;
  end process;
 
  stable_viol <= '1' when (held_q = '1' and valid = '1' and addr /= addr_q) else '0';
  violation   <= '1' when ((valid = '1' and (op_legal = '0' or fields_legal = '0'))
                           or stable_viol = '1') else '0';
end architecture;

All three raise violation on an illegal flit or a mid-hold field change (stable_viol) — the stability check spans the hold via the remembered held_q/addr_q. The DebugLab drops stable_viol, checking only the accept-beat legality.

12. Assertion View — fields stable while held

The properties formalize the rules: legality at the flit, stability across the hold.

// Bind to the channel (or chi_proto_check).
// 1. A field must be stable while the flit is held awaiting accept.
property p_field_stable_while_held;
  @(posedge clk) disable iff (!rst_n)
    (valid && !ready) |=> (valid |-> $stable(addr));
endproperty
 
// 2. Valid must not deassert without an accept (the flit is held until taken).
property p_valid_held_until_accept;
  @(posedge clk) disable iff (!rst_n)
    (valid && !ready) |=> valid;
endproperty
 
// 3. An accepted flit had a legal opcode and field combination.
property p_legal_at_accept;
  @(posedge clk) disable iff (!rst_n)
    (valid && ready) |-> (op_legal && fields_legal);
endproperty

The system point, beyond the checks:

The stability property p_field_stable_while_held is a temporal assertion — it spans two cycles with the |=> implication — and that is exactly what an accept-only check cannot express. The distinction between a single-cycle and a multi-cycle check is the whole game in protocol verification: the protocol rules that are easy to get right in a checker (legal opcode) are the single-cycle ones, and the rules that are easy to get wrong (stability, handshake ordering, no-deassert-before-accept) are the multi-cycle ones. A robust protocol monitor is mostly made of temporal assertions, and each one must have its scope chosen to match the rule's window. The $stable built-in exists precisely for this — it asks "did this signal hold its value across the window?" — and using it correctly means anchoring it to the right window (here, valid && !ready). The broader discipline this opens is that verifying a protocol is verifying behaviors over time, not values at instants, so the checker's vocabulary must be temporal ($past, $stable, $rose, sequences) — and a monitor written only in instantaneous terms is, by construction, blind to the temporal violations that are the hardest and most dangerous protocol bugs. Chapter 17.5 returns to this with SVA in depth.

• What it proves: fields are stable while held; valid holds until accept; accepted flits are legal.
• What it does not prove: the flit is coherently correct — that is Chapter 17.2's invariants.
• Bug signature: a checker with no temporal (stability/handshake) assertions — only accept-beat legality.

13. Testbench — a mid-hold field change must be flagged

Holds a flit, mutates its address mid-hold, and checks the checker flags it.

module tb_chi_proto_check;
  localparam AW = 8;
  logic clk = 0, rst_n = 0, valid, ready;
  logic [3:0] opcode;
  logic [AW-1:0] addr;
  logic op_legal, fields_legal, violation;
  int errors = 0;
 
  chi_proto_check #(.AW(AW)) dut (.*);
  always #5 clk = ~clk;
 
  initial begin
    valid = 0; ready = 0; opcode = 0; addr = 0; op_legal = 1; fields_legal = 1;
    @(posedge clk) rst_n = 1;
 
    // Assert valid with address A; receiver not ready (flit held).
    @(posedge clk) begin valid = 1; ready = 0; addr = 8'hA0; end
    @(posedge clk);   // still held
    #1;
    if (violation) begin errors++; $display("FAIL false violation on stable held flit"); end
    else $display("PASS stable held flit: no violation");
 
    // MID-HOLD: change the address to B while still held -> stability violation.
    @(posedge clk) begin addr = 8'hB0; end   // valid still high, ready still low
    #1;
    if (!violation) begin errors++; $display("FAIL mid-hold field change NOT flagged (escaped!)"); end
    else $display("PASS mid-hold field change flagged as violation");
 
    // Accept the flit (any legal final value).
    @(posedge clk) begin ready = 1; end
    @(posedge clk) begin valid = 0; ready = 0; end
 
    // An illegal opcode at a flit must also be flagged.
    @(posedge clk) begin valid = 1; op_legal = 0; addr = 8'hC0; end
    #1;
    if (!violation) begin errors++; $display("FAIL illegal opcode not flagged"); end
    else $display("PASS illegal opcode flagged");
    @(posedge clk) begin valid = 0; op_legal = 1; end
 
    if (errors == 0) $display("ALL TESTS PASSED");
    else             $display("%0d FAILURE(S)", errors);
    $finish;
  end
endmodule

Expected output:

PASS stable held flit: no violation
PASS mid-hold field change flagged as violation
PASS illegal opcode flagged
ALL TESTS PASSED

14. DebugLab — an accept-only protocol checker

valid asserted, addr = A, ready LOW (flit held)
DUT bug: addr changes A -> B while held (valid high, ready still low)  [VIOLATION]
receiver latches addr early -> uses A
accept beat: valid && ready, addr = B (legal value)
accept-only checker: samples addr at accept = B -> legal -> PASSES  (misses A->B)
  -> violation ESCAPES; receiver used A, checker approved B
correct: assert $stable(addr) while (valid && !ready) -> flags the A->B change

15. Common Mistakes

• Checking only at accept. Assumption: the accept value is all that matters. Bug: mid-hold mutation escapes (the DebugLab). Prevention: check the whole hold.
• Treating temporal rules as instantaneous. Assumption: one cycle suffices. Bug: stability/handshake unchecked. Prevention: use temporal assertions.
• No stability check. Assumption: fields never change while held. Bug: unflagged mutation. Prevention: assert $stable while held.
• Allowing valid to deassert before accept. Assumption: the sender can retract. Bug: a dropped flit unchecked. Prevention: hold valid until accept.
• Ignoring X/unknown fields. Assumption: fields are always driven. Bug: uninitialized field passes. Prevention: check for no-X on valid.
• Confusing protocol with coherence. Assumption: one checker covers both. Bug: coherence holes (Chapter 17.2). Prevention: protocol first, then invariants.

16. Engineering Checklist

• Monitor each channel (REQ/RSP/SNP/DAT) with a protocol checker.
• Check opcode legality and field-combination legality per flit.
• Check the flit's fields are $stable across valid && !ready (the hold).
• Check valid does not deassert before accept.
• Check for no X on valid fields.
• Confirm every temporal rule has a temporal (multi-cycle) assertion.

17. Key Takeaways

• Protocol verification checks each flit is legal on its channel — the first layer.
• Per-channel rules: legal opcode, legal field combinations, correct handshake.
• A flit's fields must be stable across the valid-until-ready window.
• An accept-only checker has a temporal blind spot and misses mid-hold mutations.
• A green checker with a blind spot gives false confidence — worse than none.
• Match the checker's temporal scope to the rule; the model here is representative.

18. Quick Revision

Protocol verification. The first layer of CHI verification checks that every flit is legal on its channel, independent of coherence: a legal opcode, a legal field combination, and a well-formed handshake. A protocol monitor observes each channel (REQ/RSP/SNP/DAT) and flags illegal flits before any coherence reasoning. The subtle correctness requirement is in the checker itself: a CHI handshake asserts valid and holds the flit until ready accepts it (the accept beat), and the protocol requires the flit's fields to be stable across that whole valid-high window — the receiver may sample them on any held cycle. The failure to avoid: an accept-only checker that validates fields only at the accept beat. It misses a bug where a field mutates mid-hold (valid high, ready low) — the checker sees only the final legal value and passes, while a receiver that sampled the early value used something else, so the violation escapes and corrupts the transaction later. The remedy is to check field stability across the entire hold (assert $stable while valid && !ready), matching the checker's temporal scope to the rule's window. Temporal rules (stability, handshake ordering) need temporal checks; a green checker with a blind spot gives false confidence worse than no checker. Representative model; 17.2 covers coherence-invariant verification.

Coming Next

Chapter 17.2 — Coherency Verification. Protocol checking proves each flit is well-formed; it says nothing about whether the caches stay coherent. Chapter 17.2 covers coherency verification — the end-to-end, cross-cache invariants like single-writer-multiple-reader, why they cannot be checked from any single flit, and why a checker that verifies each transaction locally but never the global invariant lets a two-writer coherence violation pass.