Added wb formal script and added other sby tasks

cores/wb/check_formal.sh

@@ -0,0 +1,89 @@
+#!/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:jtag_wb_bridge
+"
+
+# 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,33 @@ 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: ACK in the *same* cycle as the request (allowed by your A1)
+        cover(f_past_valid && !i_rst && !i_wb_rst && (i_wb_cyc && i_wb_stb) && o_wb_ack);
+
+        // C3: ACK one cycle *after* the request (also allowed by your A1)
+        // 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));
+
+        // 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

@@ -62,6 +62,30 @@ 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: ACK same-cycle vs one-cycle-late (mirrors your R1 definition)
+        cover(f_past_valid && !i_rst && !i_wb_rst && (i_wb_cyc && i_wb_stb) && o_wb_ack);
+        cover(f_past_valid && !i_rst && !i_wb_rst && $past(i_wb_cyc && i_wb_stb) && o_wb_ack);
+
+        // C4: “wait state” from the slave POV: request persists without ACK
+        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: 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,13 +1,23 @@
+[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}}
 prep -top {{top_level}}
 
 [files]
-{{files}}
+{{files}}

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
@@ -12,4 +22,4 @@ prep -top {{top_level}}
 
 [files]
 src/joppeb_util_clog2_1.0/clog2.vh
-{{files}}
+{{files}}