A counterexample names a failing assertion and a cycle. That is where most engineers start simulating, and where the confusion starts: the failing cycle is where the monitor gave up, not where the design went wrong. The design went wrong at the attempt, up to several cycles earlier. This lesson's one job is the three-step walk backwards.
Read a failure in three steps. First, find the attempt: which antecedent fired, and in which cycle, to start the check that failed. For an invariant such as conservation there is no antecedent, so the attempt is the arming event: the first cycle in which the design did something that made the state wrong. Second, walk the window forward from the attempt and name the first cycle where a required condition is missing. Third, classify: a design bug if the environment kept its contract, a missing assumption if it did not, an abstraction artefact if the trace cannot happen in the unabstracted design. The routine is the same for a finite counterexample and for a step counterexample from an induction failure.
Steps are numbered as in every proof run in this section: step 0 is the reset step, and a run of depth D checks steps 0 to D minus 1.
The bridge mutant that never captures into the skid accepts a word while stalled and drops it. The proof below fails; the table reads the failing run the way the routine demands, attempt first. It is a trace built by hand from the mutant's code that shows the same failure the solver reports, with each row giving the state at the start of the step:
// formal: bmc 4 expect fail slang top hs_bridge define BUG=1
`define FORMAL
// hs_bridge: valid/ready register stage with a skid buffer (2-entry elastic stage).
// Output stage `ovld/odat` plus skid `svld/sdat`. in_ready = !svld, so it depends on a
// register only (no combinational path from out_ready to in_ready). Synchronous
// active-high reset empties both stages. A transfer happens on a cycle where valid
// and ready are both 1.
// BUG: 0 none, 1 data dropped on stall (skid never captures), 2 valid dropped
// (stalled output loses valid when the input idles), 3 data changes under backpressure
// (stalled output overwritten by new input).
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire in_valid,
output wire in_ready,
input wire [7:0] in_data,
output wire out_valid,
input wire out_ready,
output wire [7:0] out_data
);
reg ovld, svld;
reg [7:0] odat, sdat;
assign in_ready = !svld;
assign out_valid = ovld;
assign out_data = odat;
wire in_xfer = in_valid && in_ready;
wire out_xfer = ovld && out_ready;
wire stalled = ovld && !out_ready;
always @(posedge clk) begin
if (rst) begin
ovld <= 1'b0;
svld <= 1'b0;
end else if (stalled) begin
// output holds; a new input is parked in the skid register
if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
if (BUG == 2 && !in_valid) ovld <= 1'b0;
if (BUG == 3 && in_xfer) odat <= in_data;
end else begin
// output empty or consumed this cycle
if (svld) begin
odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
end else begin
odat <= in_data; ovld <= in_valid;
end
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- conservation: accepted - delivered = items held (counters wrap at 16) ----
reg [3:0] acc, dlv;
always @(posedge clk) begin
if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
else begin
if (in_xfer) acc <= acc + 4'd1;
if (out_xfer) dlv <= dlv + 4'd1;
end
end
always @(*) if (!init) begin
a_skid_needs_out: assert (!svld || ovld); // skid only used behind a full output
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: a stalled output must hold valid and data ----
always @(posedge clk) if (!init && !$past(rst)) begin
a_valid_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_valid);
a_data_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
// ready is a registered function: it cannot depend on out_ready in the same cycle
a_no_ready_comb: assert (in_ready == !svld);
end
// ---- data integrity by tracked-item abstraction: follow the n-th accepted word ----
// free constant (see sync_fifo.sv): anyconst wire plus an equal-to-its-old-copy assumption
(* anyconst *) wire [3:0] tn;
reg [3:0] tn_q;
always @(posedge clk) tn_q <= tn;
always @(*) if (!init) assume (tn == tn_q);
reg tv; // the tracked word has been accepted and not yet delivered
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
else if (out_xfer && dlv == tn) tv <= 1'b0;
end
end
always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
// where the tracked word lives: output stage if it is next to leave, else skid
h_in_out: assert (!(tv && dlv == tn) || (ovld && odat == td));
h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
h_pos: assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
end
end endgenerate
// ---- covers ----
always @(*) if (!init) begin
c_stall: cover (stalled);
c_skid_used: cover (svld);
c_backpress_full: cover (!in_ready);
c_flow: cover (in_xfer && out_xfer);
end
`endif
endmoduleStep | in_valid, out_ready | Accepted minus delivered | Stored (output, skid) | Reading |
|---|---|---|---|---|
0 | reset step | 0 | 0, 0 | Not checked. |
1 | 1, 0 | 0 | 0, 0 | Word A is accepted into the output stage. Legal. |
2 | 1, 0 | 1 | 1, 0 | Arming event: the output is stalled and word B is accepted, but the skid never captures it. The handshake is legal; the capture is missing. |
3 | any | 2 | 1, 0 | Conservation breaks: two words owed, one stored. The monitor reports here. |
The root cause is the missing capture in step 2: the stalled branch takes the input's handshake without parking the word. The fix restores the skid write. Note the classification: the environment kept its contract throughout, so this is a design bug, not a missing assumption, and the trace replays on the unabstracted design, so it is not an abstraction artefact either.
The failure write-up names the attempt cycle, not just the failing cycle: which antecedent fired, or which event armed the invariant, and what it demanded.
The classification is stated: design bug, missing assumption, or abstraction artefact, with the test that distinguishes them.
The fix is paired with the failure: the same trace, rerun after the fix, must pass, and a cover must show the scenario still happens.
Replay the failing inputs in simulation against the same RTL: the replayer drives the trace as stimulus and the waves must show the same broken condition in the same cycle. If simulation disagrees, the harness differs from the bench: reset, initial state, or an assumption the bench does not keep. Minimise next: drop inputs the failure does not need until the shortest failing trace remains, then fix from the attempt, not from the failing cycle.
Because the failing cycle is where the monitor gave up, which moves with the monitor: a different check reports the same bug a cycle later. The attempt is where the design committed, and it does not move. Fixes written at the failing cycle chase the monitor; fixes at the attempt fix the design.