joppe/fpga_modem
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Some cleanup and added formal for the banks and timer

Browse Source
This commit is contained in:
Joppe Blondel
2026-03-01 14:12:12 +01:00
parent 8289b0d090
commit 7b46ae5e87
9 changed files with 226 additions and 14 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
cores/wb/check_formal.sh
View File

@@ -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.

10
cores/wb/formal_checker/formal/formal_wb_master_checker.v
View File

@@ -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 &&

17
cores/wb/formal_checker/formal/formal_wb_slave_checker.v
View File

@@ -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
// 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 &&

53
cores/wb/wb_gpio_banks/formal/formal_wb_gpio_banks.v Normal file
View File

@@ -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

23
cores/wb/wb_gpio_banks/formal/wb_gpio_banks.sby Normal file
View File

@@ -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}}

20
cores/wb/wb_gpio_banks/wb_gpio_banks.core
View File

@@ -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:

66
cores/wb/wb_timer/formal/formal_wb_timer.v Normal file
View File

@@ -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

23
cores/wb/wb_timer/formal/wb_timer.sby Normal file
View File

@@ -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}}

20
cores/wb/wb_timer/wb_timer.core
View File

@@ -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: