Most connections are conditional: a debug path that exists only in one mode, a clock that reaches a block only when its enable is set, a bus that belongs to one master at a time. Prove the connection without the mode condition and the proof fails on legal behaviour; prove it only in the default mode and the untested mode hides a real escape, a path that is live when the specification says it is dead. The symptom of an escape is usually a security or power finding, not a functional one: data reaching a block that should be isolated.
Each row carries its condition, and the check is an implication guarded by it: in the mode, destination equals source; outside the mode, the destination must show nothing of the source. Both directions are proved, and each mode gets a cover so an untested mode is visible. A proof run with a harness that pins the mode is one of the classic false passes: the lesson pairs the constrained proof with its mode cover, and the cover is what exposes it. The mode itself is state, here a two-bit register, so its encoding is a property too: one-hot or zero, and the illegal value 11 must never occur.
The matrix below is the whole contract for the small module used in the worked example. It has a data output dst that follows the selected source, and a debug mirror dbg of source A that exists in mode A only:
Mode register |
|
|
|---|---|---|
01 (mode A) | source A | source A |
10 (mode B) | source B | must read 0x00 |
00 (none) | 0x00 | must read 0x00 |
11 | illegal: never occurs | illegal: never occurs |
The module is lesson-local. Pulses set_a and set_b write the mode register; both together choose A. The proof checks the encoding, each in-mode row, the idle row, the mirror in mode A, and the escape row: outside mode A the mirror reads zero. Three covers show the proof exercised both modes and the colliding pulses:
// formal: prove 4 expect pass slang top mode_mux
`define FORMAL
module mode_mux #(parameter BUG = 0, parameter PIN = 0) (
input wire clk,
input wire rst,
input wire set_a,
input wire set_b,
input wire [7:0] src_a,
input wire [7:0] src_b,
output wire [7:0] dst,
output wire [7:0] dbg
);
reg [1:0] sel; // 2'b01 = mode A, 2'b10 = mode B, 2'b00 = none; 2'b11 is illegal
always @(posedge clk) begin
if (rst) sel <= 2'b00;
else if (set_a && set_b) sel <= (BUG == 2) ? 2'b11 : 2'b01;
else if (set_a) sel <= 2'b01;
else if (set_b) sel <= 2'b10;
end
assign dst = (sel == 2'b01) ? src_a : (sel == 2'b10) ? src_b : 8'h00;
// the debug mirror of source A is specified for mode A only
assign dbg = (sel == 2'b01 || (BUG == 1 && sel == 2'b10)) ? src_a : 8'h00;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init && PIN != 0) assume (!set_b);
always @(*) if (!init) begin
m_onehot_or_zero: assert (sel != 2'b11);
m_dst_a: assert (!(sel == 2'b01) || dst == src_a);
m_dst_b: assert (!(sel == 2'b10) || dst == src_b);
m_dst_none: assert (!(sel == 2'b00) || dst == 8'h00);
m_link_in_a: assert (!(sel == 2'b01) || dbg == src_a);
m_link_escape: assert ((sel == 2'b01) || dbg == 8'h00);
c_mode_a: cover (sel == 2'b01);
c_mode_b: cover (sel == 2'b10);
c_both_pulses: cover (set_a && set_b);
end
`endif
endmoduleThe first partner is the escape. In mode B the mirror still follows source A, a link that is live in a mode where it must be dead. Every in-mode row still passes, because mode A is right; only the escape row fails, which is why the escape direction must be checked on its own:
Step | set_a / set_b | mode register |
| Outcome |
|---|---|---|---|---|
0 | - | arbitrary | - | reset cycle, not checked |
1 | 0 / 1 | 00 | 0x00 | mode B requested |
2 | - | 10 (mode B) | source A | counterexample: |
// formal: bmc 6 expect fail slang top mode_mux define BUG=1
`define FORMAL
module mode_mux #(parameter BUG = 0, parameter PIN = 0) (
input wire clk,
input wire rst,
input wire set_a,
input wire set_b,
input wire [7:0] src_a,
input wire [7:0] src_b,
output wire [7:0] dst,
output wire [7:0] dbg
);
reg [1:0] sel; // 2'b01 = mode A, 2'b10 = mode B, 2'b00 = none; 2'b11 is illegal
always @(posedge clk) begin
if (rst) sel <= 2'b00;
else if (set_a && set_b) sel <= (BUG == 2) ? 2'b11 : 2'b01;
else if (set_a) sel <= 2'b01;
else if (set_b) sel <= 2'b10;
end
assign dst = (sel == 2'b01) ? src_a : (sel == 2'b10) ? src_b : 8'h00;
// the debug mirror of source A is specified for mode A only
assign dbg = (sel == 2'b01 || (BUG == 1 && sel == 2'b10)) ? src_a : 8'h00;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init && PIN != 0) assume (!set_b);
always @(*) if (!init) begin
m_onehot_or_zero: assert (sel != 2'b11);
m_dst_a: assert (!(sel == 2'b01) || dst == src_a);
m_dst_b: assert (!(sel == 2'b10) || dst == src_b);
m_dst_none: assert (!(sel == 2'b00) || dst == 8'h00);
m_link_in_a: assert (!(sel == 2'b01) || dbg == src_a);
m_link_escape: assert ((sel == 2'b01) || dbg == 8'h00);
c_mode_a: cover (sel == 2'b01);
c_mode_b: cover (sel == 2'b10);
c_both_pulses: cover (set_a && set_b);
end
`endif
endmoduleRoot cause: the mirror enable ignores the mode in one mode. Fix the wiring so the mode gates the mirror in every mode; where a leak is intended (a broadcast), write it as its own table row with its own condition instead of weakening the escape check. The second partner is the encoding: when both pulses arrive together this variant stores 11 instead of choosing A. Outputs look harmless there, which is why the encoding has its own check:
// formal: bmc 6 expect fail slang top mode_mux define BUG=2
`define FORMAL
module mode_mux #(parameter BUG = 0, parameter PIN = 0) (
input wire clk,
input wire rst,
input wire set_a,
input wire set_b,
input wire [7:0] src_a,
input wire [7:0] src_b,
output wire [7:0] dst,
output wire [7:0] dbg
);
reg [1:0] sel; // 2'b01 = mode A, 2'b10 = mode B, 2'b00 = none; 2'b11 is illegal
always @(posedge clk) begin
if (rst) sel <= 2'b00;
else if (set_a && set_b) sel <= (BUG == 2) ? 2'b11 : 2'b01;
else if (set_a) sel <= 2'b01;
else if (set_b) sel <= 2'b10;
end
assign dst = (sel == 2'b01) ? src_a : (sel == 2'b10) ? src_b : 8'h00;
// the debug mirror of source A is specified for mode A only
assign dbg = (sel == 2'b01 || (BUG == 1 && sel == 2'b10)) ? src_a : 8'h00;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init && PIN != 0) assume (!set_b);
always @(*) if (!init) begin
m_onehot_or_zero: assert (sel != 2'b11);
m_dst_a: assert (!(sel == 2'b01) || dst == src_a);
m_dst_b: assert (!(sel == 2'b10) || dst == src_b);
m_dst_none: assert (!(sel == 2'b00) || dst == 8'h00);
m_link_in_a: assert (!(sel == 2'b01) || dbg == src_a);
m_link_escape: assert ((sel == 2'b01) || dbg == 8'h00);
c_mode_a: cover (sel == 2'b01);
c_mode_b: cover (sel == 2'b10);
c_both_pulses: cover (set_a && set_b);
end
`endif
endmodulem_onehot_or_zero fails at step 2: both pulses at step 1, the register holds 11 at step 2. The row m_dst_a does not catch it, because 11 selects neither mode.
A harness that rules out set_b, for example because a test only ever used mode A, makes the escape invisible. The bounded check below runs the escape variant with that constraint and passes. It is bounded to 8 and it never visits mode B, so it says nothing about mode B. The cover run is what shows it: with the constraint, c_mode_b is not reached within 8, and a cover not reached within a bound is inconclusive. Here the reason is known, the constraint removes the only input that selects mode B, so the unreached cover is the alarm:
// formal: bmc 8 expect pass slang top mode_mux define BUG=1 define PIN=1
`define FORMAL
module mode_mux #(parameter BUG = 0, parameter PIN = 0) (
input wire clk,
input wire rst,
input wire set_a,
input wire set_b,
input wire [7:0] src_a,
input wire [7:0] src_b,
output wire [7:0] dst,
output wire [7:0] dbg
);
reg [1:0] sel; // 2'b01 = mode A, 2'b10 = mode B, 2'b00 = none; 2'b11 is illegal
always @(posedge clk) begin
if (rst) sel <= 2'b00;
else if (set_a && set_b) sel <= (BUG == 2) ? 2'b11 : 2'b01;
else if (set_a) sel <= 2'b01;
else if (set_b) sel <= 2'b10;
end
assign dst = (sel == 2'b01) ? src_a : (sel == 2'b10) ? src_b : 8'h00;
// the debug mirror of source A is specified for mode A only
assign dbg = (sel == 2'b01 || (BUG == 1 && sel == 2'b10)) ? src_a : 8'h00;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init && PIN != 0) assume (!set_b);
always @(*) if (!init) begin
m_onehot_or_zero: assert (sel != 2'b11);
m_dst_a: assert (!(sel == 2'b01) || dst == src_a);
m_dst_b: assert (!(sel == 2'b10) || dst == src_b);
m_dst_none: assert (!(sel == 2'b00) || dst == 8'h00);
m_link_in_a: assert (!(sel == 2'b01) || dbg == src_a);
m_link_escape: assert ((sel == 2'b01) || dbg == 8'h00);
c_mode_a: cover (sel == 2'b01);
c_mode_b: cover (sel == 2'b10);
c_both_pulses: cover (set_a && set_b);
end
`endif
endmodule// formal: cover 8 expect fail slang top mode_mux define PIN=1
`define FORMAL
module mode_mux #(parameter BUG = 0, parameter PIN = 0) (
input wire clk,
input wire rst,
input wire set_a,
input wire set_b,
input wire [7:0] src_a,
input wire [7:0] src_b,
output wire [7:0] dst,
output wire [7:0] dbg
);
reg [1:0] sel; // 2'b01 = mode A, 2'b10 = mode B, 2'b00 = none; 2'b11 is illegal
always @(posedge clk) begin
if (rst) sel <= 2'b00;
else if (set_a && set_b) sel <= (BUG == 2) ? 2'b11 : 2'b01;
else if (set_a) sel <= 2'b01;
else if (set_b) sel <= 2'b10;
end
assign dst = (sel == 2'b01) ? src_a : (sel == 2'b10) ? src_b : 8'h00;
// the debug mirror of source A is specified for mode A only
assign dbg = (sel == 2'b01 || (BUG == 1 && sel == 2'b10)) ? src_a : 8'h00;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init && PIN != 0) assume (!set_b);
always @(*) if (!init) begin
m_onehot_or_zero: assert (sel != 2'b11);
m_dst_a: assert (!(sel == 2'b01) || dst == src_a);
m_dst_b: assert (!(sel == 2'b10) || dst == src_b);
m_dst_none: assert (!(sel == 2'b00) || dst == 8'h00);
m_link_in_a: assert (!(sel == 2'b01) || dbg == src_a);
m_link_escape: assert ((sel == 2'b01) || dbg == 8'h00);
c_mode_a: cover (sel == 2'b01);
c_mode_b: cover (sel == 2'b10);
c_both_pulses: cover (set_a && set_b);
end
`endif
endmoduleThe same covers on the unconstrained module are all reached:
// formal: cover 6 expect reached slang top mode_mux
`define FORMAL
module mode_mux #(parameter BUG = 0, parameter PIN = 0) (
input wire clk,
input wire rst,
input wire set_a,
input wire set_b,
input wire [7:0] src_a,
input wire [7:0] src_b,
output wire [7:0] dst,
output wire [7:0] dbg
);
reg [1:0] sel; // 2'b01 = mode A, 2'b10 = mode B, 2'b00 = none; 2'b11 is illegal
always @(posedge clk) begin
if (rst) sel <= 2'b00;
else if (set_a && set_b) sel <= (BUG == 2) ? 2'b11 : 2'b01;
else if (set_a) sel <= 2'b01;
else if (set_b) sel <= 2'b10;
end
assign dst = (sel == 2'b01) ? src_a : (sel == 2'b10) ? src_b : 8'h00;
// the debug mirror of source A is specified for mode A only
assign dbg = (sel == 2'b01 || (BUG == 1 && sel == 2'b10)) ? src_a : 8'h00;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init && PIN != 0) assume (!set_b);
always @(*) if (!init) begin
m_onehot_or_zero: assert (sel != 2'b11);
m_dst_a: assert (!(sel == 2'b01) || dst == src_a);
m_dst_b: assert (!(sel == 2'b10) || dst == src_b);
m_dst_none: assert (!(sel == 2'b00) || dst == 8'h00);
m_link_in_a: assert (!(sel == 2'b01) || dbg == src_a);
m_link_escape: assert ((sel == 2'b01) || dbg == 8'h00);
c_mode_a: cover (sel == 2'b01);
c_mode_b: cover (sel == 2'b10);
c_both_pulses: cover (set_a && set_b);
end
`endif
endmoduleEvery row has a condition, and every condition has a cover proving the mode was exercised.
The escape direction is checked, not just the intended direction: the proof says what must not connect.
The mode encoding itself is checked: a one-hot assumption that the logic never enforces is an assumption, not a fact.
A failure outside the intended mode is a table bug until the schematic says otherwise: check the condition first. A failure inside the mode with a correct condition is wiring. A proof that passes but whose mode cover is unreached is the dangerous case, a constrained proof hiding a mode: treat an unreached mode cover as a failure, exactly as an unreached antecedent cover fails a signoff, and say in the report that the unreached cover is inconclusive until the constraint is removed or the mode is shown unreachable by an invariant.
In-mode rows only say the intended link works. The escape is a link that works where it must not, so only the check written for the other modes can see it.