From 50f71a29859a845a4a321a927fc10157a2783c21 Mon Sep 17 00:00:00 2001 From: Joppe Blondel Date: Mon, 2 Mar 2026 18:02:47 +0100 Subject: [PATCH] Added new master checker and changed to synchronous reset checks --- .../formal/formal_wb_master_checker.v | 278 ++++++++++++------ .../formal/formal_wb_slave_checker.v | 23 +- .../formal/jtag_wb_bridge_prove/config.sby | 13 + .../formal/jtag_wb_bridge_prove/logfile.txt | 2 + .../formal/jtag_wb_bridge_prove/status.path | 1 + 5 files changed, 221 insertions(+), 96 deletions(-) create mode 100644 cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/config.sby create mode 100644 cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/logfile.txt create mode 100644 cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/status.path diff --git a/cores/wb/formal_checker/formal/formal_wb_master_checker.v b/cores/wb/formal_checker/formal/formal_wb_master_checker.v index 13f4ae9..86ad833 100644 --- a/cores/wb/formal_checker/formal/formal_wb_master_checker.v +++ b/cores/wb/formal_checker/formal/formal_wb_master_checker.v @@ -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 ( - 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 +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, + + // Master -> bus + 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, + + // 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 - - // R3: STB never high without CYC - if(i_wb_stb) - R3: assert(i_wb_cyc); - - // 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)); - 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); - end - wire unused = &{1'b0, o_wb_rdt}; + // ----------------------------- + // 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 && $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 + + 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 + + // ----------------------------- + // 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 diff --git a/cores/wb/formal_checker/formal/formal_wb_slave_checker.v b/cores/wb/formal_checker/formal/formal_wb_slave_checker.v index 479bdbc..b277482 100644 --- a/cores/wb/formal_checker/formal/formal_wb_slave_checker.v +++ b/cores/wb/formal_checker/formal/formal_wb_slave_checker.v @@ -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,24 +91,26 @@ 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) - R01: assert(!o_wb_ack); - if (OPT_USE_ERR) R02: assert(!o_wb_err); - if (OPT_USE_RTY) R03: assert(!o_wb_rty); + 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 @@ -216,4 +219,4 @@ module formal_wb_slave_checker #( // TODO `endif -endmodule \ No newline at end of file +endmodule diff --git a/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/config.sby b/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/config.sby new file mode 100644 index 0000000..29b2876 --- /dev/null +++ b/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/config.sby @@ -0,0 +1,13 @@ +[options] +mode prove + +[engines] +abc pdr + +[script] +{{"-formal"|gen_reads}} +prep -top {{top_level}} +clk2fflogic + +[files] +{{files}} diff --git a/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/logfile.txt b/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/logfile.txt new file mode 100644 index 0000000..2c0f76b --- /dev/null +++ b/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/logfile.txt @@ -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}}'. diff --git a/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/status.path b/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/status.path new file mode 100644 index 0000000..9b60661 --- /dev/null +++ b/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/status.path @@ -0,0 +1 @@ +../jtag_wb_bridge/status.sqlite