From 7b46ae5e87b66a6516eae94ffc487d7b45a3e7c6 Mon Sep 17 00:00:00 2001 From: Joppe Blondel Date: Sun, 1 Mar 2026 14:12:12 +0100 Subject: [PATCH] Some cleanup and added formal for the banks and timer --- cores/wb/check_formal.sh | 2 + .../formal/formal_wb_master_checker.v | 10 ++- .../formal/formal_wb_slave_checker.v | 23 ++++--- .../formal/formal_wb_gpio_banks.v | 53 +++++++++++++++ .../wb/wb_gpio_banks/formal/wb_gpio_banks.sby | 23 +++++++ cores/wb/wb_gpio_banks/wb_gpio_banks.core | 20 ++++++ cores/wb/wb_timer/formal/formal_wb_timer.v | 66 +++++++++++++++++++ cores/wb/wb_timer/formal/wb_timer.sby | 23 +++++++ cores/wb/wb_timer/wb_timer.core | 20 ++++++ 9 files changed, 226 insertions(+), 14 deletions(-) create mode 100644 cores/wb/wb_gpio_banks/formal/formal_wb_gpio_banks.v create mode 100644 cores/wb/wb_gpio_banks/formal/wb_gpio_banks.sby create mode 100644 cores/wb/wb_timer/formal/formal_wb_timer.v create mode 100644 cores/wb/wb_timer/formal/wb_timer.sby diff --git a/cores/wb/check_formal.sh b/cores/wb/check_formal.sh index 629685e..4df22a7 100755 --- a/cores/wb/check_formal.sh +++ b/cores/wb/check_formal.sh @@ -4,7 +4,9 @@ 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. 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 e663660..68dc7c6 100644 --- a/cores/wb/formal_checker/formal/formal_wb_master_checker.v +++ b/cores/wb/formal_checker/formal/formal_wb_master_checker.v @@ -75,12 +75,10 @@ module formal_wb_master_checker ( // 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)); + // 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 && 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 1295f6e..866e730 100644 --- a/cores/wb/formal_checker/formal/formal_wb_slave_checker.v +++ b/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, @@ -73,14 +75,19 @@ module formal_wb_slave_checker ( // 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); + // 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” 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)); + // 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 && diff --git a/cores/wb/wb_gpio_banks/formal/formal_wb_gpio_banks.v b/cores/wb/wb_gpio_banks/formal/formal_wb_gpio_banks.v new file mode 100644 index 0000000..505d4c1 --- /dev/null +++ b/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 diff --git a/cores/wb/wb_gpio_banks/formal/wb_gpio_banks.sby b/cores/wb/wb_gpio_banks/formal/wb_gpio_banks.sby new file mode 100644 index 0000000..be55a8b --- /dev/null +++ b/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}} diff --git a/cores/wb/wb_gpio_banks/wb_gpio_banks.core b/cores/wb/wb_gpio_banks/wb_gpio_banks.core index c91c852..0fac524 100644 --- a/cores/wb/wb_gpio_banks/wb_gpio_banks.core +++ b/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: diff --git a/cores/wb/wb_timer/formal/formal_wb_timer.v b/cores/wb/wb_timer/formal/formal_wb_timer.v new file mode 100644 index 0000000..848c8e3 --- /dev/null +++ b/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 diff --git a/cores/wb/wb_timer/formal/wb_timer.sby b/cores/wb/wb_timer/formal/wb_timer.sby new file mode 100644 index 0000000..be55a8b --- /dev/null +++ b/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}} diff --git a/cores/wb/wb_timer/wb_timer.core b/cores/wb/wb_timer/wb_timer.core index 628aff2..47503f9 100644 --- a/cores/wb/wb_timer/wb_timer.core +++ b/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: