Tags: one response must not satisfy every request

Why the lanes merge

A range gives every waiting attempt a thread at each edge of its window. When windows overlap, one ack falls inside all of them, and each attempt counts it as its own. The rule checks "some response came", never "my response came".

An edge-sensitive antecedent such as $rose(req) starts fewer attempts, but back-to-back requests still share a response. Making each attempt stop at its first ack does not help either: the first ack is the same one for all three. Each response needs a tag that says which request it answers.

Tickets for in-order responses

When responses return in request order, the tag can live in the checker. Two counters hand out tickets: issued counts requests and served counts responses. A request takes ticket issued; the next ack serves ticket served.

int unsigned issued = 0, served = 0;
always @(posedge clk) begin
  if (req) issued <= issued + 1;
  if (ack) served <= served + 1;
end
property ticket_served;          // ticket t is served within 4 edges
  int unsigned t;
  @(posedge clk) (req, t = issued) |-> ##4 (served + ack > t);
endproperty

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                 // rising edges at 5, 15, 25, ...
  logic req = 0, ack = 0;

  // Ticket counters: a request takes ticket number issued, the next ack serves ticket served.
  int unsigned issued = 0, served = 0;
  always @(posedge clk) begin
    if (req) issued <= issued + 1;
    if (ack) served <= served + 1;
  end

  ticket_served: assert property (@(posedge clk) (req, t = issued) |-> ##4 (served + ack > t));

  initial begin
    @(negedge clk); req = 1;            // requests at 15, 25, 35
    repeat (2) @(negedge clk);
    @(negedge clk); req = 0; ack = 1;   // one ack, at 45
    @(negedge clk); ack = 0;
    repeat (3) @(negedge clk);          // edges at 55 ... 75
    $finish;
  end
endmodule

The verdict is checked at the deadline, so a pass is reported there, not at the ack. A failure is reported at the end of the window, as a range rule would. Add the companion ack |-> served < issued: a response with no ticket outstanding is a duplicate or an invention.

Reading a ticket failure

A ticket failure proves that a response is missing, but it does not always point at the right one. If the second of three responses is lost, the third is counted as the second, and the deadline that fails is the last one. Counting alone cannot do better: from the outside, losing the second response looks the same as losing the third. Lesson A8.2 measures exactly this case.

Take the deadline from the specification's latency bound, not from what the design happens to do today. Too short, and the rule fails legal traffic. Too long, and a lost response is still caught, only later. Remember that in-order responses queue: a response waits behind the ones ahead of it, so the bound must cover the longest legal queue, not one request in isolation.

IDs for out-of-order responses

When responses can overtake each other, the tag must travel with them, as an ID. A generate loop writes one rule per ID value, with the ID as a constant, so no local variable is needed.

Per-ID rules bring back the original problem if an ID is reused while outstanding: two requests with ID 2 would both pass on one response. A small tracker keeps a busy bit per ID, and two rules guard it: no request reuses a busy ID, and no response carries an idle one. The example runs all three.

The two tracker rules also split the blame. A reused ID is the requester's fault, so no_reuse points at the master. A response for an idle ID, whether duplicated, invented or carrying a corrupted tag, is the responder's fault, so known points at the slave. The per-ID rule then reports the request that the corrupted response should have answered, at the end of its window.

Which pairing fits the protocol

A protocol that keeps order and also carries IDs can use either pairing. Tickets cost less to write, and IDs are faster to debug. Counts tell you that a response is missing; IDs tell you which. With 256 IDs, per-ID rules become slow and hard to read, and a scoreboard keyed by ID is usually the better tool. Keep the assertions for the timing and handshake rules, which the scoreboard cannot see edge by edge.

Try it

IDs 1 and 2 came back in the opposite order and both passed. The response at 75 carried ID 0, which nothing had requested, so known fired at once. The rule for ID 3 then waited out its window and failed at 105.

Change rsp_id = 0 to rsp_id = 3 and predict the output. Then set the second request's ID to 1 as well, and see which rule complains.

Check yourself

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                  // rising edges at 5, 15, 25, ...
  logic req = 0, ack = 0;
  int unsigned issued = 0, served = 0;
  always @(posedge clk) begin
    if (req) issued <= issued + 1;
    if (ack) served <= served + 1;
  end
  int n_untagged, n_ticket;
  property ticket_served;
    int unsigned t;
    @(posedge clk) (req, t = issued) |-> ##4 (served + ack > t);
  endproperty
  untagged: assert property (@(posedge clk) req |-> ##[1:4] ack) else n_untagged++;
  ticket:   assert property (ticket_served) else n_ticket++;
  initial begin
    @(negedge clk); req = 1;              // requests at 15 and 25
    @(negedge clk);
    @(negedge clk); req = 0; ack = 1;     // first ack at 35
    @(negedge clk); ack = 0;
    repeat (3) @(negedge clk);
    ack = 1;                              // second ack at 75
    @(negedge clk); ack = 0;
    repeat (2) @(negedge clk);
    $display("untagged=%0d ticket=%0d", n_untagged, n_ticket);
    $finish;
  end
endmodule

a: assert property (@(posedge clk) req |-> ##[1:4] ack) else fails++;

property served_by_deadline;
    int unsigned t;
    @(posedge clk) (req, t = issued) |-> ##4 (served + ack > t);
  endproperty
  a: assert property (served_by_deadline) else fails++;

a: assert property (@(posedge clk) $past(req, 4) |-> served + ack > $past(issued, 4)) else fails++;

property served_by_deadline;
    int unsigned t;
    @(posedge clk) (req, t = issued) |-> ##4 (served > t || (ack && served == t));
  endproperty
  a: assert property (served_by_deadline) else fails++;

Practice

• Tickets for a lost response Verify · Medium