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

New slave checker and updated gpio and gpio_banks

Browse Source
This commit is contained in:
Joppe Blondel
2026-03-02 13:48:30 +01:00
parent a6a5c6ea3f
commit 628972ccaa
13 changed files with 334 additions and 245 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -1,101 +1,219 @@
`timescale 1ns/1ps
// formal_wb_slave_checker.v
//
// Wishbone Classic slave-side protocol checker (plain Verilog).
// Use when your DUT is a *slave* and the bus/master is the environment.
module formal_wb_slave_checker #(
parameter combinatorial_ack = 0,
parameter expect_wait_state = 0
parameter OPT_USE_ERR = 0,
parameter OPT_USE_RTY = 0,
// If 1: require slave to only assert responses when STB=1 (stricter profile).
// If 0: allow "ghost" responses with STB=0; termination still only counts when STB=1.
parameter OPT_STRICT_RESP_WITH_STB = 0,
// If 1: require termination signals to be pulses (1 cycle).
// 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).
parameter OPT_STRICT_RESET = 1,
// If 1: assert read data stable while ACK is held (useful if you allow ACK-hold).
parameter OPT_ASSERT_RDATA_STABLE_DURING_ACK = 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,
input wire i_wb_cyc,
input wire [31:0] o_wb_rdt,
input wire o_wb_ack
input wire i_clk,
input wire i_rst,
input wire i_wb_rst,
// Master -> slave
input wire i_wb_cyc,
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,
// 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: Reset forces cyc=0, stb=0
if (i_rst) begin
A1: assume(!i_wb_cyc);
A2: assume(!i_wb_stb);
end
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);
// A3: std->cyc, stb never high without cyc
if(i_wb_stb)
A3: assume(i_wb_cyc);
// Real termination only counts when STB=1
wire f_terminate;
assign f_terminate = i_wb_cyc && i_wb_stb && f_resp_any;
// A4-A9: once a request starts, hold it stable until the slave responds
if(f_past_valid && $past(i_wb_cyc && i_wb_stb && !o_wb_ack)) begin
A4: assume(i_wb_cyc);
A5: assume(i_wb_stb);
A6: assume(i_wb_adr == $past(i_wb_adr));
A7: assume(i_wb_dat == $past(i_wb_dat));
A8: assume(i_wb_sel == $past(i_wb_sel));
A9: assume(i_wb_we == $past(i_wb_we));
end
// -----------------------------
// Outstanding request tracking (Classic)
// -----------------------------
reg f_pending;
initial f_pending = 1'b0;
// R1: ACK must correspond to either a same-cycle or previous-cycle request
if(o_wb_ack)
R1: assert(
(i_wb_cyc && i_wb_stb) ||
(f_past_valid && $past(i_wb_cyc && i_wb_stb))
);
// R2: !CYC->!ACK : no ghost acks
if(!i_wb_cyc)
R2: assert(!o_wb_ack);
// R3: Reset must leave the slave initialized on the following cycle
if(f_past_valid && $past(i_rst || i_wb_rst))
R3: assert(!o_wb_ack);
// R4: once STB has been dropped for a full cycle, ACK must be low
if(
f_past_valid &&
!$past(i_wb_stb) &&
!i_wb_stb
)
R4: assert(!o_wb_ack);
// C1: A request occurs at all
C1: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb);
// C2-C3: A request with write and with read occur
C2: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && i_wb_we);
C3: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && !i_wb_we);
// C4: ACK happens during a request (basic progress)
C4: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && o_wb_ack);
// C5-C7: Exercise the expected ACK timing style for this slave.
if (combinatorial_ack) begin
C5: cover(f_past_valid && !i_rst && !i_wb_rst &&
(i_wb_cyc && i_wb_stb) && o_wb_ack);
always @(posedge i_clk or posedge rst_any) begin
if (rst_any) begin
f_pending <= 1'b0;
end else if (!i_wb_cyc) begin
f_pending <= 1'b0;
end else begin
C6: cover(f_past_valid && !i_rst && !i_wb_rst &&
$past(i_wb_cyc && i_wb_stb) && o_wb_ack);
if (!f_pending && i_wb_stb)
f_pending <= 1'b1;
// C7: Optional wait-state behavior for slaves that intentionally stall.
if (expect_wait_state)
C7: 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));
if (f_terminate)
f_pending <= 1'b0;
end
// C8: Master ends a cycle (CYC drops) after at least one request
C8: cover(f_past_valid && !i_rst && !i_wb_rst &&
$past(i_wb_cyc && i_wb_stb) && !i_wb_cyc);
end
wire unused = &{1'b0, o_wb_rdt};
endmodule
// -----------------------------
// Reset rules (recommended)
// -----------------------------
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
A00: assume(!i_wb_cyc);
// A01: During reset, assume the master is not strobing
A01: assume(!i_wb_stb);
end
// R01: Slave should not respond during reset (prevents silly traces)
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
// -----------------------------
// Master/environment assumptions (Classic rules)
// -----------------------------
always @(posedge i_clk) if (f_past_valid && !rst_any) begin
// A10: STB must imply CYC
if (i_wb_stb) begin
A10: assume(i_wb_cyc);
end
// A11: While pending and not terminated, master holds CYC asserted
if ($past(f_pending) && !$past(f_terminate)) begin
A11: assume(i_wb_cyc);
end
// A12: While pending and not terminated, master holds STB asserted
if ($past(f_pending) && !$past(f_terminate)) begin
A12: assume(i_wb_stb);
end
// A13: Address stable while pending and not terminated
if ($past(f_pending) && !$past(f_terminate)) begin
A13: assume(i_wb_adr == $past(i_wb_adr));
end
// A14: WE stable while pending and not terminated
if ($past(f_pending) && !$past(f_terminate)) begin
A14: assume(i_wb_we == $past(i_wb_we));
end
// A15: SEL stable while pending and not terminated
if ($past(f_pending) && !$past(f_terminate)) begin
A15: assume(i_wb_sel == $past(i_wb_sel));
end
// A16: Write data stable while pending and not terminated
if ($past(f_pending) && !$past(f_terminate)) begin
A16: assume(i_wb_dat == $past(i_wb_dat));
end
end
// -----------------------------
// Slave/DUT assertions (response sanity)
// -----------------------------
always @(posedge i_clk) if (f_past_valid && !rst_any) begin
// R10: Any response must occur only during an active cycle
if (f_resp_any) begin
R10: assert(i_wb_cyc);
end
// R11: Optional strict profile: response only when STB=1
if (OPT_STRICT_RESP_WITH_STB && f_resp_any) begin
R11: assert(i_wb_stb);
end
// R12-R14: Mutual exclusion of termination signals (recommended)
if (o_wb_ack) begin
if (OPT_USE_ERR) R12s1: assert(!o_wb_err);
if (OPT_USE_RTY) R12s2: assert(!o_wb_rty);
end
if (OPT_USE_ERR && o_wb_err) begin
R13s1: assert(!o_wb_ack);
if (OPT_USE_RTY) R13s2: assert(!o_wb_rty);
end
if (OPT_USE_RTY && o_wb_rty) begin
R14s1: assert(!o_wb_ack);
if (OPT_USE_ERR) R14s2: assert(!o_wb_err);
end
// R15-R17: Optional pulse-only responses
if (OPT_PULSE_RESP) begin
if ($past(o_wb_ack)) begin
R15: assert(!o_wb_ack);
end
if (OPT_USE_ERR && $past(o_wb_err)) begin
R16: assert(!o_wb_err);
end
if (OPT_USE_RTY && $past(o_wb_rty)) begin
R17: assert(!o_wb_rty);
end
end
// R18: A real termination (STB && response) should only happen when a request is pending.
if (i_wb_stb && f_resp_any) begin
R18: assert(f_pending || $past(f_pending));
end
// R19: Optional read-data stability while ACK is held (only relevant if ACK can be held)
if (OPT_ASSERT_RDATA_STABLE_DURING_ACK) begin
if (o_wb_ack && !i_wb_we && $past(o_wb_ack)) begin
R19: assert(o_wb_rdt == $past(o_wb_rdt));
end
end
// R20: If no cycle, no responses (strong sanity rule)
if (!i_wb_cyc) begin
R20: assert(!f_resp_any);
end
end
// -----------------------------
// Coverage: exercise the slave (useful witness traces)
// -----------------------------
// TODO
`endif
endmodule