Some cleanup and added formal for the banks and timer

cores/wb/check_formal.sh

@@ -0,0 +1,91 @@
+#!/bin/sh
+
+# Add or remove cores here. Each entry should be a full FuseSoC VLNV.
+CORES="
+joppeb:wb:wb_mem32
+joppeb:wb:wb_gpio
+joppeb:wb:wb_gpio_banks
+joppeb:wb:jtag_wb_bridge
+joppeb:wb:wb_timer
+"
+
+# Add or remove formal tasks here.
+TASKS="
+bmc
+cover
+prove
+"
+
+total=0
+passed=0
+failed=0
+passed_runs=""
+failed_runs=""
+
+run_task() {
+	core="$1"
+	task="$2"
+	label="$core [$task]"
+	log_file=""
+	total=$((total + 1))
+
+	printf '\n[%d] Running formal %s for %s\n' "$total" "$task" "$core"
+
+	log_file=$(mktemp /tmp/check_formal.XXXXXX) || exit 2
+
+	if \
+		FUSESOC_CORE="$core" \
+		FUSESOC_TASK="$task" \
+		script -qefc 'fusesoc run --target formal "$FUSESOC_CORE" --taskname "$FUSESOC_TASK"' "$log_file" \
+			>/dev/null 2>&1
+	then
+		passed=$((passed + 1))
+		passed_runs="$passed_runs
+$label"
+		printf 'Result: PASS (%s)\n' "$label"
+		rm -f "$log_file"
+		return 0
+	else
+		failed=$((failed + 1))
+		failed_runs="$failed_runs
+$label"
+		printf 'Result: FAIL (%s)\n' "$label"
+		printf 'Captured log for %s:\n' "$label"
+		cat "$log_file" | grep summary
+		rm -f "$log_file"
+		return 1
+	fi
+}
+
+for core in $CORES; do
+	for task in $TASKS; do
+		run_task "$core" "$task"
+	done
+done
+
+printf '\nFormal run summary\n'
+printf '  Total:   %d\n' "$total"
+printf '  Passed:  %d\n' "$passed"
+printf '  Failed:  %d\n' "$failed"
+
+if [ -n "$passed_runs" ]; then
+	printf '\nPassed runs:\n'
+	printf '%s\n' "$passed_runs" | while IFS= read -r run; do
+		if [ -n "$run" ]; then
+			printf '  - %s\n' "$run"
+		fi
+	done
+fi
+
+if [ -n "$failed_runs" ]; then
+	printf '\nFailed runs:\n'
+	printf '%s\n' "$failed_runs" | while IFS= read -r run; do
+		if [ -n "$run" ]; then
+			printf '  - %s\n' "$run"
+		fi
+	done
+fi
+
+if [ "$failed" -ne 0 ]; then
+	exit 1
+fi

cores/wb/formal_checker/formal/formal_wb_master_checker.v

@@ -68,6 +68,31 @@ module formal_wb_master_checker (
         // R4: Once CYC is low, STB must also be low
         if(!i_wb_cyc)
             assert(!i_wb_stb);
+
+        // C0: We eventually initiate a request
+        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb);
+
+        // C1: We eventually get an ACK during an active request
+        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && o_wb_ack);
+
+        // C2: A delayed ACK occurs for a request issued in a previous cycle.
+        // This does not require the request to drop in the ACK cycle.
+        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
+        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: Read and write both occur (even if only once each)
+        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && !i_wb_we);
+        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb &&  i_wb_we);
+
+        // C6: A transfer completes and the master drops CYC sometime after
+        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};

cores/wb/formal_checker/formal/formal_wb_slave_checker.v

@@ -1,6 +1,8 @@
 `timescale 1ns/1ps
 
-module formal_wb_slave_checker (
+module formal_wb_slave_checker #(
+    parameter combinatorial_ack = 0
+) (
     input wire        i_clk,
     input wire        i_rst,
     input wire        i_wb_rst,
@@ -62,6 +64,35 @@ module formal_wb_slave_checker (
             !i_wb_stb
         )
             assert(!o_wb_ack);
+
+        // C0: A request occurs at all
+        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb);
+
+        // C1: A request with write and with read occur
+        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb &&  i_wb_we);
+        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && !i_wb_we);
+
+        // C2: ACK happens during a request (basic progress)
+        cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && o_wb_ack);
+
+        // C3: Exercise the expected ACK timing style for this slave.
+        if (combinatorial_ack) begin
+            cover(f_past_valid && !i_rst && !i_wb_rst &&
+                (i_wb_cyc && i_wb_stb) && o_wb_ack);
+        end else begin
+            cover(f_past_valid && !i_rst && !i_wb_rst &&
+                $past(i_wb_cyc && i_wb_stb) && o_wb_ack);
+
+            // C4: Wait-state behavior for registered/non-zero-wait slaves.
+            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
+
+        // C5: Master ends a cycle (CYC drops) after at least one request
+        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};

cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge.sby

@@ -1,9 +1,19 @@
+[tasks]
+prove
+cover
+bmc
+
 [options]
-mode prove
+bmc: mode bmc
-depth 8
+bmc: depth 16
+cover: mode cover
+cover: depth 16
+prove: mode prove
 
 [engines]
-abc pdr
+bmc: smtbmc yices
+cover: smtbmc yices
+prove: abc pdr
 
 [script]
 {{"-formal"|gen_reads}}

cores/wb/wb_gpio/formal/wb_gpio.sby

@@ -1,9 +1,19 @@
+[tasks]
+prove
+cover
+bmc
+
 [options]
-mode prove
+bmc: mode bmc
-depth 8
+bmc: depth 50
+cover: mode cover
+cover: depth 50
+prove: mode prove
 
 [engines]
-smtbmc z3 parallel.enable=true parallel.threads.max=8
+bmc: smtbmc yices
+cover: smtbmc yices
+prove: abc pdr
 
 [script]
 {{"-formal"|gen_reads}}

cores/wb/wb_gpio_banks/formal/formal_wb_gpio_banks.v

@@ -0,0 +1,53 @@
+`timescale 1ns/1ps
+
+module formal_wb_gpio_banks #(
+    parameter integer NUM_BANKS = 2,
+    parameter [31:0] BASE_ADDR = 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 [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                            i_wb_cyc;
+
+    assign i_wb_cyc = i_wb_stb || o_wb_ack;
+
+    wb_gpio_banks #(
+        .NUM_BANKS(NUM_BANKS),
+        .BASE_ADDR(BASE_ADDR)
+    ) 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_gpio(i_gpio),
+        .o_wb_rdt(o_wb_rdt),
+        .o_wb_ack(o_wb_ack),
+        .o_gpio(o_gpio)
+    );
+
+    formal_wb_slave_checker wb_checker (
+        .i_clk(i_wb_clk),
+        .i_rst(i_rst),
+        .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),
+        .o_wb_rdt(o_wb_rdt),
+        .o_wb_ack(o_wb_ack)
+    );
+endmodule

cores/wb/wb_gpio_banks/formal/wb_gpio_banks.sby

@@ -0,0 +1,23 @@
+[tasks]
+prove
+cover
+bmc
+
+[options]
+bmc: mode bmc
+bmc: depth 50
+cover: mode cover
+cover: depth 50
+prove: mode prove
+
+[engines]
+bmc: smtbmc yices
+cover: smtbmc yices
+prove: abc pdr
+
+[script]
+{{"-formal"|gen_reads}}
+prep -top {{top_level}}
+
+[files]
+{{files}}

cores/wb/wb_gpio_banks/wb_gpio_banks.core

@@ -10,6 +10,16 @@ filesets:
         files:
             - rtl/wb_gpio_banks.v
         file_type: verilogSource
+    formal_rtl:
+        depend:
+            - joppeb:wb:formal_checker
+        files:
+            - formal/formal_wb_gpio_banks.v
+        file_type: verilogSource
+    formal_cfg:
+        files:
+            - formal/wb_gpio_banks.sby
+        file_type: sbyConfigTemplate
 
 targets:
     default:
@@ -19,6 +29,16 @@ targets:
         parameters:
             - NUM_BANKS
             - BASE_ADDR
+    formal:
+        default_tool: symbiyosys
+        filesets:
+            - rtl
+            - formal_rtl
+            - formal_cfg
+        toplevel: formal_wb_gpio_banks
+        parameters:
+            - NUM_BANKS
+            - BASE_ADDR
 
 parameters:
     NUM_BANKS:

cores/wb/wb_mem32/formal/wb_mem32.sby

@@ -1,9 +1,19 @@
+[tasks]
+prove
+cover
+bmc
+
 [options]
-mode prove
+bmc: mode bmc
-depth 8
+bmc: depth 50
+cover: mode cover
+cover: depth 50
+prove: mode prove
 
 [engines]
-smtbmc z3 parallel.enable=true parallel.threads.max=8
+bmc: smtbmc yices
+cover: smtbmc yices
+prove: abc pdr
 
 [script]
 read -formal clog2.vh

cores/wb/wb_timer/formal/formal_wb_timer.v

@@ -0,0 +1,66 @@
+`timescale 1ns/1ps
+
+module formal_wb_timer #(
+    parameter WIDTH = 8,
+    parameter DIVIDER = 0
+);
+    (* gclk *) reg        i_clk;
+    (* anyseq *) reg      i_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_cyc;
+    (* anyseq *) reg      i_wb_stb;
+    wire [31:0]           o_wb_dat;
+    wire                  o_wb_ack;
+    wire                  o_irq;
+    wire                  i_wb_rst;
+    reg                   f_past_valid;
+
+    assign i_wb_rst = 1'b0;
+
+    wb_countdown_timer #(
+        .WIDTH(WIDTH),
+        .DIVIDER(DIVIDER)
+    ) dut (
+        .i_clk(i_clk),
+        .i_rst(i_rst),
+        .o_irq(o_irq),
+        .i_wb_dat(i_wb_dat),
+        .o_wb_dat(o_wb_dat),
+        .i_wb_we(i_wb_we),
+        .i_wb_cyc(i_wb_cyc),
+        .i_wb_stb(i_wb_stb),
+        .o_wb_ack(o_wb_ack)
+    );
+
+    formal_wb_slave_checker #(
+        .combinatorial_ack(1)
+    ) wb_checker (
+        .i_clk(i_clk),
+        .i_rst(i_rst),
+        .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),
+        .o_wb_rdt(o_wb_dat),
+        .o_wb_ack(o_wb_ack)
+    );
+
+    initial f_past_valid = 1'b0;
+
+    always @(posedge i_clk) begin
+        f_past_valid <= 1'b1;
+
+        // Keep the bus idle on the first cycle after reset so the zero-wait ACK
+        // does not collide with the generic slave checker's post-reset rule.
+        if (f_past_valid && $past(i_rst)) begin
+            assume(!i_wb_cyc);
+            assume(!i_wb_stb);
+        end
+    end
+endmodule

cores/wb/wb_timer/formal/wb_timer.sby

@@ -0,0 +1,23 @@
+[tasks]
+prove
+cover
+bmc
+
+[options]
+bmc: mode bmc
+bmc: depth 50
+cover: mode cover
+cover: depth 50
+prove: mode prove
+
+[engines]
+bmc: smtbmc yices
+cover: smtbmc yices
+prove: abc pdr
+
+[script]
+{{"-formal"|gen_reads}}
+prep -top {{top_level}}
+
+[files]
+{{files}}

cores/wb/wb_timer/wb_timer.core

@@ -8,6 +8,16 @@ filesets:
         files:
             - rtl/wb_timer.v
         file_type: verilogSource
+    formal_rtl:
+        depend:
+            - joppeb:wb:formal_checker
+        files:
+            - formal/formal_wb_timer.v
+        file_type: verilogSource
+    formal_cfg:
+        files:
+            - formal/wb_timer.sby
+        file_type: sbyConfigTemplate
 
 targets:
     default:
@@ -17,6 +27,16 @@ targets:
         parameters:
             - WIDTH
             - DIVIDER
+    formal:
+        default_tool: symbiyosys
+        filesets:
+            - rtl
+            - formal_rtl
+            - formal_cfg
+        toplevel: formal_wb_timer
+        parameters:
+            - WIDTH
+            - DIVIDER
 
 parameters:
     WIDTH: