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

new timer

Browse Source
This commit is contained in:
Joppe Blondel
2026-03-01 17:16:44 +01:00
parent 7b46ae5e87
commit abe0668787
19 changed files with 381 additions and 155 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -22,14 +22,14 @@ module formal_wb_master_checker (
// A1: Slave ACK must correspond to either a same-cycle or previous-cycle request
if(o_wb_ack)
assume(
A1: assume(
(i_wb_cyc && i_wb_stb) ||
(f_past_valid && $past(i_wb_cyc && i_wb_stb))
);
// A2: Slave must not ACK outside an active cycle
if(!i_wb_cyc)
assume(!o_wb_ack);
A2: assume(!o_wb_ack);
// A3: Once STB has been low for a full cycle, slave ACK must be low
if(
@@ -37,19 +37,19 @@ module formal_wb_master_checker (
!$past(i_wb_stb) &&
!i_wb_stb
)
assume(!o_wb_ack);
A3: assume(!o_wb_ack);
// R1: Reset must leave the master initialized on the following cycle
if(f_past_valid && $past(i_rst || i_wb_rst)) begin
assert(!i_wb_cyc);
assert(!i_wb_stb);
R1: assert(!i_wb_cyc);
R2: assert(!i_wb_stb);
end
// R2: STB never high without CYC
// R3: STB never high without CYC
if(i_wb_stb)
assert(i_wb_cyc);
R3: assert(i_wb_cyc);
// R3: Once a request starts, hold it stable until the slave responds
// R4-R9: Once a request starts, hold it stable until the slave responds
if(
f_past_valid &&
!$past(i_rst || i_wb_rst) &&
@@ -57,40 +57,40 @@ module formal_wb_master_checker (
!o_wb_ack &&
!(i_rst || i_wb_rst)
) begin
assert(i_wb_cyc);
assert(i_wb_stb);
assert(i_wb_adr == $past(i_wb_adr));
assert(i_wb_dat == $past(i_wb_dat));
assert(i_wb_sel == $past(i_wb_sel));
assert(i_wb_we == $past(i_wb_we));
R4: assert(i_wb_cyc);
R5: assert(i_wb_stb);
R6: assert(i_wb_adr == $past(i_wb_adr));
R7: assert(i_wb_dat == $past(i_wb_dat));
R8: assert(i_wb_sel == $past(i_wb_sel));
R9: assert(i_wb_we == $past(i_wb_we));
end
// R4: Once CYC is low, STB must also be low
// R10: Once CYC is low, STB must also be low
if(!i_wb_cyc)
assert(!i_wb_stb);
R10: 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 initiate a request
C1: 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: We eventually get an ACK during an active request
C2: 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.
// C3: 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 &&
C3: 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 &&
C4: 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);
// C5-C6: Read and write both occur (even if only once each)
C5: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && !i_wb_we);
C6: 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 &&
// C7: A transfer completes and the master drops CYC sometime after
C7: cover(f_past_valid && !i_rst && !i_wb_rst &&
$past(i_wb_cyc && i_wb_stb && o_wb_ack) && !i_wb_cyc);
end

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

@@ -1,7 +1,8 @@
`timescale 1ns/1ps
module formal_wb_slave_checker #(
parameter combinatorial_ack = 0
parameter combinatorial_ack = 0,
parameter expect_wait_state = 0
) (
input wire i_clk,
input wire i_rst,
@@ -24,38 +25,38 @@ module formal_wb_slave_checker #(
// A1: Reset forces cyc=0, stb=0
if (i_rst) begin
assume(!i_wb_cyc);
assume(!i_wb_stb);
A1: assume(!i_wb_cyc);
A2: assume(!i_wb_stb);
end
// A2: std->cyc, stb never high without cyc
// A3: std->cyc, stb never high without cyc
if(i_wb_stb)
assume(i_wb_cyc);
A3: assume(i_wb_cyc);
// A3: once a request starts, hold it stable until the slave responds
// A4-A9: once a request starts, hold it stable until the slave responds
if(f_past_valid && $past(i_wb_cyc && i_wb_stb && !o_wb_ack)) begin
assume(i_wb_cyc);
assume(i_wb_stb);
assume(i_wb_adr == $past(i_wb_adr));
assume(i_wb_dat == $past(i_wb_dat));
assume(i_wb_sel == $past(i_wb_sel));
assume(i_wb_we == $past(i_wb_we));
A4: assume(i_wb_cyc);
A5: assume(i_wb_stb);
A6: assume(i_wb_adr == $past(i_wb_adr));
A7: assume(i_wb_dat == $past(i_wb_dat));
A8: assume(i_wb_sel == $past(i_wb_sel));
A9: assume(i_wb_we == $past(i_wb_we));
end
// R1: ACK must correspond to either a same-cycle or previous-cycle request
if(o_wb_ack)
assert(
R1: assert(
(i_wb_cyc && i_wb_stb) ||
(f_past_valid && $past(i_wb_cyc && i_wb_stb))
);
// R2: !CYC->!ACK : no ghost acks
if(!i_wb_cyc)
assert(!o_wb_ack);
R2: assert(!o_wb_ack);
// R3: Reset must leave the slave initialized on the following cycle
if(f_past_valid && $past(i_rst || i_wb_rst))
assert(!o_wb_ack);
R3: assert(!o_wb_ack);
// R4: once STB has been dropped for a full cycle, ACK must be low
if(
@@ -63,34 +64,35 @@ module formal_wb_slave_checker #(
!$past(i_wb_stb) &&
!i_wb_stb
)
assert(!o_wb_ack);
R4: 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 occurs at all
C1: 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-C3: A request with write and with read occur
C2: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && i_wb_we);
C3: 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);
// C4: ACK happens during a request (basic progress)
C4: 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.
// C5-C7: Exercise the expected ACK timing style for this slave.
if (combinatorial_ack) begin
cover(f_past_valid && !i_rst && !i_wb_rst &&
C5: 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 &&
C6: 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));
// C7: Optional wait-state behavior for slaves that intentionally stall.
if (expect_wait_state)
C7: 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 &&
// C8: Master ends a cycle (CYC drops) after at least one request
C8: cover(f_past_valid && !i_rst && !i_wb_rst &&
$past(i_wb_cyc && i_wb_stb) && !i_wb_cyc);
end