From 8289b0d090baa1f8cebd4f0e82eda691adbe78e9 Mon Sep 17 00:00:00 2001 From: Joppe Blondel Date: Sun, 1 Mar 2026 13:52:41 +0100 Subject: [PATCH] Added wb formal script and added other sby tasks --- cores/wb/check_formal.sh | 89 +++++++++++++++++++ .../formal/formal_wb_master_checker.v | 27 ++++++ .../formal/formal_wb_slave_checker.v | 24 +++++ .../jtag_wb_bridge/formal/jtag_wb_bridge.sby | 16 +++- cores/wb/wb_gpio/formal/wb_gpio.sby | 18 +++- cores/wb/wb_mem32/formal/wb_mem32.sby | 18 +++- 6 files changed, 181 insertions(+), 11 deletions(-) create mode 100755 cores/wb/check_formal.sh diff --git a/cores/wb/check_formal.sh b/cores/wb/check_formal.sh new file mode 100755 index 0000000..629685e --- /dev/null +++ b/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 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 485e4c1..e663660 100644 --- a/cores/wb/formal_checker/formal/formal_wb_master_checker.v +++ b/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}; 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 68db9d7..1295f6e 100644 --- a/cores/wb/formal_checker/formal/formal_wb_slave_checker.v +++ b/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}; diff --git a/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge.sby b/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge.sby index 175db36..75c2d00 100644 --- a/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge.sby +++ b/cores/wb/jtag_wb_bridge/formal/jtag_wb_bridge.sby @@ -1,9 +1,19 @@ +[tasks] +prove +cover +bmc + [options] -mode prove -depth 8 +bmc: mode bmc +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}} diff --git a/cores/wb/wb_gpio/formal/wb_gpio.sby b/cores/wb/wb_gpio/formal/wb_gpio.sby index 0fbf6d2..a5088be 100644 --- a/cores/wb/wb_gpio/formal/wb_gpio.sby +++ b/cores/wb/wb_gpio/formal/wb_gpio.sby @@ -1,13 +1,23 @@ +[tasks] +prove +cover +bmc + [options] -mode prove -depth 8 +bmc: mode bmc +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}} \ No newline at end of file diff --git a/cores/wb/wb_mem32/formal/wb_mem32.sby b/cores/wb/wb_mem32/formal/wb_mem32.sby index 2663fc0..670aaf9 100644 --- a/cores/wb/wb_mem32/formal/wb_mem32.sby +++ b/cores/wb/wb_mem32/formal/wb_mem32.sby @@ -1,9 +1,19 @@ +[tasks] +prove +cover +bmc + [options] -mode prove -depth 8 +bmc: mode bmc +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}} \ No newline at end of file