Added some stuff from modem and added formal

cores/wb/formal_checker/formal/formal_wb_master_checker.v

@@ -0,0 +1,73 @@
+`timescale 1ns/1ps
+
+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
+);
+    reg f_past_valid;
+
+    initial f_past_valid = 1'b0;
+
+    always @(posedge i_clk) begin
+        f_past_valid <= 1'b1;
+
+        // A1: Slave ACK must correspond to either a same-cycle or previous-cycle request
+        if(o_wb_ack)
+            assume(
+                (i_wb_cyc && i_wb_stb) ||
+                (f_past_valid && $past(i_wb_cyc && i_wb_stb))
+            );
+
+        // A2: Slave must not ACK outside an active cycle
+        if(!i_wb_cyc)
+            assume(!o_wb_ack);
+
+        // 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
+        )
+            assume(!o_wb_ack);
+
+        // R1: Reset must leave the master initialized on the following cycle
+        if(f_past_valid && $past(i_rst || i_wb_rst)) begin
+            assert(!i_wb_cyc);
+            assert(!i_wb_stb);
+        end
+
+        // R2: STB never high without CYC
+        if(i_wb_stb)
+            assert(i_wb_cyc);
+
+        // R3: 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) &&
+            !o_wb_ack &&
+            !(i_rst || i_wb_rst)
+        ) begin
+            assert(i_wb_cyc);
+            assert(i_wb_stb);
+            assert(i_wb_adr == $past(i_wb_adr));
+            assert(i_wb_dat == $past(i_wb_dat));
+            assert(i_wb_sel == $past(i_wb_sel));
+            assert(i_wb_we == $past(i_wb_we));
+        end
+
+        // R4: Once CYC is low, STB must also be low
+        if(!i_wb_cyc)
+            assert(!i_wb_stb);
+    end
+
+    wire unused = &{1'b0, o_wb_rdt};
+endmodule

cores/wb/formal_checker/formal/formal_wb_slave_checker.v

@@ -0,0 +1,68 @@
+`timescale 1ns/1ps
+
+module formal_wb_slave_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
+);
+    reg f_past_valid;
+
+    initial f_past_valid = 1'b0;
+
+    always @(posedge i_clk) begin
+        f_past_valid <= 1'b1;
+
+        // A1: Reset forces cyc=0, stb=0
+        if (i_rst) begin
+            assume(!i_wb_cyc);
+            assume(!i_wb_stb);
+        end
+
+        // A2: std->cyc, stb never high without cyc
+        if(i_wb_stb)
+            assume(i_wb_cyc);
+
+        // A3: 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
+            assume(i_wb_cyc);
+            assume(i_wb_stb);
+            assume(i_wb_adr == $past(i_wb_adr));
+            assume(i_wb_dat == $past(i_wb_dat));
+            assume(i_wb_sel == $past(i_wb_sel));
+            assume(i_wb_we == $past(i_wb_we));
+        end
+
+        // R1: ACK must correspond to either a same-cycle or previous-cycle request
+        if(o_wb_ack)
+            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)
+            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))
+            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
+        )
+            assert(!o_wb_ack);
+    end
+
+    wire unused = &{1'b0, o_wb_rdt};
+endmodule

cores/wb/formal_checker/formal_checker.core

@@ -0,0 +1,16 @@
+CAPI=2:
+
+name: joppeb:wb:formal_checker:1.0
+description: Reusable formal Wishbone protocol checkers
+
+filesets:
+    formal_rtl:
+        files:
+            - formal/formal_wb_slave_checker.v
+            - formal/formal_wb_master_checker.v
+        file_type: verilogSource
+
+targets:
+    default:
+        filesets:
+            - formal_rtl