joppe/fpga_modem
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Added new master checker and changed to synchronous reset checks

Browse Source
This commit is contained in:
Joppe Blondel
2026-03-02 18:02:47 +01:00
parent 628972ccaa
commit 50f71a2985
5 changed files with 221 additions and 96 deletions
Download Patch File Download Diff File Expand all files Collapse all files

262
cores/wb/formal_checker/formal/formal_wb_master_checker.v
View File

@@ -1,99 +1,205 @@
`timescale 1ns/1ps
// formal_wb_master_checker.v
//
// Wishbone Classic master-side protocol checker (plain Verilog).
// Use when your DUT is a *master* and the bus/slave is the environment.
module formal_wb_master_checker (
module formal_wb_master_checker #(
parameter OPT_USE_ERR = 0,
parameter OPT_USE_RTY = 0,
// If 1: require responses only when STB=1 (stricter than spec permission).
// If 0: allow "ghost" responses with STB=0; we only COUNT termination when STB=1.
parameter OPT_STRICT_RESP_WITH_STB = 0,
// If 1: require ACK/ERR/RTY to be single-cycle pulses.
// If 0: allow them to be held.
parameter OPT_PULSE_RESP = 1,
// If 1: after a synchronous reset has been asserted for one clock,
// require the master to hold CYC/STB low.
parameter OPT_STRICT_RESET = 1,
// Optional widths
parameter AW = 32,
parameter DW = 32,
parameter SW = 4
) (
input wire i_clk,
input wire i_rst,
input wire i_wb_rst,
input wire [31:0] i_wb_adr,
input wire [31:0] i_wb_dat,
input wire [3:0] i_wb_sel,
input wire i_wb_we,
input wire i_wb_stb,
// Master -> bus
input wire i_wb_cyc,
input wire [31:0] o_wb_rdt,
input wire o_wb_ack
input wire i_wb_stb,
input wire i_wb_we,
input wire [AW-1:0] i_wb_adr,
input wire [DW-1:0] i_wb_dat,
input wire [SW-1:0] i_wb_sel,
// Bus/slave -> master
input wire o_wb_ack,
input wire o_wb_err,
input wire o_wb_rty,
input wire [DW-1:0] o_wb_rdt
);
`ifdef FORMAL
// -----------------------------
// Reset combine
// -----------------------------
wire rst_any;
assign rst_any = i_rst | i_wb_rst;
// -----------------------------
// Formal infrastructure
// -----------------------------
reg f_past_valid;
initial f_past_valid = 1'b0;
always @(posedge i_clk) begin
always @(posedge i_clk)
f_past_valid <= 1'b1;
// A1: Slave ACK must correspond to either a same-cycle or previous-cycle request
if(o_wb_ack)
A1: assume(
(i_wb_cyc && i_wb_stb) ||
(f_past_valid && $past(i_wb_cyc && i_wb_stb))
);
wire f_resp_any;
assign f_resp_any = o_wb_ack
| (OPT_USE_ERR ? o_wb_err : 1'b0)
| (OPT_USE_RTY ? o_wb_rty : 1'b0);
// A2: Slave must not ACK outside an active cycle
if(!i_wb_cyc)
A2: assume(!o_wb_ack);
// A "real" termination in Classic requires STB high (handshake qualifies the transfer)
wire f_terminate;
assign f_terminate = i_wb_cyc && i_wb_stb && f_resp_any;
// A3: Once STB has been low for a full cycle, slave ACK must be low
if(
f_past_valid &&
!$past(i_wb_stb) &&
!i_wb_stb
)
A3: assume(!o_wb_ack);
// -----------------------------
// Track exactly one outstanding request (Classic)
// -----------------------------
reg f_pending;
initial f_pending = 1'b0;
// R1: Reset must leave the master initialized on the following cycle
if(f_past_valid && $past(i_rst || i_wb_rst)) begin
R1: assert(!i_wb_cyc);
R2: assert(!i_wb_stb);
always @(posedge i_clk or posedge rst_any) begin
if (rst_any) begin
f_pending <= 1'b0;
end else if (!i_wb_cyc) begin
// Dropping CYC ends the bus cycle and clears any outstanding request
f_pending <= 1'b0;
end else begin
// Start pending when STB is asserted and none is pending
if (!f_pending && i_wb_stb)
f_pending <= 1'b1;
// Clear pending only on a real termination (STB && response)
if (f_terminate)
f_pending <= 1'b0;
end
end
// R3: STB never high without CYC
if(i_wb_stb)
R3: assert(i_wb_cyc);
// -----------------------------
// Reset rules (Wishbone synchronous reset semantics)
// -----------------------------
always @(posedge i_clk) if (f_past_valid) begin
if (rst_any) begin
// R00: Monitor pending state must be cleared during reset
R00: assert(f_pending == 1'b0);
// R4-R9: Once a request starts, hold it stable until the slave responds
if(
f_past_valid &&
!$past(i_rst || i_wb_rst) &&
$past(i_wb_cyc && i_wb_stb && !o_wb_ack) &&
!o_wb_ack &&
!(i_rst || i_wb_rst)
) begin
R4: assert(i_wb_cyc);
R5: assert(i_wb_stb);
R6: assert(i_wb_adr == $past(i_wb_adr));
R7: assert(i_wb_dat == $past(i_wb_dat));
R8: assert(i_wb_sel == $past(i_wb_sel));
R9: assert(i_wb_we == $past(i_wb_we));
if (OPT_STRICT_RESET && $past(rst_any)) begin
// R01: After reset was asserted on the prior clock, master must be idle
R01: assert(!i_wb_cyc);
// R02: After reset was asserted on the prior clock, master must not strobe
R02: assert(!i_wb_stb);
end
// R10: Once CYC is low, STB must also be low
if(!i_wb_cyc)
R10: assert(!i_wb_stb);
// C1: We eventually initiate a request
C1: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb);
// C2: We eventually get an ACK during an active request
C2: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && o_wb_ack);
// C3: A delayed ACK occurs for a request issued in a previous cycle.
// This does not require the request to drop in the ACK cycle.
C3: cover(f_past_valid && !i_rst && !i_wb_rst &&
$past(i_wb_cyc && i_wb_stb) && o_wb_ack);
// C4: A “wait state” happens: request asserted, no ACK for at least 1 cycle
C4: cover(f_past_valid && !i_rst && !i_wb_rst &&
$past(i_wb_cyc && i_wb_stb && !o_wb_ack) &&
(i_wb_cyc && i_wb_stb && !o_wb_ack));
// C5-C6: Read and write both occur (even if only once each)
C5: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && !i_wb_we);
C6: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && i_wb_we);
// C7: A transfer completes and the master drops CYC sometime after
C7: cover(f_past_valid && !i_rst && !i_wb_rst &&
$past(i_wb_cyc && i_wb_stb && o_wb_ack) && !i_wb_cyc);
if ($past(rst_any)) begin
// A00: After reset was asserted on the prior clock, environment should not respond
A00: assume(!o_wb_ack);
if (OPT_USE_ERR) A01: assume(!o_wb_err);
if (OPT_USE_RTY) A02: assume(!o_wb_rty);
end
end
end
wire unused = &{1'b0, o_wb_rdt};
// -----------------------------
// Master-side RULES (ASSERTIONS)
// -----------------------------
always @(posedge i_clk) if (f_past_valid && !rst_any) begin
// R10: STB must imply CYC (no strobe outside of a cycle)
if (i_wb_stb) begin
R10: assert(i_wb_cyc);
end
// R11: While a request is pending and NOT terminated, master must keep CYC asserted
if ($past(f_pending) && !$past(f_terminate)) begin
R11: assert(i_wb_cyc);
end
// R12: While a request is pending and NOT terminated, master must keep STB asserted
if ($past(f_pending) && !$past(f_terminate)) begin
R12: assert(i_wb_stb);
end
// R13: Address stable while pending and not terminated
if ($past(f_pending) && !$past(f_terminate)) begin
R13: assert(i_wb_adr == $past(i_wb_adr));
end
// R14: WE stable while pending and not terminated
if ($past(f_pending) && !$past(f_terminate)) begin
R14: assert(i_wb_we == $past(i_wb_we));
end
// R15: SEL stable while pending and not terminated
if ($past(f_pending) && !$past(f_terminate)) begin
R15: assert(i_wb_sel == $past(i_wb_sel));
end
// R16: Write data stable while pending and not terminated
if ($past(f_pending) && !$past(f_terminate)) begin
R16: assert(i_wb_dat == $past(i_wb_dat));
end
end
// -----------------------------
// Environment SLAVE assumptions
// -----------------------------
always @(posedge i_clk) if (f_past_valid && !rst_any) begin
// A10: Any response must occur only during an active cycle
if (f_resp_any) begin
A10: assume(i_wb_cyc);
end
// A11: Optional strict profile: response only when STB=1
if (OPT_STRICT_RESP_WITH_STB && f_resp_any) begin
A11: assume(i_wb_stb);
end
// A12-A14: Mutual exclusion between ACK/ERR/RTY (recommended)
if (o_wb_ack) begin
if (OPT_USE_ERR) A12s1: assume(!o_wb_err);
if (OPT_USE_RTY) A12s2: assume(!o_wb_rty);
end
if (OPT_USE_ERR && o_wb_err) begin
A13s1: assume(!o_wb_ack);
if (OPT_USE_RTY) A13s2: assume(!o_wb_rty);
end
if (OPT_USE_RTY && o_wb_rty) begin
A14s1: assume(!o_wb_ack);
if (OPT_USE_ERR) A14s2: assume(!o_wb_err);
end
// A15-A17: Optional pulse-only responses
if (OPT_PULSE_RESP) begin
if ($past(o_wb_ack)) begin
A15: assume(!o_wb_ack);
end
if (OPT_USE_ERR && $past(o_wb_err)) begin
A16: assume(!o_wb_err);
end
if (OPT_USE_RTY && $past(o_wb_rty)) begin
A17: assume(!o_wb_rty);
end
end
end
// -----------------------------
// Coverage: explore protocol space ("state diagram" witnesses)
// -----------------------------
// TODO
`endif
endmodule

15
cores/wb/formal_checker/formal/formal_wb_slave_checker.v
View File

@@ -15,7 +15,8 @@ module formal_wb_slave_checker #(
// If 0: allow them to be held.
parameter OPT_PULSE_RESP = 1,
// If 1: during reset require master to hold CYC/STB low (assumption; common convention).
// If 1: after a synchronous reset has been asserted for one clock,
// require the master to hold CYC/STB low.
parameter OPT_STRICT_RESET = 1,
// If 1: assert read data stable while ACK is held (useful if you allow ACK-hold).
@@ -90,26 +91,28 @@ module formal_wb_slave_checker #(
end
// -----------------------------
// Reset rules (recommended)
// Reset rules (Wishbone synchronous reset semantics)
// -----------------------------
always @(posedge i_clk) if (f_past_valid) begin
if (rst_any) begin
// R00: Monitor pending state must be cleared during reset
R00: assert(f_pending == 1'b0);
if (OPT_STRICT_RESET) begin
// A00: During reset, assume the master is not attempting a bus cycle
if (OPT_STRICT_RESET && $past(rst_any)) begin
// A00: After reset was asserted on the prior clock, assume master is idle
A00: assume(!i_wb_cyc);
// A01: During reset, assume the master is not strobing
// A01: After reset was asserted on the prior clock, assume master is not strobing
A01: assume(!i_wb_stb);
end
// R01: Slave should not respond during reset (prevents silly traces)
if ($past(rst_any)) begin
// R01: After reset was asserted on the prior clock, slave must not respond
R01: assert(!o_wb_ack);
if (OPT_USE_ERR) R02: assert(!o_wb_err);
if (OPT_USE_RTY) R03: assert(!o_wb_rty);
end
end
end
// -----------------------------
// Master/environment assumptions (Classic rules)

13
cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/config.sby Normal file
View File

@@ -0,0 +1,13 @@
[options]
mode prove
[engines]
abc pdr
[script]
{{"-formal"|gen_reads}}
prep -top {{top_level}}
clk2fflogic
[files]
{{files}}

2
cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/logfile.txt Normal file
View File

@@ -0,0 +1,2 @@
SBY 17:52:48 [/data/joppe/projects/fusesoc_test/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove] Removing directory '/data/joppe/projects/fusesoc_test/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove'.
SBY 17:52:48 [/data/joppe/projects/fusesoc_test/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove] Copy '/data/joppe/projects/fusesoc_test/cores/wb/jtag_wb_bridge/formal/{{files}}' to '/data/joppe/projects/fusesoc_test/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/src/{{files}}'.

1
cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/status.path Normal file
View File

@@ -0,0 +1 @@
../jtag_wb_bridge/status.sqlite