Files
retroSoC/rtl/mini/dv/sva/axi4_protocol_sva.sv
T
maksyuki de32aa2979 feat: add AXI4 interconnect testbench and enhance existing tests
- Introduced a new testbench for the AXI4 interconnect () to validate fault classification for decode and access errors.
- Updated  and  to reflect changes in bus naming conventions.
- Enhanced  to include AXI4-Stream interface checks and validate stream data transfers.
- Modified  to integrate AXI4-Stream interfaces for improved DMA testing.
- Added new Python tests () to verify AXI4 to RIBP burst bridge functionality and interconnect fault classification.
- Updated existing tests to include AXI4 interfaces and ensure proper error handling and response validation.
- Adjusted memory map generation and test setups to accommodate new AXI4 interface requirements.
2026-08-12 12:30:12 +08:00

72 lines
2.8 KiB
Systemverilog

// Copyright (c) 2026 Yuchi Miao <miaoyuchi@ict.ac.cn>
// retroSoC is licensed under Mulan PSL v2.
// See LICENSE for the complete license text.
`ifndef SV_ASSRT_DISABLE
`ifndef SYNTHESIS
// The design uses rst_n_i asynchronously in state registers while SVA samples
// it synchronously in disable iff. This is intentional assertion semantics.
/* verilator lint_off SYNCASYNCNET */
module axi4_interconnect_sva #(
parameter int NUM_MASTERS = 3,
parameter int NUM_TARGETS = 9,
parameter int MASTER_WIDTH = $clog2(NUM_MASTERS),
parameter int TARGET_WIDTH = $clog2(NUM_TARGETS)
) (
input logic clk_i,
input logic rst_n_i,
input logic [NUM_MASTERS-1:0][ 1:0] master_state_i,
input logic [NUM_MASTERS-1:0][TARGET_WIDTH-1:0] master_target_i,
input logic [NUM_TARGETS-1:0] target_valid_i,
input logic [NUM_TARGETS-1:0] target_addr_sent_i,
input logic [NUM_TARGETS-1:0][MASTER_WIDTH-1:0] target_owner_i,
input logic user_bus_enable_i,
input logic user_awready_i,
input logic user_arready_i
);
localparam logic [1:0] MASTER_IDLE = 2'd0;
localparam logic [1:0] MASTER_ACTIVE = 2'd2;
for (genvar target = 0; target < NUM_TARGETS; target++) begin : GEN_TARGET_OWNERSHIP
assert property (@(posedge clk_i) disable iff (!rst_n_i)
target_addr_sent_i[target] |-> target_valid_i[target]);
assert property (@(posedge clk_i) disable iff (!rst_n_i)
target_valid_i[target] |->
master_state_i[target_owner_i[target]] == MASTER_ACTIVE &&
master_target_i[target_owner_i[target]] == TARGET_WIDTH'(target));
for (genvar other = target + 1; other < NUM_TARGETS; other++) begin : GEN_UNIQUE_OWNER
assert property (@(posedge clk_i) disable iff (!rst_n_i)
target_valid_i[target] && target_valid_i[other] |->
target_owner_i[target] != target_owner_i[other]);
end
end
assert property (@(posedge clk_i) disable iff (!rst_n_i)
!user_bus_enable_i && master_state_i[1] == MASTER_IDLE |->
!user_awready_i && !user_arready_i);
endmodule
bind axi4_interconnect axi4_interconnect_sva #(
.NUM_MASTERS(NUM_MASTERS),
.NUM_TARGETS(NUM_TARGETS)
) u_axi4_interconnect_sva (
.clk_i (clk_i),
.rst_n_i (rst_n_i),
.master_state_i (r_master_state),
.master_target_i (r_master_target),
.target_valid_i (r_target_valid),
.target_addr_sent_i(r_target_addr_sent),
.target_owner_i (r_target_owner),
.user_bus_enable_i (user_bus_enable_i),
.user_awready_i (m_awready[1]),
.user_arready_i (m_arready[1])
);
/* verilator lint_on SYNCASYNCNET */
`endif
`endif