Capstone: a tagged request/response channel

The channel

A requester sends req with a 3-bit req_id and an address. The responder answers with rsp_valid, rsp_id and rsp_data. Each response is ready a few edges after its request, the delay depending on the address, and responses leave in request order, so one can also wait behind earlier ones. A response is held while rsp_ready is low. An abort cancels every outstanding request, and a synchronous reset empties everything.

The specification adds one bound: every request is answered, or cancelled, within six edges. The testbench never has more than four requests in flight, so that bound covers the longest legal queue.

From specification to rules

Each rule states one property of the pairing. ticket is about time, orphan about counts, tag about identity and hold about stability. A fault that breaks one of these properties should trip the matching rule, and the matrix below checks that it does.

The model carries the tags

The rules read three pieces of auxiliary state, built from the ports only. issued counts requests, served counts taken responses, and id_of records the ID of each ticket, indexed by ticket number modulo 8. The ticket due next is always served, because responses come back in order.

The abort lives in the model too. At an abort, served jumps to issued, so every cancelled ticket counts as served. The ticket rule then needs no special case, and a response that arrives after the abort finds nothing outstanding, which orphan reports.

This design choice is worth copying. Let the model decide what an event means for the protocol, and keep each property a plain statement about the model and the pins.

Why the rules are this plain

Every rule is one implication whose antecedent is decided at a single edge, and the only local variable is captured there and read at a fixed delay. That fits the simulator: on Verilator 5.052 these forms report failures exactly where the standard says.

It also helps whoever reads a failure. Each rule starts at most one attempt per edge, so a failure count is a count of bad edges, and a failure time points straight at the edge to inspect. When a rule needs to know more, such as which ticket is due, that knowledge goes into the model. There it can be printed and debugged like any other code.

The fault bank and the matrix

The suite is silent on the correct design and catches every fault. The untagged range rule catches none: each faulty variant still produces some response inside every window.

Reading the matrix

Fault 1 trips two rules, at two different places. tag fires at 85, the first response after the gap, and names the missing ID. ticket fires at 115, for the fourth request, because the counting has shifted by one. The count proves something is missing; the ID says what.

Fault 3 passes ticket, since the abort already marked every ticket served. The late response is caught by orphan, the rule about counts. Fault 2 is caught by tag first, because the repeated ID arrives where the next one was due. orphan fires only at the end of the burst, when the extra response finds nothing outstanding.

No rule here checks rsp_data against the request's address, so a responder that corrupts data would pass. Adding that rule is the natural next step, with an addr_of table beside id_of.

Try it

One rule module, bound into six responders, prints one line per variant. The correct responder is silent; every faulty one trips at least one paired rule, and the untagged range rule trips on none.

Change fault 1 to drop the fourth request instead of the third (nreq == 4) and predict its line. Then add the data rule and see which variants it catches.

Check yourself

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                       // rising edges at 5, 15, 25, ...
  logic       req = 0, rsp = 0;
  logic [2:0] req_id = 0, rsp_id = 0;
  int unsigned issued = 0, served = 0;
  logic [2:0]  id_of [8];
  always @(posedge clk) begin
    if (req) begin id_of[issued % 8] <= req_id; issued <= issued + 1; end
    if (rsp) served <= served + 1;
  end
  int f_ticket, f_tag;
  property ticket_served;
    int unsigned t;
    @(posedge clk) (req, t = issued) |-> ##4 (served + rsp > t);
  endproperty
  ticket: assert property (ticket_served) else f_ticket++;
  tag:    assert property (@(posedge clk) rsp |-> rsp_id == id_of[served % 8]) else f_tag++;
  initial begin
    @(negedge clk); req = 1; req_id = 1;      // requests 1, 2, 3 at 15, 25, 35
    @(negedge clk); req_id = 2;
    @(negedge clk); req_id = 3;
    @(negedge clk); req = 0; rsp = 1; rsp_id = 1;   // responses at 45 and 55
    @(negedge clk); rsp_id = 2;
    @(negedge clk); rsp = 0;                  // the response for 3 never comes
    repeat (4) @(negedge clk);
    $display("ticket=%0d tag=%0d", f_ticket, f_tag);
    $finish;
  end
endmodule

Practice

• A tagged channel assertion suite Verify · Hard