Added new master checker and changed to synchronous reset checks

cores/system/mcu/rtl/mcu_peripherals.v

@@ -99,7 +99,8 @@ module mcu_peripherals (
         .i_wb_dat(gpio_wbs_dat_w),
         .i_wb_adr(gpio_wbs_adr),
         .i_wb_we(gpio_wbs_we),
-        .i_wb_stb(gpio_wbs_stb & gpio_wbs_cyc),
+        .i_wb_stb(gpio_wbs_stb),
+        .i_wb_cyc(gpio_wbs_cyc),
         .i_wb_sel(gpio_wbs_sel),
         .o_wb_rdt(gpio_wbs_dat_r),
         .o_wb_ack(gpio_wbs_ack),
@@ -110,9 +111,7 @@ module mcu_peripherals (
     assign wbs_dat_r[0*32 +: 32] = gpio_wbs_dat_r;
     assign wbs_ack[0] = gpio_wbs_ack;
 
-    wb_countdown_timer #(
+    wb_countdown_timer timer (
-        .address(TIMER_BASE_ADDR)
-    ) timer (
         .i_clk(i_clk),
         .i_rst(i_rst),
         .o_irq(o_timer_irq),

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 (
+module formal_wb_master_checker #(
-    input wire        i_clk,
+    parameter OPT_USE_ERR              = 0,
-    input wire        i_rst,
+    parameter OPT_USE_RTY              = 0,
-    input wire        i_wb_rst,
+
-    input wire [31:0] i_wb_adr,
+    // If 1: require responses only when STB=1 (stricter than spec permission).
-    input wire [31:0] i_wb_dat,
+    // If 0: allow "ghost" responses with STB=0; we only COUNT termination when STB=1.
-    input wire [3:0]  i_wb_sel,
+    parameter OPT_STRICT_RESP_WITH_STB = 0,
-    input wire        i_wb_we,
+
-    input wire        i_wb_stb,
+    // If 1: require ACK/ERR/RTY to be single-cycle pulses.
-    input wire        i_wb_cyc,
+    // If 0: allow them to be held.
-    input wire [31:0] o_wb_rdt,
+    parameter OPT_PULSE_RESP           = 1,
-    input wire        o_wb_ack
+
+    // 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)
-    always @(posedge i_clk) begin
         f_past_valid <= 1'b1;
 
-        // A1: Slave ACK must correspond to either a same-cycle or previous-cycle request
+    wire f_resp_any;
-        if(o_wb_ack)
+    assign f_resp_any = o_wb_ack
-            A1: assume(
+                      | (OPT_USE_ERR ? o_wb_err : 1'b0)
-                (i_wb_cyc && i_wb_stb) ||
+                      | (OPT_USE_RTY ? o_wb_rty : 1'b0);
-                (f_past_valid && $past(i_wb_cyc && i_wb_stb))
-            );
 
-        // A2: Slave must not ACK outside an active cycle
+    // A "real" termination in Classic requires STB high (handshake qualifies the transfer)
-        if(!i_wb_cyc)
+    wire f_terminate;
-            A2: assume(!o_wb_ack);
+    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(
+    // Track exactly one outstanding request (Classic)
-            f_past_valid &&
+    // -----------------------------
-            !$past(i_wb_stb) &&
+    reg f_pending;
-            !i_wb_stb
+    initial f_pending = 1'b0;
-        )
-            A3: assume(!o_wb_ack);
 
-        // R1: Reset must leave the master initialized on the following cycle
+    always @(posedge i_clk or posedge rst_any) begin
-        if(f_past_valid && $past(i_rst || i_wb_rst)) begin
+        if (rst_any) begin
-            R1: assert(!i_wb_cyc);
+            f_pending <= 1'b0;
-            R2: assert(!i_wb_stb);
+        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

cores/wb/formal_checker/formal/formal_wb_slave_checker.v

@@ -1,101 +1,222 @@
-`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 OPT_USE_ERR              = 0,
-    parameter expect_wait_state = 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: 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).
+    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_clk,
-    input wire        i_rst,
+    input  wire              i_rst,
-    input wire        i_wb_rst,
+    input  wire              i_wb_rst,
-    input wire [31:0] i_wb_adr,
+
-    input wire [31:0] i_wb_dat,
+    // Master -> slave
-    input wire [3:0]  i_wb_sel,
+    input  wire              i_wb_cyc,
-    input wire        i_wb_we,
+    input  wire              i_wb_stb,
-    input wire        i_wb_stb,
+    input  wire              i_wb_we,
-    input wire        i_wb_cyc,
+    input  wire [AW-1:0]     i_wb_adr,
-    input wire [31:0] o_wb_rdt,
+    input  wire [DW-1:0]     i_wb_dat,
-    input wire        o_wb_ack
+    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)
-    always @(posedge i_clk) begin
         f_past_valid <= 1'b1;
 
-        // A1: Reset forces cyc=0, stb=0
+    wire f_resp_any;
-        if (i_rst) begin
+    assign f_resp_any = o_wb_ack
-            A1: assume(!i_wb_cyc);
+                      | (OPT_USE_ERR ? o_wb_err : 1'b0)
-            A2: assume(!i_wb_stb);
+                      | (OPT_USE_RTY ? o_wb_rty : 1'b0);
-        end
 
-        // A3: std->cyc, stb never high without cyc
+    // Real termination only counts when STB=1
-        if(i_wb_stb)
+    wire f_terminate;
-            A3: assume(i_wb_cyc);
+    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
+    // Outstanding request tracking (Classic)
-            A4: assume(i_wb_cyc);
+    // -----------------------------
-            A5: assume(i_wb_stb);
+    reg f_pending;
-            A6: assume(i_wb_adr == $past(i_wb_adr));
+    initial f_pending = 1'b0;
-            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
 
-        // R1: ACK must correspond to either a same-cycle or previous-cycle request
+    always @(posedge i_clk or posedge rst_any) begin
-        if(o_wb_ack)
+        if (rst_any) begin
-            R1: assert(
+            f_pending <= 1'b0;
-                (i_wb_cyc && i_wb_stb) ||
+        end else if (!i_wb_cyc) begin
-                (f_past_valid && $past(i_wb_cyc && i_wb_stb))
+            f_pending <= 1'b0;
-            );
-
-        // 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);
         end else begin
-            C6: cover(f_past_valid && !i_rst && !i_wb_rst &&
+            if (!f_pending && i_wb_stb)
-                $past(i_wb_cyc && i_wb_stb) && o_wb_ack);
+                f_pending <= 1'b1;
 
-            // C7: Optional wait-state behavior for slaves that intentionally stall.
+            if (f_terminate)
-            if (expect_wait_state)
+                f_pending <= 1'b0;
-                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));
         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};
+    // -----------------------------
+    // 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
+                // A00: After reset was asserted on the prior clock, assume master is idle
+                A00: assume(!i_wb_cyc);
+                // A01: After reset was asserted on the prior clock, assume master is not strobing
+                A01: assume(!i_wb_stb);
+            end
+
+            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)
+    // -----------------------------
+    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

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}}

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}}'.

cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge_prove/status.path

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

cores/wb/wb_gpio/formal/formal_wb_gpio.v

@@ -1,35 +1,29 @@
 `timescale 1ns/1ps
 
-module formal_wb_gpio #(
+module formal_wb_gpio;
-    parameter [31:0] address = 32'h00000000
-);
     (* gclk *) reg        i_wb_clk;
-    (* anyseq *) reg      i_rst;
     (* anyseq *) reg      i_wb_rst;
     (* anyseq *) reg [31:0] i_wb_adr;
     (* anyseq *) reg [31:0] i_wb_dat;
     (* anyseq *) reg [3:0]  i_wb_sel;
     (* anyseq *) reg      i_wb_we;
     (* anyseq *) reg      i_wb_stb;
+    (* anyseq *) reg      i_wb_cyc;
     (* anyseq *) reg [31:0] i_gpio;
     wire [31:0] o_wb_rdt;
     wire        o_wb_ack;
     wire [31:0] o_gpio;
-    wire        i_wb_cyc;
     reg         f_past_valid;
 
-    assign i_wb_cyc = i_wb_stb || o_wb_ack;
+    wb_gpio dut (
-
+        .i_clk(i_wb_clk),
-    wb_gpio #(
+        .i_rst(i_wb_rst),
-        .address(address)
-    ) dut (
-        .i_wb_clk(i_wb_clk),
-        .i_wb_rst(i_wb_rst),
         .i_wb_adr(i_wb_adr),
         .i_wb_dat(i_wb_dat),
         .i_wb_sel(i_wb_sel),
         .i_wb_we(i_wb_we),
         .i_wb_stb(i_wb_stb),
+        .i_wb_cyc(i_wb_cyc),
         .i_gpio(i_gpio),
         .o_wb_rdt(o_wb_rdt),
         .o_wb_ack(o_wb_ack),
@@ -38,7 +32,7 @@ module formal_wb_gpio #(
 
     formal_wb_slave_checker wb_checker (
         .i_clk(i_wb_clk),
-        .i_rst(i_rst),
+        .i_rst(i_wb_rst),
         .i_wb_rst(i_wb_rst),
         .i_wb_adr(i_wb_adr),
         .i_wb_dat(i_wb_dat),
@@ -56,9 +50,13 @@ module formal_wb_gpio #(
         f_past_valid <= 1'b1;
 
         // R1: reads return the sampled GPIO input on the following cycle
-        if (f_past_valid && !$past(i_wb_rst) && !i_wb_rst && $past(i_wb_stb) && !$past(i_wb_we)) begin
+        if(f_past_valid && 
+                !i_wb_rst && $past(!i_wb_rst) && 
+                o_wb_ack && 
+                $past(i_wb_sel)==4'hf && i_wb_sel==4'hf &&
+                $past(i_wb_cyc & i_wb_stb & !i_wb_we) &&
+                (i_wb_cyc & i_wb_stb & !i_wb_we))
             assert(o_wb_rdt == $past(i_gpio));
-        end
 
         // R2: reset clears the output register and read data register
         if (f_past_valid && $past(i_wb_rst)) begin

cores/wb/wb_gpio/rtl/wb_gpio.v

@@ -1,56 +1,53 @@
-module wb_gpio #(
+module wb_gpio (
-  parameter address = 32'h00000000
+    input  wire         i_clk,
-)(
+    input  wire         i_rst,
-  input  wire        i_wb_clk,
-  input  wire        i_wb_rst,   // optional; tie low if unused
-  input  wire [31:0] i_wb_adr,   // optional; can ignore for single-reg
-  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 [31:0] i_gpio,
 
-  output reg  [31:0] o_wb_rdt,
+    input  wire [31:0]  i_wb_adr,
-  output reg         o_wb_ack,
+    input  wire [31:0]  i_wb_dat,
-  output reg  [31:0] o_gpio
+    output reg  [31:0]  o_wb_rdt,
+    input  wire [3:0]   i_wb_sel,
+    input  wire         i_wb_we,
+    input  wire         i_wb_cyc,
+    input  wire         i_wb_stb,
+    output wire         o_wb_ack,
+
+	input  wire	[31:0]	i_gpio,
+	output wire	[31:0]	o_gpio
 );
 	
-  initial o_gpio <= 32'h00000000;
+	// Registers
-  initial o_wb_rdt <= 32'h00000000;
+	reg [31:0] gpo;
+	wire [31:0] gpi;
+	assign o_gpio = gpo;
+	assign gpi = i_gpio;
 
-  wire addr_check;
+	reg wb_ack = 0;
-  assign addr_check = (i_wb_adr == address);
+	assign o_wb_ack = wb_ack & i_wb_cyc & i_wb_stb;
 
-  // One-cycle ACK pulse per request (works even if stb stays high)
+	always @(posedge i_clk) begin
-  initial o_wb_ack <= 1'b0;
+		if(i_rst) begin
-  always @(posedge i_wb_clk) begin
+			gpo <= 0;
-    if (i_wb_rst) begin
+			wb_ack <= 0;
-      o_wb_ack <= 1'b0;
+			o_wb_rdt <= 0;
-    end else begin
+		end else begin
-      o_wb_ack <= i_wb_stb & ~o_wb_ack; // pulse while stb asserted
+			// Ack generation
-    end
+            wb_ack <= i_wb_cyc & i_wb_stb & !wb_ack;
-  end
 
-  // Read data (combinational or registered; registered here)
+            // Read cycle
-  always @(posedge i_wb_clk) begin
+            if(i_wb_cyc && i_wb_stb && !i_wb_we) begin
-    if (i_wb_rst) begin
+				if(i_wb_sel[0]) o_wb_rdt[7:0] <= gpi[7:0];
-      o_wb_rdt <= 32'h0;
+				if(i_wb_sel[1]) o_wb_rdt[15:8] <= gpi[15:8];
-    end else if (i_wb_stb && !i_wb_we) begin
+				if(i_wb_sel[2]) o_wb_rdt[23:16] <= gpi[23:16];
-      o_wb_rdt <= i_gpio;
+				if(i_wb_sel[3]) o_wb_rdt[31:24] <= gpi[31:24];
-    end
+            end
-  end
+            // write cycle
-
+            if(i_wb_cyc && i_wb_stb && i_wb_we) begin
-  // Write latch (update on the acknowledged cycle)
+				if(i_wb_sel[0]) gpo[7:0] <= i_wb_dat[7:0];
-  always @(posedge i_wb_clk) begin
+				if(i_wb_sel[1]) gpo[15:8] <= i_wb_dat[15:8];
-    if (i_wb_rst) begin
+				if(i_wb_sel[2]) gpo[23:16] <= i_wb_dat[23:16];
-      o_gpio <= 32'h0;
+				if(i_wb_sel[3]) gpo[31:24] <= i_wb_dat[31:24];
-    end else if (i_wb_stb && i_wb_we && addr_check && (i_wb_stb & ~o_wb_ack)) begin
+			end
-      // Apply byte enables (so sb works if the master uses sel)
+		end
-      if (i_wb_sel[0]) o_gpio[7:0]   <= i_wb_dat[7:0];
+	end
-      if (i_wb_sel[1]) o_gpio[15:8]  <= i_wb_dat[15:8];
-      if (i_wb_sel[2]) o_gpio[23:16] <= i_wb_dat[23:16];
-      if (i_wb_sel[3]) o_gpio[31:24] <= i_wb_dat[31:24];
-    end
-  end
 
 endmodule

cores/wb/wb_gpio/wb_gpio.core

@@ -25,8 +25,6 @@ targets:
         filesets:
             - rtl
         toplevel: wb_gpio
-        parameters:
-            - address
             
     formal:
         default_tool: symbiyosys
@@ -35,11 +33,3 @@ targets:
             - formal_rtl
             - formal_cfg
         toplevel: formal_wb_gpio
-        parameters:
-            - address
-
-parameters:
-    address:
-        datatype: int
-        description: Wishbone address matched by this peripheral
-        paramtype: vlogparam

cores/wb/wb_gpio_banks/formal/formal_wb_gpio_banks.v

@@ -1,31 +1,28 @@
 `timescale 1ns/1ps
 
 module formal_wb_gpio_banks #(
-    parameter integer NUM_BANKS = 2,
+    parameter integer num_banks = 2,
-    parameter [31:0] BASE_ADDR = 32'h00000000
 );
-    (* gclk *) reg                  i_wb_clk;
+    (* gclk *) reg                  i_clk;
     (* anyseq *) reg                i_rst;
-    (* anyseq *) reg                i_wb_rst;
     (* anyseq *) reg [31:0]         i_wb_adr;
     (* anyseq *) reg [31:0]         i_wb_dat;
     (* anyseq *) reg [3:0]          i_wb_sel;
     (* anyseq *) reg                i_wb_we;
     (* anyseq *) reg                i_wb_stb;
-    (* anyseq *) reg [NUM_BANKS*32-1:0] i_gpio;
+    (* anyseq *) reg [num_banks*32-1:0] i_gpio;
     wire [31:0]                     o_wb_rdt;
     wire                            o_wb_ack;
-    wire [NUM_BANKS*32-1:0]         o_gpio;
+    wire [num_banks*32-1:0]         o_gpio;
     wire                            i_wb_cyc;
 
     assign i_wb_cyc = i_wb_stb || o_wb_ack;
 
     wb_gpio_banks #(
-        .NUM_BANKS(NUM_BANKS),
+        .num_banks(num_banks)
-        .BASE_ADDR(BASE_ADDR)
     ) dut (
-        .i_wb_clk(i_wb_clk),
+        .i_clk(i_clk),
-        .i_wb_rst(i_wb_rst),
+        .i_rst(i_rst),
         .i_wb_adr(i_wb_adr),
         .i_wb_dat(i_wb_dat),
         .i_wb_sel(i_wb_sel),
@@ -38,9 +35,9 @@ module formal_wb_gpio_banks #(
     );
 
     formal_wb_slave_checker wb_checker (
-        .i_clk(i_wb_clk),
+        .i_clk(i_clk),
         .i_rst(i_rst),
-        .i_wb_rst(i_wb_rst),
+        .i_wb_rst(i_rst),
         .i_wb_adr(i_wb_adr),
         .i_wb_dat(i_wb_dat),
         .i_wb_sel(i_wb_sel),

cores/wb/wb_gpio_banks/formal/wb_gpio_banks.sby

@@ -16,8 +16,10 @@ cover: smtbmc yices
 prove: abc pdr
 
 [script]
+read -formal clog2.vh
 {{"-formal"|gen_reads}}
 prep -top {{top_level}}
 
 [files]
+src/joppeb_util_clog2_1.0/clog2.vh
 {{files}}

cores/wb/wb_gpio_banks/rtl/wb_gpio_banks.v

@@ -1,63 +1,61 @@
-`default_nettype none
+`include "clog2.vh"
 
 module wb_gpio_banks #(
-  parameter integer NUM_BANKS = 4,
+	parameter  num_banks = 4
-  parameter [31:0] BASE_ADDR = 32'h8000_0000
+)(
-) (
+    input  wire         i_clk,
-  input  wire                     i_wb_clk,
+    input  wire         i_rst,
-  input  wire                     i_wb_rst,
+
-  input  wire [31:0]              i_wb_adr,
+    input  wire [31:0]  i_wb_adr,
-  input  wire [31:0]              i_wb_dat,
+    input  wire [31:0]  i_wb_dat,
-  input  wire [3:0]               i_wb_sel,
+    output reg  [31:0]  o_wb_rdt,
-  input  wire                     i_wb_we,
+    input  wire [3:0]   i_wb_sel,
-  input  wire                     i_wb_stb,
+    input  wire         i_wb_we,
-  input  wire [NUM_BANKS*32-1:0]  i_gpio,
+    input  wire         i_wb_cyc,
-  output reg  [31:0]              o_wb_rdt,
+    input  wire         i_wb_stb,
-  output reg                      o_wb_ack,
+    output wire         o_wb_ack,
-  output wire [NUM_BANKS*32-1:0]  o_gpio
+
+	input wire [num_banks*32-1:0] i_gpio,
+	output wire [num_banks*32-1:0] o_gpio
 );
+	localparam sw = `CLOG2(num_banks);
+	wire [num_banks-1:0] bank_sel;
 
-  wire [NUM_BANKS-1:0]           bank_sel;
+	wire [num_banks-1:0] bank_ack;
-  wire [NUM_BANKS-1:0]           bank_stb;
+	wire [num_banks*32-1:0] bank_rdt;
-  wire [NUM_BANKS*32-1:0]        bank_rdt;
-  wire [NUM_BANKS-1:0]           bank_ack;
 
-  genvar gi;
+	genvar gi;
-  generate
+	generate
-    for (gi = 0; gi < NUM_BANKS; gi = gi + 1) begin : gen_gpio
+		for(gi=0; gi<num_banks; gi=gi+1) begin : gen_gpio
-      localparam [31:0] BANK_ADDR = BASE_ADDR + (gi * 4);
+			localparam [2+sw-1:0] addr = gi*4;
+			assign bank_sel[gi] = (i_wb_adr[2+sw-1:0] == addr);
+			wb_gpio u_gpio(
+				.i_clk(i_clk),
+				.i_rst(i_rst),
+				.i_wb_adr(i_wb_adr),
+				.i_wb_dat(i_wb_dat),
+				.i_wb_cyc(i_wb_cyc & bank_sel[gi]),
+				.i_wb_stb(i_wb_stb & bank_sel[gi]),
+				.i_wb_we(i_wb_we),
+				.i_wb_sel(i_wb_sel),
+				.o_wb_ack(bank_ack[gi]),
+				.o_wb_rdt(bank_rdt[gi*32 +: 32]),
+				.i_gpio(i_gpio[gi*32 +: 32]),
+				.o_gpio(o_gpio[gi*32 +: 32])
+			);
+		end
+	endgenerate
 
-      assign bank_sel[gi] = (i_wb_adr == BANK_ADDR);
+	integer bi;
-      assign bank_stb[gi] = i_wb_stb & bank_sel[gi];
+	always @* begin
-
+		o_wb_rdt = 0;
-      wb_gpio #(
+		o_wb_ack = 0;
-        .address(BANK_ADDR)
+		for(bi=0; bi<num_banks; bi=bi+1) begin
-      ) u_gpio (
+			if(bank_sel[bi]) begin
-        .i_wb_clk(i_wb_clk),
+				o_wb_rdt = bank_rdt[bi*32 +: 32];
-        .i_wb_rst(i_wb_rst),
+				o_wb_ack = bank_ack[bi];
-        .i_wb_adr(i_wb_adr),
+			end
-        .i_wb_dat(i_wb_dat),
+		end
-        .i_wb_sel(i_wb_sel),
+	end;
-        .i_wb_we(i_wb_we),
-        .i_wb_stb(bank_stb[gi]),
-        .i_gpio(i_gpio[gi*32 +: 32]),
-        .o_wb_rdt(bank_rdt[gi*32 +: 32]),
-        .o_wb_ack(bank_ack[gi]),
-        .o_gpio(o_gpio[gi*32 +: 32])
-      );
-    end
-  endgenerate
-
-  integer bi;
-  always @* begin
-    o_wb_rdt = 32'h0000_0000;
-    o_wb_ack = 1'b0;
-    for (bi = 0; bi < NUM_BANKS; bi = bi + 1) begin
-      if (bank_sel[bi]) begin
-        o_wb_rdt = bank_rdt[bi*32 +: 32];
-        o_wb_ack = bank_ack[bi];
-      end
-    end
-  end
 
 endmodule

cores/wb/wb_gpio_banks/wb_gpio_banks.core

@@ -7,6 +7,7 @@ filesets:
     rtl:
         depend:
             - joppeb:wb:wb_gpio
+            - joppeb:util:clog2
         files:
             - rtl/wb_gpio_banks.v
         file_type: verilogSource

cores/wb/wb_mem32/rtl/wb_mem32.v

@@ -27,7 +27,7 @@ module wb_mem32 #(
     wire [mem_aw-1:0] wb_word_adr = i_wb_adr[mem_aw+1:2];
 
     assign o_wb_rdt = wb_rdt_r;
-    assign o_wb_ack = wb_ack_r;
+    assign o_wb_ack = wb_ack_r & i_wb_cyc & i_wb_stb;
 
     always @(posedge i_clk) begin
         if (i_rst || i_wb_rst) begin

cores/wb/wb_timer/formal/formal_wb_timer.v

@@ -31,9 +31,7 @@ module formal_wb_timer;
         .o_wb_ack(o_wb_ack)
     );
 
-    formal_wb_slave_checker #(
+    formal_wb_slave_checker wb_checker (
-        .combinatorial_ack(0),
-    ) wb_checker (
         .i_clk(i_clk),
         .i_rst(i_rst),
         .i_wb_rst(i_wb_rst),

cores/wb/wb_timer/rtl/wb_timer.v

@@ -1,8 +1,6 @@
 `timescale 1ns/1ps
 
-module wb_countdown_timer #(
+module wb_countdown_timer (
-    parameter address = 32'h00000000 // Base address of peripheral
-)(
     input  wire         i_clk,
     input  wire         i_rst,
     output wire         o_irq,
@@ -26,7 +24,7 @@ module wb_countdown_timer #(
     reg counter_started = 0;
     reg counter_running = 0;
     reg prev_counter_running = 0;
-    assign o_wb_ack = wb_ack;
+    assign o_wb_ack = wb_ack & i_wb_cyc & i_wb_stb; // Make sure the ack only happend during a cycle
 
     assign o_irq = irq_fired;
 

cores/wb/wb_timer/wb_timer.core

@@ -28,8 +28,6 @@ targets:
         filesets:
             - rtl
         toplevel: wb_countdown_timer
-        parameters:
-            - address
     sim:
         default_tool: icarus
         filesets:
@@ -44,14 +42,9 @@ targets:
             - formal_cfg
         toplevel: formal_wb_timer
         parameters:
-            - address
             - FORMAL=true
 
 parameters:
-    address:
-        datatype: int
-        description: Base address of register set
-        paramtype: vlogparam
     FORMAL:
         datatype: bool
         description: Enable in-module formal-only logic