The symptom is a hang or a missed error: software reads a faulty peripheral, the bus returns the error one cycle after the master gave up waiting, or the error never comes because the property that should have caught the timing was written for zero wait states and the design under check inserts one.
State the cycle of the consequent explicitly. With zero wait states the error response is in the access cycle: request and error in the same cycle, an overlapped relationship. With wait states the request holds across several cycles and the error is due when the access completes, so the property must hold its antecedent through the wait instead of expecting the answer in a fixed cycle. The register block has no bus timing, so this lesson uses a small lesson-local access wrapper with a programmable wait count and an error-generating address.
The textbook form uses implication: the overlapped operator checks the response in the completion cycle, the non-overlapped one a cycle after, which is the mistake shown failing below. The runnable front end does not accept implication, so this is a concept block and the Boolean forms are what runs:
// not-run: implication operators are not accepted by this front end
// a_err_same_cycle: assert property (@(posedge clk) disable iff (rst)
// (psel && penable && pready && bad) |-> perr); // overlapped: error in the completion cycle
// a_err_next_cycle: assert property (@(posedge clk) disable iff (rst)
// (psel && penable && pready && bad) |=> perr); // non-overlapped: one cycle later (the mistake)
// a_no_early_err: assert property (@(posedge clk) disable iff (rst)
// (psel && penable && !pready) |-> !perr); // nothing while the access waitsThe runnable forms are Boolean: the same-cycle form checks perr in the cycle where the antecedent holds, and the next-cycle form reads the antecedent signals through $past and checks perr one cycle after. The cycle table shows the one-wait case on the wrapper (with zero waits the error is in the first access cycle, as the waveform shows):
Step | psel | penable | paddr | pready | perr | What happens |
|---|---|---|---|---|---|---|
n | 1 | 0 | 3 | 0 | 0 | setup phase, wait count loaded as 1 |
n+1 | 1 | 1 | 3 | 0 | 0 | access waits: no error yet (the early-error check) |
n+2 | 1 | 1 | 3 | 1 | 1 | access completes after one wait: error with the completion |
How to read it: the first access has its setup phase at step 2 and its access phase at step 3, where pready, completes_bad and perr all rise together and fall at step 4. The second access loads a wait count of 1 at step 5; at step 6 pready is low, waiting is high and perr stays low; at step 7 the access completes and perr rises in the same step. In both accesses perr follows completes_bad exactly and is never high while waiting is.
The wrapper answers every access, inserts the programmed number of wait cycles, and raises the error exactly when a held access to the unmapped offset completes. Two documented assumptions describe the bus master: an access phase follows a setup phase, and a waiting access is held with the same address until it completes. Without them the proof would check a bus no real master drives; each is owed as an assertion on the master's side. The proof passes with zero waits and with waits, because the property only demands the error when the access completes:
// formal: prove 4 expect pass slang top apb_csr_access
`define FORMAL
module apb_csr_access #(parameter BUG = 0, parameter CHECK = 0) (
input wire clk,
input wire rst,
input wire psel,
input wire penable,
input wire pwrite,
input wire [1:0] paddr,
input wire [7:0] pwdata,
input wire [1:0] waits,
output wire pready,
output wire perr,
output wire [7:0] prdata
);
reg [1:0] wleft;
reg active;
reg err_q;
reg waited; // a wait cycle has already happened in this access
wire setup = psel && !penable;
wire access = psel && penable;
wire bad = (paddr == 2'b11); // the unmapped offset answers with an error
wire done = access && (wleft == 2'd0); // completion cycle
assign pready = done;
assign perr = (BUG == 1) ? err_q : // BUG 1: error one cycle late
(BUG == 2) ? (access && bad) // BUG 2: error raised while still waiting
: (done && bad); // correct: error together with the completion
assign prdata = 8'h00;
always @(posedge clk) begin
if (rst) begin wleft <= 2'd0; active <= 1'b0; err_q <= 1'b0; waited <= 1'b0; end
else begin
if (setup && !active) begin wleft <= waits; active <= 1'b1; end
if (done) active <= 1'b0;
else if (access && wleft != 2'd0) wleft <= wleft - 2'd1;
err_q <= done && bad;
if (done) waited <= 1'b0;
else if (access) waited <= 1'b1;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// documented bus contract, an assumption on the master: an access phase follows a setup phase,
// and a waiting access is held with the same address until it completes
reg was_psel, hold;
reg [1:0] addr_q;
always @(posedge clk) begin
was_psel <= psel;
hold <= access && !done;
addr_q <= paddr;
end
always @(*) if (!init) begin
assume (!penable || was_psel);
assume (!hold || (psel && penable && paddr == addr_q));
end
generate if (CHECK == 0) begin : g_ok
always @(*) if (!init) begin
a_err_same_cycle: assert (!(psel && penable && pready && bad) || perr);
a_no_early_err: assert (!(psel && penable && !pready) || !perr);
end
end else begin : g_late
// the mistake: the error is demanded one cycle AFTER the completion
always @(posedge clk) if (!init && !$past(rst)) begin
a_err_next_cycle: assert (!($past(psel) && $past(penable) && $past(pready) && $past(bad)) || perr);
end
end endgenerate
always @(*) if (!init) begin
c_err_nowait: cover (done && bad && !waited);
c_err_after_wait: cover (done && bad && waited);
end
`endif
endmoduleBoth covers are reached when the same module is run as a cover: the error with zero waits at step 1 and the error after a real wait cycle at step 3. The second cover is only satisfied after a cycle in which the access was waiting, so it is not satisfied by the wait count input alone:
// formal: cover 8 expect reached slang top apb_csr_access
`define FORMAL
module apb_csr_access #(parameter BUG = 0, parameter CHECK = 0) (
input wire clk,
input wire rst,
input wire psel,
input wire penable,
input wire pwrite,
input wire [1:0] paddr,
input wire [7:0] pwdata,
input wire [1:0] waits,
output wire pready,
output wire perr,
output wire [7:0] prdata
);
reg [1:0] wleft;
reg active;
reg err_q;
reg waited; // a wait cycle has already happened in this access
wire setup = psel && !penable;
wire access = psel && penable;
wire bad = (paddr == 2'b11); // the unmapped offset answers with an error
wire done = access && (wleft == 2'd0); // completion cycle
assign pready = done;
assign perr = (BUG == 1) ? err_q : // BUG 1: error one cycle late
(BUG == 2) ? (access && bad) // BUG 2: error raised while still waiting
: (done && bad); // correct: error together with the completion
assign prdata = 8'h00;
always @(posedge clk) begin
if (rst) begin wleft <= 2'd0; active <= 1'b0; err_q <= 1'b0; waited <= 1'b0; end
else begin
if (setup && !active) begin wleft <= waits; active <= 1'b1; end
if (done) active <= 1'b0;
else if (access && wleft != 2'd0) wleft <= wleft - 2'd1;
err_q <= done && bad;
if (done) waited <= 1'b0;
else if (access) waited <= 1'b1;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// documented bus contract, an assumption on the master: an access phase follows a setup phase,
// and a waiting access is held with the same address until it completes
reg was_psel, hold;
reg [1:0] addr_q;
always @(posedge clk) begin
was_psel <= psel;
hold <= access && !done;
addr_q <= paddr;
end
always @(*) if (!init) begin
assume (!penable || was_psel);
assume (!hold || (psel && penable && paddr == addr_q));
end
generate if (CHECK == 0) begin : g_ok
always @(*) if (!init) begin
a_err_same_cycle: assert (!(psel && penable && pready && bad) || perr);
a_no_early_err: assert (!(psel && penable && !pready) || !perr);
end
end else begin : g_late
// the mistake: the error is demanded one cycle AFTER the completion
always @(posedge clk) if (!init && !$past(rst)) begin
a_err_next_cycle: assert (!($past(psel) && $past(penable) && $past(pready) && $past(bad)) || perr);
end
end endgenerate
always @(*) if (!init) begin
c_err_nowait: cover (done && bad && !waited);
c_err_after_wait: cover (done && bad && waited);
end
`endif
endmoduleA proof of the same-cycle property can fail only if some variant breaks it. The first variant returns the error one cycle late (a registered copy), which fails the same-cycle check at the completion cycle. The second raises the error while the access is still waiting, which fails the no-early-error check. Both are bounded runs that find a counterexample:
// formal: bmc 8 expect fail slang top apb_csr_access define BUG=1
`define FORMAL
module apb_csr_access #(parameter BUG = 0, parameter CHECK = 0) (
input wire clk,
input wire rst,
input wire psel,
input wire penable,
input wire pwrite,
input wire [1:0] paddr,
input wire [7:0] pwdata,
input wire [1:0] waits,
output wire pready,
output wire perr,
output wire [7:0] prdata
);
reg [1:0] wleft;
reg active;
reg err_q;
reg waited; // a wait cycle has already happened in this access
wire setup = psel && !penable;
wire access = psel && penable;
wire bad = (paddr == 2'b11); // the unmapped offset answers with an error
wire done = access && (wleft == 2'd0); // completion cycle
assign pready = done;
assign perr = (BUG == 1) ? err_q : // BUG 1: error one cycle late
(BUG == 2) ? (access && bad) // BUG 2: error raised while still waiting
: (done && bad); // correct: error together with the completion
assign prdata = 8'h00;
always @(posedge clk) begin
if (rst) begin wleft <= 2'd0; active <= 1'b0; err_q <= 1'b0; waited <= 1'b0; end
else begin
if (setup && !active) begin wleft <= waits; active <= 1'b1; end
if (done) active <= 1'b0;
else if (access && wleft != 2'd0) wleft <= wleft - 2'd1;
err_q <= done && bad;
if (done) waited <= 1'b0;
else if (access) waited <= 1'b1;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// documented bus contract, an assumption on the master: an access phase follows a setup phase,
// and a waiting access is held with the same address until it completes
reg was_psel, hold;
reg [1:0] addr_q;
always @(posedge clk) begin
was_psel <= psel;
hold <= access && !done;
addr_q <= paddr;
end
always @(*) if (!init) begin
assume (!penable || was_psel);
assume (!hold || (psel && penable && paddr == addr_q));
end
generate if (CHECK == 0) begin : g_ok
always @(*) if (!init) begin
a_err_same_cycle: assert (!(psel && penable && pready && bad) || perr);
a_no_early_err: assert (!(psel && penable && !pready) || !perr);
end
end else begin : g_late
// the mistake: the error is demanded one cycle AFTER the completion
always @(posedge clk) if (!init && !$past(rst)) begin
a_err_next_cycle: assert (!($past(psel) && $past(penable) && $past(pready) && $past(bad)) || perr);
end
end endgenerate
always @(*) if (!init) begin
c_err_nowait: cover (done && bad && !waited);
c_err_after_wait: cover (done && bad && waited);
end
`endif
endmodule// formal: bmc 8 expect fail slang top apb_csr_access define BUG=2
`define FORMAL
module apb_csr_access #(parameter BUG = 0, parameter CHECK = 0) (
input wire clk,
input wire rst,
input wire psel,
input wire penable,
input wire pwrite,
input wire [1:0] paddr,
input wire [7:0] pwdata,
input wire [1:0] waits,
output wire pready,
output wire perr,
output wire [7:0] prdata
);
reg [1:0] wleft;
reg active;
reg err_q;
reg waited; // a wait cycle has already happened in this access
wire setup = psel && !penable;
wire access = psel && penable;
wire bad = (paddr == 2'b11); // the unmapped offset answers with an error
wire done = access && (wleft == 2'd0); // completion cycle
assign pready = done;
assign perr = (BUG == 1) ? err_q : // BUG 1: error one cycle late
(BUG == 2) ? (access && bad) // BUG 2: error raised while still waiting
: (done && bad); // correct: error together with the completion
assign prdata = 8'h00;
always @(posedge clk) begin
if (rst) begin wleft <= 2'd0; active <= 1'b0; err_q <= 1'b0; waited <= 1'b0; end
else begin
if (setup && !active) begin wleft <= waits; active <= 1'b1; end
if (done) active <= 1'b0;
else if (access && wleft != 2'd0) wleft <= wleft - 2'd1;
err_q <= done && bad;
if (done) waited <= 1'b0;
else if (access) waited <= 1'b1;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// documented bus contract, an assumption on the master: an access phase follows a setup phase,
// and a waiting access is held with the same address until it completes
reg was_psel, hold;
reg [1:0] addr_q;
always @(posedge clk) begin
was_psel <= psel;
hold <= access && !done;
addr_q <= paddr;
end
always @(*) if (!init) begin
assume (!penable || was_psel);
assume (!hold || (psel && penable && paddr == addr_q));
end
generate if (CHECK == 0) begin : g_ok
always @(*) if (!init) begin
a_err_same_cycle: assert (!(psel && penable && pready && bad) || perr);
a_no_early_err: assert (!(psel && penable && !pready) || !perr);
end
end else begin : g_late
// the mistake: the error is demanded one cycle AFTER the completion
always @(posedge clk) if (!init && !$past(rst)) begin
a_err_next_cycle: assert (!($past(psel) && $past(penable) && $past(pready) && $past(bad)) || perr);
end
end endgenerate
always @(*) if (!init) begin
c_err_nowait: cover (done && bad && !waited);
c_err_after_wait: cover (done && bad && waited);
end
`endif
endmoduleThe late-error variant fails at the completion cycle: pready is 1 and perr is still 0, because the registered copy rises a cycle later. The early-error variant fails at the first waiting cycle, where perr is 1 while pready is 0.
Writing the check as a non-overlapped relationship, expecting the error one cycle after the completed access, fails on the correct wrapper: the bus is idle again and the error flag is down. The property is wrong and the design is right, and the temptation is to 'fix' the design by delaying the error:
// formal: bmc 8 expect fail slang top apb_csr_access define CHECK=1
`define FORMAL
module apb_csr_access #(parameter BUG = 0, parameter CHECK = 0) (
input wire clk,
input wire rst,
input wire psel,
input wire penable,
input wire pwrite,
input wire [1:0] paddr,
input wire [7:0] pwdata,
input wire [1:0] waits,
output wire pready,
output wire perr,
output wire [7:0] prdata
);
reg [1:0] wleft;
reg active;
reg err_q;
reg waited; // a wait cycle has already happened in this access
wire setup = psel && !penable;
wire access = psel && penable;
wire bad = (paddr == 2'b11); // the unmapped offset answers with an error
wire done = access && (wleft == 2'd0); // completion cycle
assign pready = done;
assign perr = (BUG == 1) ? err_q : // BUG 1: error one cycle late
(BUG == 2) ? (access && bad) // BUG 2: error raised while still waiting
: (done && bad); // correct: error together with the completion
assign prdata = 8'h00;
always @(posedge clk) begin
if (rst) begin wleft <= 2'd0; active <= 1'b0; err_q <= 1'b0; waited <= 1'b0; end
else begin
if (setup && !active) begin wleft <= waits; active <= 1'b1; end
if (done) active <= 1'b0;
else if (access && wleft != 2'd0) wleft <= wleft - 2'd1;
err_q <= done && bad;
if (done) waited <= 1'b0;
else if (access) waited <= 1'b1;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// documented bus contract, an assumption on the master: an access phase follows a setup phase,
// and a waiting access is held with the same address until it completes
reg was_psel, hold;
reg [1:0] addr_q;
always @(posedge clk) begin
was_psel <= psel;
hold <= access && !done;
addr_q <= paddr;
end
always @(*) if (!init) begin
assume (!penable || was_psel);
assume (!hold || (psel && penable && paddr == addr_q));
end
generate if (CHECK == 0) begin : g_ok
always @(*) if (!init) begin
a_err_same_cycle: assert (!(psel && penable && pready && bad) || perr);
a_no_early_err: assert (!(psel && penable && !pready) || !perr);
end
end else begin : g_late
// the mistake: the error is demanded one cycle AFTER the completion
always @(posedge clk) if (!init && !$past(rst)) begin
a_err_next_cycle: assert (!($past(psel) && $past(penable) && $past(pready) && $past(bad)) || perr);
end
end endgenerate
always @(*) if (!init) begin
c_err_nowait: cover (done && bad && !waited);
c_err_after_wait: cover (done && bad && waited);
end
`endif
endmoduleRoot cause: an overlapped response checked with non-overlapped timing. Fix the cycle, not the design: the check belongs in the access cycle.
Every property states its cycle: same-cycle or completion-cycle, never an implied one.
Wait-state behaviour has a cover that needs a real wait cycle, not just a non-zero wait input.
No property demands anything while the access waits: the antecedent repeats until completion, and an early error is itself a failure.
The bus assumptions are listed, each asserted on the master that owes it.
Ask which cycle the specification promises (the completion cycle), then whether the trace has waits: a property written for zero waits fails on the first waited access. Check the waited-case cover before changing anything.
Counting assumes a fixed wait, which the interconnect does not promise. Conditioning on completion holds for any wait count, including zero, so one property covers every timing the bus allows.