mirror of
https://github.com/retroSoC/retroSoC.git
synced 2026-11-06 14:55:14 +00:00
feat: add I2C support to the SoC topology and formal verification
- Updated to include I2C1 in IRQ bindings. - Modified to increase IRQ group width and add I2C1 interrupt. - Enhanced to include I2C formal properties and adjust timeouts. - Added I2C-related source files to the formal verification flow. - Updated DMA wrapper in to handle I2C DMA signals. - Created a new testbench for I2C functionality verification. - Implemented I2C helper functions in for testing. - Added I2C tests in to validate controller behavior and recovery. - Updated existing tests to accommodate changes in DMA and IRQ handling.
This commit is contained in:
48 files changed
+3862
-1030
No files matched your search
+28
-4
@@ -4,6 +4,7 @@
|
||||
#include <retrosoc/core/status.h>
|
||||
#include <retrosoc/core/wait.h>
|
||||
#include <retrosoc/hal/gpio.h>
|
||||
#include <retrosoc/hal/i2c.h>
|
||||
#include <retrosoc/hal/lcd.h>
|
||||
#include <retrosoc/hal/spisd.h>
|
||||
#include <retrosoc/hal/timer.h>
|
||||
@@ -211,6 +212,30 @@ static int test_uart_helpers(void) {
|
||||
return 0;
|
||||
}
|
||||
|
||||
static int test_i2c_helpers(void) {
|
||||
rs_i2c_timing_t timing;
|
||||
|
||||
if ((rs_i2c_timing_calculate(72000000U, 400000U, &timing) != RS_OK) ||
|
||||
(timing.scl_low_cycles != 136U) || (timing.scl_high_cycles != 44U) ||
|
||||
(timing.start_hold_cycles != 44U) || (timing.start_setup_cycles != 44U) ||
|
||||
(timing.data_setup_cycles != 8U) || (timing.stop_setup_cycles != 44U) ||
|
||||
(timing.bus_free_cycles != 94U)) {
|
||||
return 1;
|
||||
}
|
||||
if ((rs_i2c_timing_calculate(72000000U, 1000000U, &timing) != RS_OK) ||
|
||||
(timing.scl_low_cycles != 53U) || (timing.scl_high_cycles != 19U) ||
|
||||
(timing.data_setup_cycles != 4U)) {
|
||||
return 2;
|
||||
}
|
||||
if ((rs_i2c_timing_calculate(0U, 400000U, &timing) != RS_EINVAL) ||
|
||||
(rs_i2c_timing_calculate(72000000U, 0U, &timing) != RS_EINVAL) ||
|
||||
(rs_i2c_timing_calculate(72000000U, 1000001U, &timing) != RS_EINVAL) ||
|
||||
(rs_i2c_timing_calculate(72000000U, 400000U, NULL) != RS_EINVAL)) {
|
||||
return 3;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
static int test_gpio_helpers(void) {
|
||||
rs_gpio_filter_timing_t timing;
|
||||
|
||||
@@ -271,10 +296,9 @@ static int test_video_parser(void) {
|
||||
|
||||
int main(void) {
|
||||
const int results[] = {
|
||||
test_string_helpers(), test_formatter(), test_compiler_helpers(),
|
||||
test_wait_helper(), test_ws2812_helpers(), test_timer_helpers(),
|
||||
test_uart_helpers(), test_gpio_helpers(), test_wav_parser(),
|
||||
test_video_parser(),
|
||||
test_string_helpers(), test_formatter(), test_compiler_helpers(), test_wait_helper(),
|
||||
test_ws2812_helpers(), test_timer_helpers(), test_uart_helpers(), test_i2c_helpers(),
|
||||
test_gpio_helpers(), test_wav_parser(), test_video_parser(),
|
||||
};
|
||||
|
||||
for (size_t index = 0U; index < (sizeof(results) / sizeof(results[0])); ++index) {
|
||||
|
||||
@@ -7,7 +7,7 @@ module dma_error_tb;
|
||||
|
||||
logic clk_i = 1'b0;
|
||||
logic rst_n_i = 1'b0;
|
||||
logic [ 2:0] mode_i = 3'd0;
|
||||
logic [ 3:0] mode_i = 4'd0;
|
||||
logic [31:0] srcaddr_i = 32'h3800_1000;
|
||||
logic srcincr_i = 1'b1;
|
||||
logic [31:0] dstaddr_i = 32'h4000_1000;
|
||||
@@ -145,6 +145,10 @@ module dma_error_tb;
|
||||
hw_trg.qspi_rx_proc = 1'b0;
|
||||
hw_trg.uart_tx_proc = 1'b0;
|
||||
hw_trg.uart_rx_proc = 1'b0;
|
||||
hw_trg.i2c0_tx_proc = 1'b0;
|
||||
hw_trg.i2c0_rx_proc = 1'b0;
|
||||
hw_trg.i2c1_tx_proc = 1'b0;
|
||||
hw_trg.i2c1_rx_proc = 1'b0;
|
||||
repeat (2) @(posedge clk_i);
|
||||
rst_n_i = 1'b1;
|
||||
|
||||
|
||||
@@ -0,0 +1,314 @@
|
||||
`timescale 1ns / 1ps
|
||||
|
||||
`include "ribp_i2c_define.svh"
|
||||
|
||||
module i2c_tb;
|
||||
logic clk_i = 1'b0;
|
||||
logic rst_n_i = 1'b0;
|
||||
logic dma_tx_stall;
|
||||
logic dma_rx_stall;
|
||||
logic slave_scl_low = 1'b0;
|
||||
logic slave_sda_low = 1'b0;
|
||||
logic scl_line;
|
||||
logic sda_line;
|
||||
ribp_if ribp ();
|
||||
i2c_if i2c ();
|
||||
|
||||
always #5 clk_i = ~clk_i;
|
||||
|
||||
assign scl_line = (i2c.scl_oe_o || slave_scl_low) ? 1'b0 : 1'b1;
|
||||
assign sda_line = (i2c.sda_oe_o || slave_sda_low) ? 1'b0 : 1'b1;
|
||||
assign i2c.scl_i = scl_line;
|
||||
assign i2c.sda_i = sda_line;
|
||||
|
||||
ribp_i2c u_dut (
|
||||
.clk_i (clk_i),
|
||||
.rst_n_i (rst_n_i),
|
||||
.dma_tx_stall_o(dma_tx_stall),
|
||||
.dma_rx_stall_o(dma_rx_stall),
|
||||
.ribp (ribp),
|
||||
.i2c (i2c)
|
||||
);
|
||||
|
||||
task automatic ribp_write(input logic [31:0] address, input logic [31:0] data,
|
||||
input logic expected_error);
|
||||
begin
|
||||
@(negedge clk_i);
|
||||
ribp.addr = address;
|
||||
ribp.wdata = data;
|
||||
ribp.wstrb = 4'hF;
|
||||
ribp.valid = 1'b1;
|
||||
while (!ribp.ready) begin
|
||||
@(posedge clk_i);
|
||||
#1;
|
||||
end
|
||||
if (ribp.resp_err !== expected_error) begin
|
||||
$fatal(1, "I2C write %h error=%b expected=%b", address, ribp.resp_err, expected_error);
|
||||
end
|
||||
@(negedge clk_i);
|
||||
ribp.valid = 1'b0;
|
||||
ribp.wstrb = '0;
|
||||
end
|
||||
endtask
|
||||
|
||||
task automatic ribp_read(input logic [31:0] address, input logic expected_error,
|
||||
output logic [31:0] data);
|
||||
begin
|
||||
@(negedge clk_i);
|
||||
ribp.addr = address;
|
||||
ribp.wdata = '0;
|
||||
ribp.wstrb = '0;
|
||||
ribp.valid = 1'b1;
|
||||
while (!ribp.ready) begin
|
||||
@(posedge clk_i);
|
||||
#1;
|
||||
end
|
||||
if (ribp.resp_err !== expected_error) begin
|
||||
$fatal(1, "I2C read %h error=%b expected=%b", address, ribp.resp_err, expected_error);
|
||||
end
|
||||
data = ribp.rdata;
|
||||
@(negedge clk_i);
|
||||
ribp.valid = 1'b0;
|
||||
end
|
||||
endtask
|
||||
|
||||
task automatic wait_start;
|
||||
begin
|
||||
@(negedge sda_line);
|
||||
while (!scl_line) begin
|
||||
@(negedge sda_line);
|
||||
end
|
||||
end
|
||||
endtask
|
||||
|
||||
task automatic receive_byte(output logic [7:0] data, input integer stretch_cycles);
|
||||
integer bit_index;
|
||||
begin
|
||||
for (bit_index = 7; bit_index >= 0; bit_index = bit_index - 1) begin
|
||||
@(posedge scl_line);
|
||||
data[bit_index] = sda_line;
|
||||
end
|
||||
@(negedge scl_line);
|
||||
slave_sda_low = 1'b1;
|
||||
if (stretch_cycles != 0) begin
|
||||
slave_scl_low = 1'b1;
|
||||
repeat (stretch_cycles) @(posedge clk_i);
|
||||
slave_scl_low = 1'b0;
|
||||
end
|
||||
@(posedge scl_line);
|
||||
@(negedge scl_line);
|
||||
slave_sda_low = 1'b0;
|
||||
end
|
||||
endtask
|
||||
|
||||
task automatic send_byte(input logic [7:0] data, output logic nack);
|
||||
integer bit_index;
|
||||
begin
|
||||
for (bit_index = 7; bit_index >= 0; bit_index = bit_index - 1) begin
|
||||
slave_sda_low = !data[bit_index];
|
||||
@(posedge scl_line);
|
||||
@(negedge scl_line);
|
||||
end
|
||||
slave_sda_low = 1'b0;
|
||||
@(posedge scl_line);
|
||||
nack = sda_line;
|
||||
@(negedge scl_line);
|
||||
end
|
||||
endtask
|
||||
|
||||
task automatic wait_done;
|
||||
logic [31:0] value;
|
||||
logic [31:0] error_value;
|
||||
logic [31:0] status_value;
|
||||
integer attempts;
|
||||
begin
|
||||
value = '0;
|
||||
for (attempts = 0; attempts < 4000; attempts = attempts + 1) begin
|
||||
ribp_read(`RIBP_I2C_INTR_STATE, 1'b0, value);
|
||||
if (value[`I2C_INTR_DONE]) begin
|
||||
attempts = 4000;
|
||||
end
|
||||
end
|
||||
if (!value[`I2C_INTR_DONE]) begin
|
||||
ribp_read(`RIBP_I2C_ERROR_STATUS, 1'b0, error_value);
|
||||
ribp_read(`RIBP_I2C_STATUS, 1'b0, status_value);
|
||||
$fatal(1, "I2C transaction did not complete: error=%h status=%h fsm=%0d", error_value,
|
||||
status_value, u_dut.u_i2c_core.s_fsm_q);
|
||||
end
|
||||
ribp_write(`RIBP_I2C_INTR_STATE, 32'hFF, 1'b0);
|
||||
end
|
||||
endtask
|
||||
|
||||
task automatic clear_state;
|
||||
begin
|
||||
ribp_write(`RIBP_I2C_ERROR_STATUS, 32'h7FF, 1'b0);
|
||||
ribp_write(`RIBP_I2C_INTR_STATE, 32'hFF, 1'b0);
|
||||
ribp_write(`RIBP_I2C_COMMAND, 32'hC, 1'b0);
|
||||
end
|
||||
endtask
|
||||
|
||||
initial begin
|
||||
logic [31:0] value;
|
||||
logic [ 7:0] byte_value;
|
||||
logic nack;
|
||||
integer pulse_count;
|
||||
|
||||
ribp.valid = 1'b0;
|
||||
ribp.addr = '0;
|
||||
ribp.wdata = '0;
|
||||
ribp.wstrb = '0;
|
||||
repeat (4) @(posedge clk_i);
|
||||
rst_n_i = 1'b1;
|
||||
repeat (4) @(posedge clk_i);
|
||||
|
||||
ribp_read(`RIBP_I2C_IP_VERSION, 1'b0, value);
|
||||
if (value != 32'h0002_0000) $fatal(1, "I2C version mismatch");
|
||||
ribp_read(`RIBP_I2C_CAPABILITY, 1'b0, value);
|
||||
if (value != 32'h007F_1010) $fatal(1, "I2C capability mismatch: %h", value);
|
||||
ribp_read(32'h2, 1'b1, value);
|
||||
|
||||
ribp_write(`RIBP_I2C_SCL_TIMING, 32'h0008_0008, 1'b0);
|
||||
ribp_write(`RIBP_I2C_START_TIMING, 32'h0002_0002, 1'b0);
|
||||
ribp_write(`RIBP_I2C_DATA_TIMING, 32'h0001_0000, 1'b0);
|
||||
ribp_write(`RIBP_I2C_STOP_TIMING, 32'h0002_0002, 1'b0);
|
||||
ribp_write(`RIBP_I2C_FILTER, 0, 1'b0);
|
||||
ribp_write(`RIBP_I2C_STRETCH_TIMEOUT, 200, 1'b0);
|
||||
ribp_write(`RIBP_I2C_BUS_IDLE_TIMEOUT, 200, 1'b0);
|
||||
ribp_write(`RIBP_I2C_COMMAND_TIMEOUT, 2000, 1'b0);
|
||||
ribp_write(`RIBP_I2C_TARGET_ADDR, 7'h50, 1'b0);
|
||||
ribp_write(`RIBP_I2C_CTRL, 1, 1'b0);
|
||||
|
||||
fork
|
||||
begin
|
||||
wait_start();
|
||||
receive_byte(byte_value, 0);
|
||||
if (byte_value != 8'hA0) $fatal(1, "write address mismatch: %h", byte_value);
|
||||
receive_byte(byte_value, 0);
|
||||
if (byte_value != 8'hA5) $fatal(1, "write data mismatch: %h", byte_value);
|
||||
end
|
||||
begin
|
||||
ribp_write(`RIBP_I2C_DATA_CMD, 32'h4A5, 1'b0);
|
||||
wait_done();
|
||||
end
|
||||
join
|
||||
|
||||
clear_state();
|
||||
ribp_write(`RIBP_I2C_TARGET_ADDR, 32'h0000_06AA, 1'b0);
|
||||
fork
|
||||
begin
|
||||
wait_start();
|
||||
receive_byte(byte_value, 0);
|
||||
if (byte_value != 8'hF4) $fatal(1, "10-bit write header mismatch: %h", byte_value);
|
||||
receive_byte(byte_value, 0);
|
||||
if (byte_value != 8'hAA) $fatal(1, "10-bit low address mismatch: %h", byte_value);
|
||||
wait_start();
|
||||
receive_byte(byte_value, 0);
|
||||
if (byte_value != 8'hF5) $fatal(1, "10-bit read header mismatch: %h", byte_value);
|
||||
send_byte(8'hC3, nack);
|
||||
if (!nack) $fatal(1, "final 10-bit read byte was not NACKed");
|
||||
end
|
||||
begin
|
||||
ribp_write(`RIBP_I2C_DATA_CMD, 32'hD00, 1'b0);
|
||||
wait_done();
|
||||
ribp_read(`RIBP_I2C_RXDATA, 1'b0, value);
|
||||
if (value[7:0] != 8'hC3) $fatal(1, "10-bit read data mismatch: %h", value);
|
||||
end
|
||||
join
|
||||
|
||||
clear_state();
|
||||
ribp_write(`RIBP_I2C_TARGET_ADDR, 7'h50, 1'b0);
|
||||
fork
|
||||
begin
|
||||
wait_start();
|
||||
receive_byte(byte_value, 0);
|
||||
if (byte_value != 8'hA0) $fatal(1, "combined write address mismatch");
|
||||
receive_byte(byte_value, 0);
|
||||
if (byte_value != 8'h12) $fatal(1, "combined register byte mismatch");
|
||||
wait_start();
|
||||
receive_byte(byte_value, 0);
|
||||
if (byte_value != 8'hA1) $fatal(1, "combined read address mismatch");
|
||||
send_byte(8'h5A, nack);
|
||||
if (!nack) $fatal(1, "final read byte was not NACKed");
|
||||
end
|
||||
begin
|
||||
ribp_write(`RIBP_I2C_DATA_CMD, 32'h012, 1'b0);
|
||||
ribp_write(`RIBP_I2C_DATA_CMD, 32'hF00, 1'b0);
|
||||
wait_done();
|
||||
ribp_read(`RIBP_I2C_RXDATA, 1'b0, value);
|
||||
if (value[7:0] != 8'h5A) $fatal(1, "read data mismatch: %h", value);
|
||||
end
|
||||
join
|
||||
|
||||
clear_state();
|
||||
fork
|
||||
begin
|
||||
wait_start();
|
||||
receive_byte(byte_value, 12);
|
||||
receive_byte(byte_value, 0);
|
||||
end
|
||||
begin
|
||||
ribp_write(`RIBP_I2C_DATA_CMD, 32'h45C, 1'b0);
|
||||
wait_done();
|
||||
end
|
||||
join
|
||||
|
||||
clear_state();
|
||||
ribp_write(`RIBP_I2C_TARGET_ADDR, 7'h51, 1'b0);
|
||||
ribp_write(`RIBP_I2C_DATA_CMD, 32'h455, 1'b0);
|
||||
repeat (300) @(posedge clk_i);
|
||||
ribp_read(`RIBP_I2C_ERROR_STATUS, 1'b0, value);
|
||||
if (!value[`I2C_ERROR_ADDR_NACK]) $fatal(1, "address NACK was not reported");
|
||||
|
||||
clear_state();
|
||||
ribp_write(`RIBP_I2C_TARGET_ADDR, 7'h7F, 1'b0);
|
||||
fork
|
||||
begin
|
||||
wait_start();
|
||||
@(negedge scl_line);
|
||||
#1 slave_sda_low = 1'b1;
|
||||
@(posedge scl_line);
|
||||
repeat (4) @(posedge clk_i);
|
||||
slave_sda_low = 1'b0;
|
||||
end
|
||||
begin
|
||||
ribp_write(`RIBP_I2C_DATA_CMD, 32'h400, 1'b0);
|
||||
end
|
||||
join
|
||||
repeat (20) @(posedge clk_i);
|
||||
ribp_read(`RIBP_I2C_ERROR_STATUS, 1'b0, value);
|
||||
if (!value[`I2C_ERROR_ARB_LOST]) $fatal(1, "arbitration loss was not reported");
|
||||
|
||||
clear_state();
|
||||
slave_sda_low = 1'b1;
|
||||
fork
|
||||
begin
|
||||
pulse_count = 0;
|
||||
while (pulse_count < 9) begin
|
||||
@(posedge scl_line);
|
||||
pulse_count = pulse_count + 1;
|
||||
end
|
||||
slave_sda_low = 1'b0;
|
||||
end
|
||||
begin
|
||||
ribp_write(`RIBP_I2C_COMMAND, 32'h2, 1'b0);
|
||||
end
|
||||
join
|
||||
repeat (80) @(posedge clk_i);
|
||||
ribp_read(`RIBP_I2C_INTR_STATE, 1'b0, value);
|
||||
if (!value[`I2C_INTR_RECOVERY_DONE] || (pulse_count != 9)) begin
|
||||
$fatal(1, "bus recovery failed: intr=%h pulses=%0d", value, pulse_count);
|
||||
end
|
||||
|
||||
if (i2c.scl_o !== 1'b0 || i2c.sda_o !== 1'b0) begin
|
||||
$fatal(1, "I2C pads are not open-drain constants");
|
||||
end
|
||||
$display("I2C V2 transfer, error, stretch, arbitration, and recovery test passed");
|
||||
$finish;
|
||||
end
|
||||
|
||||
initial begin
|
||||
repeat (50000) @(posedge clk_i);
|
||||
$fatal(1, "I2C test timeout");
|
||||
end
|
||||
|
||||
endmodule
|
||||
@@ -127,7 +127,7 @@ module ws2812_dma_tb;
|
||||
dma_core u_dma_core (
|
||||
.clk_i (clk_i),
|
||||
.rst_n_i (rst_n_i),
|
||||
.mode_i (3'd0),
|
||||
.mode_i (4'd0),
|
||||
.srcaddr_i (SOURCE_BASE + 32'd4),
|
||||
.srcincr_i (1'b1),
|
||||
.dstaddr_i (WS2812_TXDATA),
|
||||
@@ -219,6 +219,10 @@ module ws2812_dma_tb;
|
||||
hw_trg.qspi_rx_proc = 1'b0;
|
||||
hw_trg.uart_tx_proc = 1'b0;
|
||||
hw_trg.uart_rx_proc = 1'b0;
|
||||
hw_trg.i2c0_tx_proc = 1'b0;
|
||||
hw_trg.i2c0_rx_proc = 1'b0;
|
||||
hw_trg.i2c1_tx_proc = 1'b0;
|
||||
hw_trg.i2c1_rx_proc = 1'b0;
|
||||
|
||||
repeat (3) @(posedge clk_i);
|
||||
rst_n_i = 1'b1;
|
||||
|
||||
@@ -0,0 +1,66 @@
|
||||
"""Directed I2C V2 controller, FIFO, error, timeout, and recovery tests."""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import shutil
|
||||
import subprocess
|
||||
import sys
|
||||
from pathlib import Path
|
||||
|
||||
|
||||
ROOT = Path(__file__).resolve().parents[1]
|
||||
|
||||
|
||||
def test_i2c_v2_controller_and_recovery_contract(tmp_path: Path) -> None:
|
||||
iverilog = shutil.which("iverilog")
|
||||
vvp = shutil.which("vvp")
|
||||
if iverilog is None or vvp is None:
|
||||
return
|
||||
|
||||
common = ROOT / "rtl/managed/clusterip/common/rtl"
|
||||
serial = ROOT / "rtl/ip/ribp/serial"
|
||||
cluster_i2c = ROOT / "rtl/managed/clusterip/i2c/rtl"
|
||||
source_list = tmp_path / "i2c.fl"
|
||||
source_list.write_text(
|
||||
"\n".join(
|
||||
[
|
||||
"+define+SV_ASSRT_DISABLE",
|
||||
f"+incdir+{common}",
|
||||
f"+incdir+{common / 'interface'}",
|
||||
f"+incdir+{common / 'utils'}",
|
||||
f"+incdir+{common / 'cdc'}",
|
||||
f"+incdir+{serial}",
|
||||
str(common / "interface/ribp_if.sv"),
|
||||
str(common / "utils/register.sv"),
|
||||
str(common / "utils/fifo.sv"),
|
||||
str(common / "cdc/cdc_sync.sv"),
|
||||
str(cluster_i2c / "i2c_if.sv"),
|
||||
str(serial / "i2c_filter.sv"),
|
||||
str(serial / "i2c_core.sv"),
|
||||
str(serial / "i2c_reg.sv"),
|
||||
str(serial / "ribp_i2c.sv"),
|
||||
str(ROOT / "tests/rtl/i2c_tb.sv"),
|
||||
"",
|
||||
]
|
||||
),
|
||||
encoding="utf-8",
|
||||
)
|
||||
converted = tmp_path / "i2c_tb.v"
|
||||
subprocess.run(
|
||||
[
|
||||
sys.executable,
|
||||
str(ROOT / "rtl/mini/script/convt_sv2v.py"),
|
||||
"-f",
|
||||
str(source_list),
|
||||
"--output",
|
||||
str(converted),
|
||||
],
|
||||
check=True,
|
||||
)
|
||||
simulation = tmp_path / "i2c_tb"
|
||||
subprocess.run(
|
||||
[iverilog, "-g2012", "-s", "i2c_tb", "-o", str(simulation), str(converted)],
|
||||
check=True,
|
||||
)
|
||||
result = subprocess.run([vvp, str(simulation)], text=True, capture_output=True, check=True)
|
||||
assert "I2C V2 transfer, error, stretch, arbitration, and recovery test passed" in result.stdout
|
||||
@@ -205,6 +205,7 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non
|
||||
pll_rcu_filelist = tmp_path / "pll_rcu.fl"
|
||||
gpio_filelist = tmp_path / "gpio.fl"
|
||||
ws2812_filelist = tmp_path / "ws2812.fl"
|
||||
i2c_filelist = tmp_path / "i2c.fl"
|
||||
clint_filelist = tmp_path / "clint.fl"
|
||||
assert generate_formal_filelist("bus", bus_filelist, memory_map, topology, user_extensions)
|
||||
assert generate_formal_filelist(
|
||||
@@ -225,6 +226,7 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non
|
||||
assert generate_formal_filelist(
|
||||
"ws2812", ws2812_filelist, memory_map, topology, user_extensions
|
||||
)
|
||||
assert generate_formal_filelist("i2c", i2c_filelist, memory_map, topology, user_extensions)
|
||||
assert generate_formal_filelist(
|
||||
"clint", clint_filelist, memory_map, topology, user_extensions
|
||||
)
|
||||
@@ -236,6 +238,7 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non
|
||||
pll_rcu = parse_filelists([pll_rcu_filelist], require_files=False)
|
||||
gpio = parse_filelists([gpio_filelist], require_files=False)
|
||||
ws2812 = parse_filelists([ws2812_filelist], require_files=False)
|
||||
i2c = parse_filelists([i2c_filelist], require_files=False)
|
||||
clint = parse_filelists([clint_filelist], require_files=False)
|
||||
assert "+define+SV_ASSRT_DISABLE" in bus.defines
|
||||
assert ROOT / "rtl/mini/top/bus.sv" in bus.files
|
||||
@@ -262,6 +265,9 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non
|
||||
assert ROOT / "rtl/ip/ribp/serial/ribp_ws2812.sv" in ws2812.files
|
||||
assert ROOT / "rtl/managed/clusterip/common/rtl/utils/fifo.sv" in ws2812.files
|
||||
assert ROOT / "rtl/mini/formal/ws2812_formal.sv" in ws2812.files
|
||||
assert ROOT / "rtl/ip/ribp/serial/ribp_i2c.sv" in i2c.files
|
||||
assert ROOT / "rtl/ip/ribp/serial/i2c_filter.sv" in i2c.files
|
||||
assert ROOT / "rtl/mini/formal/i2c_formal.sv" in i2c.files
|
||||
assert ROOT / "rtl/ip/ribp/peripheral/ribp_clint.sv" in clint.files
|
||||
assert ROOT / "rtl/mini/formal/clint_formal.sv" in clint.files
|
||||
|
||||
@@ -284,6 +290,9 @@ def test_sby_config_uses_prove_and_cover_with_bitwuzla(tmp_path: Path) -> None:
|
||||
properties = tmp_path / "properties.v"
|
||||
prove_config = render_sby_config("bus_formal", design, properties, "bitwuzla", "prove", 20)
|
||||
cover_config = render_sby_config("bus_formal", design, properties, "bitwuzla", "cover", 20)
|
||||
compact_cover_config = render_sby_config(
|
||||
"i2c_formal", design, properties, "bitwuzla", "cover", 80, vcd=False
|
||||
)
|
||||
|
||||
assert "mode prove" in prove_config
|
||||
assert "mode cover" in cover_config
|
||||
@@ -291,6 +300,8 @@ def test_sby_config_uses_prove_and_cover_with_bitwuzla(tmp_path: Path) -> None:
|
||||
assert "smtbmc --presat --nounroll bitwuzla" in prove_config
|
||||
assert f"design.v {design.resolve()}" in prove_config
|
||||
assert f"properties.v {properties.resolve()}" in prove_config
|
||||
assert "vcd off" not in cover_config
|
||||
assert "vcd off" in compact_cover_config
|
||||
|
||||
|
||||
def test_bitwuzla_wrapper_translates_yosys_legacy_arguments() -> None:
|
||||
|
||||
@@ -97,12 +97,13 @@ def test_topology_generates_complete_rib_apb_and_gpio_bindings(tmp_path: Path) -
|
||||
assert ".apb_rib(u_apb_rib_if)" in bus_fabric
|
||||
assert ".rib(u_rib_if)" in bus_fabric
|
||||
assert "`define SOC_IRQ_VECTOR_WIDTH 32" in irq_config
|
||||
assert "`define SOC_USER_IRQ_MASK 32'h0007FFFC" in irq_config
|
||||
assert "`define SOC_IRQ_RIBP_WIDTH 12" in irq_config
|
||||
assert "`define SOC_USER_IRQ_MASK 32'h000FFFFC" in irq_config
|
||||
assert "`define SOC_IRQ_RIBP_WIDTH 13" in irq_config
|
||||
assert "`define SOC_IRQ_APB_WIDTH 7" in irq_config
|
||||
assert "assign irq_o[0] = u_clint_if.software_irq_o[0];" in rib_irq
|
||||
assert "assign irq_o[10] = ws2812.irq_o;" in rib_irq
|
||||
assert "assign irq_o[11] = gpio.irq_o;" in rib_irq
|
||||
assert "assign irq_o[12] = i2c1.irq_o;" in rib_irq
|
||||
assert "assign irq_o[5] = u_tmr_if.irq_o;" in apb_irq
|
||||
assert "s_irq[16] = s_apb_irq[6];" in irq_wiring
|
||||
assert "irq_i[31] == 1'b0" in irq_sva
|
||||
@@ -123,7 +124,7 @@ def test_topology_preserves_default_irq_compatibility_mapping() -> None:
|
||||
)
|
||||
for interrupt in document["interrupts"]
|
||||
]
|
||||
assert mappings[:19] == [
|
||||
assert mappings[:20] == [
|
||||
("clint_software", "ribp", 0, 0, "u_clint_if.software_irq_o[0]"),
|
||||
("clint_timer", "ribp", 1, 1, "u_clint_if.timer_irq_o[0]"),
|
||||
("uart0", "ribp", 2, 2, "uart.irq_o"),
|
||||
@@ -143,8 +144,9 @@ def test_topology_preserves_default_irq_compatibility_mapping() -> None:
|
||||
("reserved", "apb", 6, 16, "1'b0"),
|
||||
("ws2812", "ribp", 10, 17, "ws2812.irq_o"),
|
||||
("gpio", "ribp", 11, 18, "gpio.irq_o"),
|
||||
("i2c1", "ribp", 12, 19, "i2c1.irq_o"),
|
||||
]
|
||||
assert all(mapping[3] >= 19 for mapping in mappings[19:])
|
||||
assert all(mapping[3] >= 20 for mapping in mappings[20:])
|
||||
|
||||
|
||||
def test_topology_always_adds_the_user_apb_target(tmp_path: Path) -> None:
|
||||
|
||||
Reference in new issue
Block a user