A request held for four cycles with a two-cycle response window fails its property on the good design. The responder answered the request: once, one cycle after it rose. But the level form started four attempts, one per high cycle, and the later attempts have no response inside their windows. The engineer reads the failure as a slow responder and loosens the window; the real error is that one request produced four proof obligations. This lesson's one job is to count attempts correctly.
An implication with a level antecedent starts a new check in every cycle the antecedent is true. An edge-gated antecedent starts one check per rising edge. When the request is a pulse the two coincide; when the request is held they differ, and every held cycle is a fresh attempt that needs its own response inside its own window. The Boolean forms differ by one term: the level form names the sampled request, the edge form names the sampled request qualified by its absence one cycle earlier.
The rising edge is the sampled-value function of the previous lesson: $rose(req) is req now and not req in the previous sample, which is a history flop and an AND gate. Textbook form and Boolean form side by side:
// not-run: implication operators are not accepted by this front end
// level: req |-> ##[1:2] ack // one attempt in EVERY cycle req is high
// edge: $rose(req) |-> ##[1:2] ack // one attempt per rising edge
// Boolean edge form used below: rose = req && !req_q, checked as
// !rose_d2 || ack_d1 || ack // the attempt that started two cycles agoThe responder below answers one cycle after each rising edge. The request is held for four cycles. The level form fails on the attempt that starts in the second high cycle: its window holds no answer, because the only answer belongs to the first attempt. The edge form passes: one edge, one attempt, one answer in its window. Cycles are numbered from the first high cycle of the request.
Attempt starts | Attempt type | Answer in window | Verdict |
|---|---|---|---|
Cycle 1 (rise) | Both forms | Cycle 2 | Holds. |
Cycle 2 (held) | Level only | None in cycles 3 to 4 | Level fails here. |
Cycle 3 (held) | Level only | None in cycles 4 to 5 | Level fails here. |
Cycle 4 (held) | Level only | None in cycles 5 to 6 | Level fails here. |
The two runnable blocks are the same responder with the two antecedents; only the parameter differs. The level form fails on the good design, which is the point: the failure names the attempt, not a bug:
// formal: bmc 6 expect fail slang define EDGE=0
`define FORMAL
// req_window: answers one cycle after each rising edge of req. EDGE selects the
// antecedent: 0 starts an attempt in every cycle req is high (level), 1 starts
// one attempt per rising edge. The guard skips two cycles past reset because the
// checks look two cycles back.
module req_window #(parameter EDGE = 1) (
input wire clk,
input wire rst,
input wire req,
output reg ack
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!req);
reg req_q, rose_d1, rose_d2, req_d1, req_d2;
wire rose = req && !req_q;
always @(posedge clk) begin
if (rst) begin
req_q <= 1'b0; rose_d1 <= 1'b0; rose_d2 <= 1'b0;
req_d1 <= 1'b0; req_d2 <= 1'b0; ack <= 1'b0;
end else begin
req_q <= req;
rose_d1 <= rose; rose_d2 <= rose_d1;
req_d1 <= req; req_d2 <= req_d1;
ack <= rose;
end
end
always @(posedge clk) if (!init && !$past(rst) && !$past(rst, 2)) begin
if (EDGE == 0) p_level: assert (!req_d2 || $past(ack) || ack);
else p_edge: assert (!rose_d2 || $past(ack) || ack);
end
endmoduleThe edge form passes on the same design and the same stimulus: one edge, one attempt, answered in its window:
// formal: bmc 6 expect pass slang define EDGE=1
`define FORMAL
// req_window: answers one cycle after each rising edge of req. EDGE selects the
// antecedent: 0 starts an attempt in every cycle req is high (level), 1 starts
// one attempt per rising edge. The guard skips two cycles past reset because the
// checks look two cycles back.
module req_window #(parameter EDGE = 1) (
input wire clk,
input wire rst,
input wire req,
output reg ack
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!req);
reg req_q, rose_d1, rose_d2, req_d1, req_d2;
wire rose = req && !req_q;
always @(posedge clk) begin
if (rst) begin
req_q <= 1'b0; rose_d1 <= 1'b0; rose_d2 <= 1'b0;
req_d1 <= 1'b0; req_d2 <= 1'b0; ack <= 1'b0;
end else begin
req_q <= req;
rose_d1 <= rose; rose_d2 <= rose_d1;
req_d1 <= req; req_d2 <= req_d1;
ack <= rose;
end
end
always @(posedge clk) if (!init && !$past(rst) && !$past(rst, 2)) begin
if (EDGE == 0) p_level: assert (!req_d2 || $past(ack) || ack);
else p_edge: assert (!rose_d2 || $past(ack) || ack);
end
endmoduleThe same attempt counting, checked exhaustively in a few lines: a held request with one answer fails the level attempts and passes the edge attempt, and a responder that never answers fails the edge form too, which is the evidence the edge form is not vacuous:
def attempts(req):
level = [t for t, v in enumerate(req) if v]
edge = [t for t, v in enumerate(req) if v and (t == 0 or not req[t - 1])]
return level, edge
def answered(att, ack, lo=1, hi=2):
bad = []
for t in att:
window = [ack[t + d] for d in range(lo, hi + 1) if t + d < len(ack)]
if not any(window):
bad.append(t)
return bad
N = 8
req = [False, True, True, True, True, False, False, False]
ack = [False, False, True, False, False, False, False, False]
level, edge = attempts(req)
assert len(answered(level, ack)) > 0
assert len(answered(edge, ack)) == 0
dead = [False] * N
assert len(answered(edge, dead)) > 0
print("PASS: level fails held requests, edge passes; dead responder caught")The antecedent says edge or level in words: a held request needs the edge form unless the protocol truly re-requests every cycle.
Every failing run names the attempt: which start cycle, which window, which missing answer, not just the failing cycle.
The passing form still has a failing partner: a responder that never answers must fail it, or the form checks nothing.
Read a window failure backwards: from the failing cycle, subtract the window to find the attempt that started it, then ask whether that attempt corresponds to a real request. If the request line was already high the cycle before, the attempt is a level artefact and the fix is the edge qualifier, not a wider window. Widening the window to quiet a level failure only moves the same failure to longer holds.
The window: the attempt counting was already right, only the due cycles move. Change the window to one-to-two cycles after the edge and leave the edge qualifier alone.