An engineer writes the upstream rule "data holds while waiting" as an assertion on a block's input and the proof fails at once: the input was promised nothing. Another leaves the rule out and the proof fails later with a trace that no real upstream block can produce. Job of this lesson: assume the rule at the input of the block that needs it, assert it at the output of the block that owes it, and see both wrong placements fail.
Block A passes a data word on when it is granted. It holds the first word offered and relies on the word staying stable while the request waits. The specification: the cycle after a grant, the answer carries the word that was presented in the grant cycle. Two lines make up the rule: req stays high, and data stays equal to its old value, until gnt. They appear in the same text with three roles:
Role | Where the rule sits | Result in the runs below |
|---|---|---|
Assumed | A's inputs | A proves (with two helper invariants) |
Missing | Nowhere | A fails at step 3 on a trace no neighbour could produce |
Asserted on an input | A's inputs, as an assert | Fails at step 2: the input was promised nothing |
The rule is assumed at A's input and asserted at the output of the block that drives A: the next two lessons show that block. Never assert on an input, never assume on an output.
// formal: prove 6 expect pass slang top unitA define ASSUME=1 define BUG=0
`define FORMAL
module a_blk (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt,
output reg ov, output reg [3:0] out, output wire dbg_pend, output wire [3:0] dbg_held);
reg pend; reg [3:0] held;
assign dbg_pend = pend; assign dbg_held = held;
always @(posedge clk) begin
if (rst) begin pend <= 1'b0; ov <= 1'b0; end
else begin
ov <= req && gnt;
if (req && !gnt) pend <= 1'b1; else if (gnt) pend <= 1'b0;
if (req && !pend) held <= data;
out <= pend ? held : data;
end
end
endmodule
module hold_rule #(parameter ASSUME = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
reg init = 1'b1; reg pv = 1'b0, pg = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pv <= req; pg <= gnt; prst <= rst; pd <= data; end
wire waiting = !init && !rst && !prst && pv && !pg;
generate if (ASSUME == 2) begin : g_n
end else if (ASSUME) begin : g_a
always @(*) if (waiting) begin r_req: assume (req); r_dat: assume (data == pd); end
end else begin : g_s
always @(*) if (waiting) begin r_req: assert (req); r_dat: assert (data == pd); end
end endgenerate
endmodule
module a_spec (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt, input wire ov, input wire [3:0] out);
reg init = 1'b1; reg pgo = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pgo <= req && gnt; prst <= rst; pd <= data; end
always @(*) if (!init && !prst && pgo) a_answer: assert (ov && out == pd);
always @(*) if (!init) c_wait_then_grant: cover (!prst && ov && out == pd && out != 4'd0);
endmodule
module unitA #(parameter ASSUME = 1, parameter BUG = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
reg qv = 1'b0, qg = 1'b0; always @(posedge clk) begin qv <= req; qg <= gnt; end
always @(*) if (!init0 && ASSUME == 1) h_hist: assert (!dp || rst || (qv && !qg));
always @(*) if (!init0 && ASSUME == 1) h_pend: assert (!dp || rst || dh == data);
hold_rule #(.ASSUME(ASSUME)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmodule
module b_req #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt,
output wire req, output wire [3:0] data);
reg busy; reg [3:0] d;
assign req = busy; assign data = d;
always @(posedge clk) begin
if (rst) busy <= 1'b0;
else begin
if (!busy && want) begin busy <= 1'b1; d <= nd; end
else if (busy && gnt) busy <= 1'b0;
else if (busy && BUG == 1 && want) d <= nd;
end
end
endmodule
module unitB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
hold_rule #(.ASSUME(0)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
endmodule
module sysAB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data; wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
always @(*) if (!init0 && BUG == 0) begin h_pend_req: assert (!dp || req); h_pend_held: assert (!dp || dh == data); end
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmodule// formal: bmc 4 expect fail slang top unitA define ASSUME=2
`define FORMAL
module a_blk (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt,
output reg ov, output reg [3:0] out, output wire dbg_pend, output wire [3:0] dbg_held);
reg pend; reg [3:0] held;
assign dbg_pend = pend; assign dbg_held = held;
always @(posedge clk) begin
if (rst) begin pend <= 1'b0; ov <= 1'b0; end
else begin
ov <= req && gnt;
if (req && !gnt) pend <= 1'b1; else if (gnt) pend <= 1'b0;
if (req && !pend) held <= data;
out <= pend ? held : data;
end
end
endmodule
module hold_rule #(parameter ASSUME = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
reg init = 1'b1; reg pv = 1'b0, pg = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pv <= req; pg <= gnt; prst <= rst; pd <= data; end
wire waiting = !init && !rst && !prst && pv && !pg;
generate if (ASSUME == 2) begin : g_n
end else if (ASSUME) begin : g_a
always @(*) if (waiting) begin r_req: assume (req); r_dat: assume (data == pd); end
end else begin : g_s
always @(*) if (waiting) begin r_req: assert (req); r_dat: assert (data == pd); end
end endgenerate
endmodule
module a_spec (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt, input wire ov, input wire [3:0] out);
reg init = 1'b1; reg pgo = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pgo <= req && gnt; prst <= rst; pd <= data; end
always @(*) if (!init && !prst && pgo) a_answer: assert (ov && out == pd);
always @(*) if (!init) c_wait_then_grant: cover (!prst && ov && out == pd && out != 4'd0);
endmodule
module unitA #(parameter ASSUME = 1, parameter BUG = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
reg qv = 1'b0, qg = 1'b0; always @(posedge clk) begin qv <= req; qg <= gnt; end
always @(*) if (!init0 && ASSUME == 1) h_hist: assert (!dp || rst || (qv && !qg));
always @(*) if (!init0 && ASSUME == 1) h_pend: assert (!dp || rst || dh == data);
hold_rule #(.ASSUME(ASSUME)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmodule
module b_req #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt,
output wire req, output wire [3:0] data);
reg busy; reg [3:0] d;
assign req = busy; assign data = d;
always @(posedge clk) begin
if (rst) busy <= 1'b0;
else begin
if (!busy && want) begin busy <= 1'b1; d <= nd; end
else if (busy && gnt) busy <= 1'b0;
else if (busy && BUG == 1 && want) d <= nd;
end
end
endmodule
module unitB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
hold_rule #(.ASSUME(0)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
endmodule
module sysAB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data; wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
always @(*) if (!init0 && BUG == 0) begin h_pend_req: assert (!dp || req); h_pend_held: assert (!dp || dh == data); end
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmodule// formal: bmc 3 expect fail slang top unitA define ASSUME=0
`define FORMAL
module a_blk (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt,
output reg ov, output reg [3:0] out, output wire dbg_pend, output wire [3:0] dbg_held);
reg pend; reg [3:0] held;
assign dbg_pend = pend; assign dbg_held = held;
always @(posedge clk) begin
if (rst) begin pend <= 1'b0; ov <= 1'b0; end
else begin
ov <= req && gnt;
if (req && !gnt) pend <= 1'b1; else if (gnt) pend <= 1'b0;
if (req && !pend) held <= data;
out <= pend ? held : data;
end
end
endmodule
module hold_rule #(parameter ASSUME = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
reg init = 1'b1; reg pv = 1'b0, pg = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pv <= req; pg <= gnt; prst <= rst; pd <= data; end
wire waiting = !init && !rst && !prst && pv && !pg;
generate if (ASSUME == 2) begin : g_n
end else if (ASSUME) begin : g_a
always @(*) if (waiting) begin r_req: assume (req); r_dat: assume (data == pd); end
end else begin : g_s
always @(*) if (waiting) begin r_req: assert (req); r_dat: assert (data == pd); end
end endgenerate
endmodule
module a_spec (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt, input wire ov, input wire [3:0] out);
reg init = 1'b1; reg pgo = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pgo <= req && gnt; prst <= rst; pd <= data; end
always @(*) if (!init && !prst && pgo) a_answer: assert (ov && out == pd);
always @(*) if (!init) c_wait_then_grant: cover (!prst && ov && out == pd && out != 4'd0);
endmodule
module unitA #(parameter ASSUME = 1, parameter BUG = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
reg qv = 1'b0, qg = 1'b0; always @(posedge clk) begin qv <= req; qg <= gnt; end
always @(*) if (!init0 && ASSUME == 1) h_hist: assert (!dp || rst || (qv && !qg));
always @(*) if (!init0 && ASSUME == 1) h_pend: assert (!dp || rst || dh == data);
hold_rule #(.ASSUME(ASSUME)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmodule
module b_req #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt,
output wire req, output wire [3:0] data);
reg busy; reg [3:0] d;
assign req = busy; assign data = d;
always @(posedge clk) begin
if (rst) busy <= 1'b0;
else begin
if (!busy && want) begin busy <= 1'b1; d <= nd; end
else if (busy && gnt) busy <= 1'b0;
else if (busy && BUG == 1 && want) d <= nd;
end
end
endmodule
module unitB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
hold_rule #(.ASSUME(0)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
endmodule
module sysAB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data; wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
always @(*) if (!init0 && BUG == 0) begin h_pend_req: assert (!dp || req); h_pend_held: assert (!dp || dh == data); end
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmoduleStep | req, data, gnt (rule missing) | What happens |
|---|---|---|
1 | 1, 0, 0 | The request waits; A captures word 0 |
2 | 1, 1, 1 | Data changed to 1 while waiting; the grant arrives; A still holds 0 |
3 | - |
|
With the rule asserted on A's input, the tool picks req high at step 1 and low at step 2 with no grant: r_req fails at step 2 (depth 2 passes). Nothing is wrong with A; the rule was placed on the wrong side. The bridge shows the other side in miniature: it owes a downstream rule, and its asserted form catches the fault that breaks it (one word accepted at step 1, out_ready low, input idle at step 2, ovld gone at step 3):
// 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 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
endmoduleRule | Side | Form | Wrong side gives |
|---|---|---|---|
Upstream holds valid until accepted | Assumed at this block's input; asserted on the upstream block's output | Assume here, assert there | Assert on the input fails at once; no assume leaves a false counterexample |
A stalled output holds valid and data | This block's output | Assert | An assume prunes the design and hides the bug |
Reset at the first cycle | Whole harness | Assume once | A free start state fails the good design |
Porting simulation constraints uses the same test. A constraint that states a specification sentence (a legal request has a non-zero length) becomes an assumption on the matching input. A constraint that only biases random stimulus (keep requests sparse so the queue drains) is a distribution, not a rule: formal explores every input, so it has no assumption form, and writing it as one removes legal traffic.
Assumes sit on inputs and cut points only; asserts sit on outputs only. An assume on an output or an assert on an input is a finding on sight.
A constraint ported from simulation cites a specification sentence. Constraints that only narrow random stimulus for convenience stay out.
No rule appears as both an assume and an assert on the same signals.
When a counterexample looks impossible, ask which neighbour could produce its inputs. If none can, a rule is missing; add it as an assumption and write the assertion for the neighbour at once.
That A meets its specification for every environment that keeps the rule. Open: the environment keeping the rule, which only an assertion on the driving block can show.