A review meeting asks whether the bridge properties prove anything. The honest answer starts one level below the property text: the proof engine never reads an assertion as text. It compiles each concurrent assertion into a small monitor circuit, adds that circuit to the design to form one product model, and asks a single question about the combined model. Job of this lesson: fix that picture of assert, assume and cover as monitor questions, because every later lesson reasons inside it.
Three directives, three questions. An assert adds a monitor with a fail state and asks whether that state is reachable: a proof says no input sequence from reset can drive it there. A Boolean assume adds no monitor at all (a sequence-shaped assume does need one); it deletes every trace that breaks its condition, so the proof only searches what is left. A cover adds a monitor with a match state and asks whether that state is reachable: it shows the good behaviour can happen, which is the evidence that a passing assert is not vacuous. The roles of the three directives in a design flow are covered in the RTL course; here only the reachability question matters.
The monitor for an implication needs exactly one memory element plus a comparator. For the rule this lesson works, the bridge hold check, the flop remembers whether the output was stalled last cycle, and the comparator demands that the output is still valid now. Nothing about sequences, repetitions or clocks survives into the proof: all of it is compiled down to flops and gates before the solver starts.
The running rule is the output hold on the skid register stage: when the output is valid and the downstream is not ready, the output must still be valid in the next cycle. In textbook form it is an overlapped antecedent with a non-overlapped conclusion:
// not-run: implication operators are not accepted by this front end
// textbook: out_valid && !out_ready |=> out_valid
// checks the cycle AFTER a stalled cycleThe runnable Boolean form is the history check already in the bridge file. Written as hardware it is the flop and the comparator of the diagram above; the second listing is the same text the proof below runs (the label a_valid_hold in the module):
// snippet: the monitor of the rule above, drawn as hardware
// reg stalled_q; // the one history flop
// always @(posedge clk) stalled_q <= out_valid && !out_ready;
// comparator: !stalled_q || out_valid // must still be valid now
// snippet: the same check as written in the module (skips the cycle after reset)
// always @(posedge clk) if (!init && !$past(rst))
// a_valid_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_valid);On the correct bridge the full property set is proved. The header below checks the base case and the induction step; a pass means no trace from reset can break any of the nine assertions in the file:
// formal: prove 4 expect pass slang top hs_bridge
`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
endmoduleThe same file with the planted mutant, which clears the output valid while stalled whenever the input idles, gives the counterexample. Step 0 is the reset step, and a run of depth 4 checks steps 0 to 3. The run reports the conservation check and a helper invariant failing at step 3. A clocked check such as the hold check judges a cycle at its closing edge, so it reports one step after the state it judges: the same dropped valid would be named by the hold check at step 4, which this depth does not reach.
// formal: bmc 4 expect fail slang top hs_bridge define BUG=2
`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 | ovld, svld at the start of the step | Accepted minus delivered | Which condition breaks |
|---|---|---|---|---|---|
0 | 0 | 0 | reset step | 0 | None: the reset step is never checked. |
1 | 1 | 0 | 0, 0 | 0 | None: word A is accepted into the output stage. |
2 | 0 | 0 | 1, 0 | 1 | None yet: the output is stalled and the input idles, so the mutant clears the valid at the edge. |
3 | 0 | 0 | 0, 0 | 1 | Conservation: one word accepted, none stored, none delivered. |
The table is built by hand from the mutant's code, with every row showing the state at the start of the step, which is what a combinational check sees. The solver's own trace may pick different values for the free inputs; the shape is the same.
Every property sits inside the module under the formal guard, never reaching across hierarchy: the open flow accepts properties in the module or in a wrapper that instantiates the design.
Asserts sit on outputs and guarantees, assumes on inputs and environment rules, and every assume is a candidate for a matching assert on the neighbour block.
Each property is labelled, so the counterexample names the check that fired rather than a line number.
Run the pair: the proof to depth 4, then the bounded check with the mutant. Read the failing label first, then walk one cycle back to the attempt that armed the monitor: which history flop was set, and what the comparator saw. If the proof passes but the cover of normal traffic is unreachable, the pass is suspect: an assumption has pruned the behaviour away, which is the subject of the assumptions topic.
Whether the good behaviour can happen at all. An assert says the fail state is unreachable; a cover says the match state is reachable. A passing assert whose trigger never fires is vacuous, and only the cover exposes it.