A checker on a gated clock stopped evaluating while the clock was gated, and a bug inside the gated window passed every run. The harness had clocked the assertions with the gated clock instead of the free clock plus an enable. Every part of a harness is a decision about what gets checked. This lesson numbers the parts of a complete harness, shows the wrapper form once, and then breaks the clock.
Job of this lesson: show a complete harness with every part labelled, and demonstrate the gated-clock blind window it must avoid.
A harness gives the solver free inputs, one reset sequence, assumptions that model the environment, assertions for the guarantees, covers for the witnesses, and parameters for bug variants and helpers. Formal-only code lives under a formal guard so simulation never sees it. Properties live inside the design file under the guard, or in a wrapper that instantiates the design and sees only its ports. Hierarchical references into a design and bind are not portable: they work in one of the two front ends available here and fail in the other, so keep properties in one of those two places and the same file runs in both.
Part | Where in the file below | What it decides |
|---|---|---|
1 Parameters | comment [1] | Which planted bug or helper set a run uses. |
2 Free inputs | comment [2] | Every port is free unless assumed otherwise. |
3 Reset and assumptions | comment [3] | The one reset sequence; what the environment may do. |
4 State assertions | comment [4] | Guarantees on current state. |
5 Protocol assertions | comment [5] | Guarantees that look back, with the history gate. |
6 Data integrity | comment [6] | A tracked word, its shadow value, helper invariants. |
7 Covers | comment [7] | The behaviours judged are reachable. |
The numbered file proves at depth 4. Its partner has the planted bug that overwrites a stalled word: the data check fails at depth 4.
// 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).
// [1] parameters: BUG selects a planted bug, HELPER switches the helper invariants
// [2] free inputs: every input port is free in every cycle unless assumed
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
// [3] reset and assumptions: step 0 is a power-up state with reset asserted
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// [4] harness registers and state assertions: 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
// [5] protocol assertions (they read $past, so they skip the cycle after reset)
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
// [6] data integrity by a tracked word: a free constant (an assumption), a shadow value, an assertion, helpers
// free constant 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
// [7] covers: the behaviours the assertions judge are reachable
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
endmodule// formal: bmc 4 expect fail slang top hs_bridge define BUG=3
`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).
// [1] parameters: BUG selects a planted bug, HELPER switches the helper invariants
// [2] free inputs: every input port is free in every cycle unless assumed
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
// [3] reset and assumptions: step 0 is a power-up state with reset asserted
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// [4] harness registers and state assertions: 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
// [5] protocol assertions (they read $past, so they skip the cycle after reset)
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
// [6] data integrity by a tracked word: a free constant (an assumption), a shadow value, an assertion, helpers
// free constant 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
// [7] covers: the behaviours the assertions judge are reachable
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 wrapper form checks only the ports, so nothing reaches inside. Its partner plants the bug that drops valid while stalled; the hold check fails at depth 5 (depth 4 passes).
// formal: prove 4 expect pass slang top hs_wrap
`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
endmodule
module hs_wrap #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
input wire out_ready
);
wire in_ready, out_valid;
wire [7:0] out_data;
hs_bridge #(.BUG(BUG)) dut (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(in_ready), .in_data(in_data),
.out_valid(out_valid), .out_ready(out_ready), .out_data(out_data));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
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));
end
`endif
endmodule// formal: bmc 5 expect fail slang top hs_wrap 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
endmodule
module hs_wrap #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
input wire out_ready
);
wire in_ready, out_valid;
wire [7:0] out_data;
hs_bridge #(.BUG(BUG)) dut (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(in_ready), .in_data(in_data),
.out_valid(out_valid), .out_ready(out_ready), .out_data(out_data));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
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));
end
`endif
endmoduleNow the clock. A checker on a gated clock evaluates only at the gated edges; the open flow has one clock, so the blind window is emulated by a check evaluated only in cycles where the enable is high. The register loads when en is high, and the hold property is $past(en) || q == $past(q): it changes only if the enable of the previous cycle was high. It proves on the good register and catches a spurious clear inside the gated window (bug 1, depth 5).
// formal: prove 4 expect pass slang top en_reg
`define FORMAL
module en_reg #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire en,
input wire [3:0] d,
output reg [3:0] q,
output wire [3:0] q_out
);
always @(posedge clk) begin
if (rst) q <= 4'd0;
else if (en) q <= d;
else if (BUG == 1 && d == 4'd15) q <= 4'd0;
end
assign q_out = (BUG == 2 && !en && d == 4'd15) ? 4'd0 : q;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hold while gated: the register loads at the edge when the enable of the previous cycle was high
always @(posedge clk) if (!init && !$past(rst)) a_hold: assert ($past(en) || q == $past(q));
`endif
endmodule// formal: bmc 5 expect fail slang top en_reg define BUG=1
`define FORMAL
module en_reg #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire en,
input wire [3:0] d,
output reg [3:0] q,
output wire [3:0] q_out
);
always @(posedge clk) begin
if (rst) q <= 4'd0;
else if (en) q <= d;
else if (BUG == 1 && d == 4'd15) q <= 4'd0;
end
assign q_out = (BUG == 2 && !en && d == 4'd15) ? 4'd0 : q;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hold while gated: the register loads at the edge when the enable of the previous cycle was high
always @(posedge clk) if (!init && !$past(rst)) a_hold: assert ($past(en) || q == $past(q));
`endif
endmoduleThe tempting repair, “state equals its past on every enabled cycle”, is wrong and fails on the good register at its first enabled load (depth 4):
// formal: bmc 4 expect fail slang top en_reg
`define FORMAL
module en_reg #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire en,
input wire [3:0] d,
output reg [3:0] q,
output wire [3:0] q_out
);
always @(posedge clk) begin
if (rst) q <= 4'd0;
else if (en) q <= d;
else if (BUG == 1 && d == 4'd15) q <= 4'd0;
end
assign q_out = (BUG == 2 && !en && d == 4'd15) ? 4'd0 : q;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// tempting but wrong: the register changes at its first enabled load
always @(posedge clk) if (!init && !$past(rst) && en) a_hold: assert (q == $past(q));
`endif
endmoduleThe blind window itself is bug 2: the output shows 0 for one cycle while the enable is low, and the register is never wrong. A check on every cycle sees it; the enable-gated check never does.
// formal: bmc 4 expect fail slang top en_reg define BUG=2
`define FORMAL
module en_reg #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire en,
input wire [3:0] d,
output reg [3:0] q,
output wire [3:0] q_out
);
always @(posedge clk) begin
if (rst) q <= 4'd0;
else if (en) q <= d;
else if (BUG == 1 && d == 4'd15) q <= 4'd0;
end
assign q_out = (BUG == 2 && !en && d == 4'd15) ? 4'd0 : q;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hold while gated: the register loads at the edge when the enable of the previous cycle was high
always @(posedge clk) if (!init && !$past(rst)) a_hold: assert ($past(en) || q == $past(q));
// checked in every cycle on the free clock
always @(*) if (!init) a_out: assert (q_out == q);
`endif
endmodule// formal: bmc 8 expect pass slang top en_reg define BUG=2
`define FORMAL
module en_reg #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire en,
input wire [3:0] d,
output reg [3:0] q,
output wire [3:0] q_out
);
always @(posedge clk) begin
if (rst) q <= 4'd0;
else if (en) q <= d;
else if (BUG == 1 && d == 4'd15) q <= 4'd0;
end
assign q_out = (BUG == 2 && !en && d == 4'd15) ? 4'd0 : q;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hold while gated: the register loads at the edge when the enable of the previous cycle was high
always @(posedge clk) if (!init && !$past(rst)) a_hold: assert ($past(en) || q == $past(q));
// checked only in cycles where the enable is high, as a checker on a gated clock is
always @(posedge clk) if (!init && en) a_out_g: assert (q_out == q);
`endif
endmoduleHow to read it: one slot is one step, so slot 1 is step 0. en is high in step 1 only. d is 1 in steps 0 and 1 and 15 in steps 2 and 3. q is 1 in step 0 (the power-up value the solver chose), 0 in step 1 (reset), 1 in step 2 (it loaded d at the end of step 1) and 0 in step 3 (reset again). q_out follows q except in step 2, where en is low and d is 15: there q_out reads 0 while q reads 1. free_check_fail is the output check on the free clock, evaluated in every step after step 0; it is high in step 2 only. gated_check_runs is high in step 1 only: a check evaluated only when the enable is high looks at step 1, where q_out equals q, and never at step 2, so gated_check_fail stays 0 in all four slots. The register itself is not wrong in any step; only the output differs, for one step.
The first run is a counterexample on the free clock; the second is bounded to 8 and passes, because the glitch appears only where the checker is not looking. The good register proves both checks:
// formal: prove 4 expect pass slang top en_reg
`define FORMAL
module en_reg #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire en,
input wire [3:0] d,
output reg [3:0] q,
output wire [3:0] q_out
);
always @(posedge clk) begin
if (rst) q <= 4'd0;
else if (en) q <= d;
else if (BUG == 1 && d == 4'd15) q <= 4'd0;
end
assign q_out = (BUG == 2 && !en && d == 4'd15) ? 4'd0 : q;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hold while gated: the register loads at the edge when the enable of the previous cycle was high
always @(posedge clk) if (!init && !$past(rst)) a_hold: assert ($past(en) || q == $past(q));
// checked in every cycle on the free clock
always @(*) if (!init) a_out: assert (q_out == q);
`endif
endmoduleOne design instance, free inputs, one reset sequence, formal-only code guarded; properties inside the file or a wrapper.
Assertions on the free clock with enable qualifiers, never on a gated clock; covers for every behaviour judged, gated windows included.
Mutate inside each window the harness claims to check, gated windows included, and confirm the matching property fires. If a gated-window mutant survives, the checker is blind there: move it to the free clock with the enable qualifier and rerun.
The checkers run on the gated clock, so they never evaluate while the gate is shut. Move them to the free clock with an enable qualifier.
Hierarchical references and bind are rejected by one of the front ends, so such a property may run in one flow and fail in another. A wrapper sees only ports and runs in both.