A synchroniser proved safe by a protocol check still needs its structural analysis, an isolation cell still needs its power intent verified, a pipeline still needs its full property set. The formal part of each neighbour flow is small and precise: check the protocol around an abstracted element. Teaching the whole neighbour flow here would duplicate three courses; skipping the boundary would leave readers proving the wrong thing. This lesson draws the line and links out.
Structural analysis is not formal: cone tracing, clock-domain structure and power-intent structure are computed, not proved. The formal contribution is the protocol around the abstraction: the synchroniser becomes a bounded delay of two to three cycles and the proof checks bounded response across it; isolation becomes a clamp value while the source is off and the proof checks the clamp; a CPU pipeline property becomes a latency rule the CPU course owns in full. Each row of the table below says what is structural, what is formal, and who owns it:
Flow | Structural (computed) | Formal (proved here) | Owner |
|---|---|---|---|
clock crossings | domain structure, synchroniser presence | bounded-latency protocol across a 2-3 cycle abstract delay | CDC signoff flow |
low power | isolation and retention placement | clamp value while source is off | low-power verification |
CPU pipeline | hazard structure | fixed-latency response rules | CPU pipeline checks |
The lesson-local check below models the crossing as a delay line with an agreed range: the request arrives after two cycles, or after three when a free input says the crossing resolved late. That is a model of the crossing, not the synchroniser circuit. The destination may stall, and one fairness entry owned by the neighbour flow bounds it: while a request is pending the destination is not stalled for a third consecutive cycle, written as an assumption with a stall cover beside it. The window is derived: three cycles of delay plus two of stall, so a request is acknowledged with at most five pending cycles counted. The intended crossing proves the bound, and the bound is exact:
// formal: prove 8 expect pass slang top sync_check
`define FORMAL
module sync_check #(parameter BUG = 0, parameter BOUND = 5) (
input wire clk,
input wire rst,
input wire req,
input wire extra, // free: the crossing resolves one cycle late
input wire dst_ready,
output wire ack
);
reg r1, r2, r3, r4;
always @(posedge clk) begin
if (rst) begin r1 <= 1'b0; r2 <= 1'b0; r3 <= 1'b0; r4 <= 1'b0; end
else begin r1 <= req; r2 <= r1; r3 <= r2; r4 <= r3; end
end
// the abstraction: the request arrives after two cycles, or three when extra is set. BUG 1 is a four-cycle crossing.
wire arrived = (BUG == 1) ? r4 : (extra ? r3 : r2);
assign ack = arrived && dst_ready;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// documented fairness, owned by the neighbour flow: while a request is pending the
// destination is not stalled for a third consecutive cycle
reg [1:0] sc;
always @(posedge clk) begin
if (rst) sc <= 2'd0;
else if (req && !dst_ready && sc != 2'd2) sc <= sc + 2'd1;
else if (!req || dst_ready) sc <= 2'd0;
end
always @(*) if (!init) assume (!(req && !dst_ready && sc == 2'd2));
reg [2:0] age; // consecutive cycles with a request pending and no acknowledge
always @(posedge clk) begin
if (rst) age <= 3'd0;
else if (req && !ack) age <= age + 3'd1;
else age <= 3'd0;
end
always @(*) if (!init) begin
s_bounded: assert (age <= BOUND);
c_req_ack: cover (req && ack);
c_stall: cover (req && !dst_ready);
c_slow: cover (ack && !r2 && r3);
end
`endif
endmodule// formal: bmc 12 expect fail slang top sync_check define BOUND=4
`define FORMAL
module sync_check #(parameter BUG = 0, parameter BOUND = 5) (
input wire clk,
input wire rst,
input wire req,
input wire extra, // free: the crossing resolves one cycle late
input wire dst_ready,
output wire ack
);
reg r1, r2, r3, r4;
always @(posedge clk) begin
if (rst) begin r1 <= 1'b0; r2 <= 1'b0; r3 <= 1'b0; r4 <= 1'b0; end
else begin r1 <= req; r2 <= r1; r3 <= r2; r4 <= r3; end
end
// the abstraction: the request arrives after two cycles, or three when extra is set. BUG 1 is a four-cycle crossing.
wire arrived = (BUG == 1) ? r4 : (extra ? r3 : r2);
assign ack = arrived && dst_ready;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// documented fairness, owned by the neighbour flow: while a request is pending the
// destination is not stalled for a third consecutive cycle
reg [1:0] sc;
always @(posedge clk) begin
if (rst) sc <= 2'd0;
else if (req && !dst_ready && sc != 2'd2) sc <= sc + 2'd1;
else if (!req || dst_ready) sc <= 2'd0;
end
always @(*) if (!init) assume (!(req && !dst_ready && sc == 2'd2));
reg [2:0] age; // consecutive cycles with a request pending and no acknowledge
always @(posedge clk) begin
if (rst) age <= 3'd0;
else if (req && !ack) age <= age + 3'd1;
else age <= 3'd0;
end
always @(*) if (!init) begin
s_bounded: assert (age <= BOUND);
c_req_ack: cover (req && ack);
c_stall: cover (req && !dst_ready);
c_slow: cover (ack && !r2 && r3);
end
`endif
endmoduleThe second run tightens the bound to four and the intended crossing fails it, so five is the exact window and not a loose one. The covers show the abstraction still allows real behaviour: a request is acknowledged, the destination stalls, and an acknowledge arrives through the late path:
// formal: cover 10 expect reached slang top sync_check
`define FORMAL
module sync_check #(parameter BUG = 0, parameter BOUND = 5) (
input wire clk,
input wire rst,
input wire req,
input wire extra, // free: the crossing resolves one cycle late
input wire dst_ready,
output wire ack
);
reg r1, r2, r3, r4;
always @(posedge clk) begin
if (rst) begin r1 <= 1'b0; r2 <= 1'b0; r3 <= 1'b0; r4 <= 1'b0; end
else begin r1 <= req; r2 <= r1; r3 <= r2; r4 <= r3; end
end
// the abstraction: the request arrives after two cycles, or three when extra is set. BUG 1 is a four-cycle crossing.
wire arrived = (BUG == 1) ? r4 : (extra ? r3 : r2);
assign ack = arrived && dst_ready;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// documented fairness, owned by the neighbour flow: while a request is pending the
// destination is not stalled for a third consecutive cycle
reg [1:0] sc;
always @(posedge clk) begin
if (rst) sc <= 2'd0;
else if (req && !dst_ready && sc != 2'd2) sc <= sc + 2'd1;
else if (!req || dst_ready) sc <= 2'd0;
end
always @(*) if (!init) assume (!(req && !dst_ready && sc == 2'd2));
reg [2:0] age; // consecutive cycles with a request pending and no acknowledge
always @(posedge clk) begin
if (rst) age <= 3'd0;
else if (req && !ack) age <= age + 3'd1;
else age <= 3'd0;
end
always @(*) if (!init) begin
s_bounded: assert (age <= BOUND);
c_req_ack: cover (req && ack);
c_stall: cover (req && !dst_ready);
c_slow: cover (ack && !r2 && r3);
end
`endif
endmoduleThe partner is a crossing that has grown a fourth stage, outside the documented range, without widening the window. The bound fails: the request arrives at the fourth cycle, the destination stalls two cycles, and the pending count reaches six. Change the window only with the abstraction owner, never alone:
Step | req | dst_ready | arrived (fourth stage) | ack | pending count |
|---|---|---|---|---|---|
1 | 1 | 0 | 0 | 0 | 0 |
2 | 1 | 1 | 0 | 0 | 1 |
3 | 1 | 0 | 0 | 0 | 2 |
4 | 1 | 1 | 0 | 0 | 3 |
5 | 1 | 0 | 1 | 0 | 4 (arrived, destination stalls) |
6 | 1 | 0 | 1 | 0 | 5 (second stall) |
7 | 0 | 0 | 1 | 0 | 6: counterexample, |
// formal: bmc 7 expect pass slang top sync_check define BUG=1
`define FORMAL
module sync_check #(parameter BUG = 0, parameter BOUND = 5) (
input wire clk,
input wire rst,
input wire req,
input wire extra, // free: the crossing resolves one cycle late
input wire dst_ready,
output wire ack
);
reg r1, r2, r3, r4;
always @(posedge clk) begin
if (rst) begin r1 <= 1'b0; r2 <= 1'b0; r3 <= 1'b0; r4 <= 1'b0; end
else begin r1 <= req; r2 <= r1; r3 <= r2; r4 <= r3; end
end
// the abstraction: the request arrives after two cycles, or three when extra is set. BUG 1 is a four-cycle crossing.
wire arrived = (BUG == 1) ? r4 : (extra ? r3 : r2);
assign ack = arrived && dst_ready;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// documented fairness, owned by the neighbour flow: while a request is pending the
// destination is not stalled for a third consecutive cycle
reg [1:0] sc;
always @(posedge clk) begin
if (rst) sc <= 2'd0;
else if (req && !dst_ready && sc != 2'd2) sc <= sc + 2'd1;
else if (!req || dst_ready) sc <= 2'd0;
end
always @(*) if (!init) assume (!(req && !dst_ready && sc == 2'd2));
reg [2:0] age; // consecutive cycles with a request pending and no acknowledge
always @(posedge clk) begin
if (rst) age <= 3'd0;
else if (req && !ack) age <= age + 3'd1;
else age <= 3'd0;
end
always @(*) if (!init) begin
s_bounded: assert (age <= BOUND);
c_req_ack: cover (req && ack);
c_stall: cover (req && !dst_ready);
c_slow: cover (ack && !r2 && r3);
end
`endif
endmodule// formal: bmc 8 expect fail slang top sync_check define BUG=1
`define FORMAL
module sync_check #(parameter BUG = 0, parameter BOUND = 5) (
input wire clk,
input wire rst,
input wire req,
input wire extra, // free: the crossing resolves one cycle late
input wire dst_ready,
output wire ack
);
reg r1, r2, r3, r4;
always @(posedge clk) begin
if (rst) begin r1 <= 1'b0; r2 <= 1'b0; r3 <= 1'b0; r4 <= 1'b0; end
else begin r1 <= req; r2 <= r1; r3 <= r2; r4 <= r3; end
end
// the abstraction: the request arrives after two cycles, or three when extra is set. BUG 1 is a four-cycle crossing.
wire arrived = (BUG == 1) ? r4 : (extra ? r3 : r2);
assign ack = arrived && dst_ready;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// documented fairness, owned by the neighbour flow: while a request is pending the
// destination is not stalled for a third consecutive cycle
reg [1:0] sc;
always @(posedge clk) begin
if (rst) sc <= 2'd0;
else if (req && !dst_ready && sc != 2'd2) sc <= sc + 2'd1;
else if (!req || dst_ready) sc <= 2'd0;
end
always @(*) if (!init) assume (!(req && !dst_ready && sc == 2'd2));
reg [2:0] age; // consecutive cycles with a request pending and no acknowledge
always @(posedge clk) begin
if (rst) age <= 3'd0;
else if (req && !ack) age <= age + 3'd1;
else age <= 3'd0;
end
always @(*) if (!init) begin
s_bounded: assert (age <= BOUND);
c_req_ack: cover (req && ack);
c_stall: cover (req && !dst_ready);
c_slow: cover (ack && !r2 && r3);
end
`endif
endmoduleThe abstraction boundary is the whole point: this proof says nothing about metastability, resolution time or the synchroniser circuit itself. Those belong to the structural analysis and the electrical domain, linked below. What it says is that the protocol tolerates the documented delay range, which is the only claim formal can own here.
The abstraction is documented with its range and its owner: two to three cycles here, owned by the CDC flow.
The window is derived from the range plus the stall bound, and shown exact by a run that tightens it.
The proof never claims synchroniser correctness, isolation correctness or pipeline correctness: only the boundary rule.
Each neighbour row links to the owning topic page, never to a templated child.
A boundary failure first asks whether the abstraction still holds: a four-cycle crossing against a three-cycle abstraction fails the proof correctly, and the fix is re-agreeing the range, not weakening the property. Teach nothing about synchroniser design here; check the protocol, link the structure.
The abstraction range grows by one cycle and the window widens with it, agreed with the CDC owner. The proof shape stays identical; only the documented numbers move, and the covers must still reach.