admin/retroSoC
1
0 Fork 0
mirror of https://github.com/retroSoC/retroSoC.git synced 2026-11-04 22:32:36 +00:00
Code Issues Packages Projects Releases Wiki Activity

fix(tiny): preserve AXI transactions across target reset

Browse Source 
Drain remaining write beats before returning B, retain captured R/B responses, and append missing read error beats through the response spills. Preserve first-error attribution and prevent replay after target reset release.

Cover 28 reset scenarios in both simulators, including production DMA drain and APB bridge cases. Extend reset formal checks and publication contract mutation tests.

Validation: 101 focused tests passed; full Pytest reported 1685 passed and one optional pypdf skip. TINY ICS55 and IHP130 PR regressions passed. Timing remains observational and unclosed; no performance or physical qualification is claimed.
This commit is contained in:
maksyuki committed 2026-10-12 07:15:32 +08:00
1 parent 4e6ab1a6fb
commit edb6e93eee
6 files changed
+545 -239
Download Patch File Download Diff File Expand all files Collapse all files

No files matched your search

publications/datasheets/tiny/source-contract.json
+6 -2
View File
@@ -187,9 +187,13 @@
"file": "rtl/tiny/top/tiny_axi4_target.sv",
"text": [
"assign s_accept = (s_req_q.state == Idle) && enable_i && s_valid;",
" assign s_terminal = (s_req_q.state == Response) &&\n (s_req_q.write ? (s_b_valid && s_bready[s_req_q.owner]) :\n (s_r_valid && s_rready[s_req_q.owner] && s_r_data[1]));",
"assign s_terminal = s_resp_active && (s_req_q.write ? (s_b_valid && s_bready[s_req_q.owner]) : (s_r_valid && s_rready[s_req_q.owner] && s_r_data[1]));",
"assign fault_valid_o = s_terminal && s_req_q.error_seen;",
"if (!s_req_q.error_seen && (target.rresp != 2'b00)) begin s_req_d.error_seen = 1'b1; s_req_d.error_addr = s_req_q.read_addr; s_req_d.error_resp = target.rresp; end",
"if (!s_req_q.error_seen && (s_rin_data[3:2] != 2'b00)) begin s_req_d.error_seen = 1'b1; s_req_d.error_addr = s_req_q.read_addr; s_req_d.error_resp = s_rin_data[3:2]; end",
"assign s_abort_write_valid = (s_req_q.state == AbortResponse) && s_req_q.write && s_req_q.write_done && !s_req_q.b_captured;",
"assign s_abort_read_valid = (s_req_q.state == AbortResponse) && !s_req_q.write && (s_req_q.read_count <= {1'b0, s_saved_addr.len});",
".flush_i(1'b0)",
"AbortWrite: begin",
"if (s_terminal) s_req_d.state = Idle;"
]
}
rtl/tiny/top/tiny_axi4_target.sv
+80 -60
View File
@@ -18,10 +18,11 @@ module tiny_axi4_target (
output logic fault_instruction_o,
output logic [ 1:0] fault_resp_o
);
typedef enum logic [1:0] {
typedef enum logic [2:0] {
Idle,
Address,
Response,
AbortWrite,
AbortResponse
} state_e;
typedef struct packed {
@@ -44,6 +45,8 @@ module tiny_axi4_target (
addr_t addr;
logic [7:0] write_beat;
logic write_done;
logic [8:0] read_count;
logic b_captured;
logic [31:0] read_addr, error_addr;
logic [1:0] error_resp;
logic error_seen;
@@ -64,6 +67,9 @@ module tiny_axi4_target (
logic [ 3:0] s_b_data;
logic s_read_capture, s_write_capture;
logic s_abort_read_valid, s_abort_write_valid;
logic s_resp_active, s_rin_valid, s_bin_valid;
logic [36:0] s_rin_data;
logic [ 3:0] s_bin_data;
assign s_saved_addr = s_req_q.addr;
assign s_req_addr = s_saved_addr.addr;
@@ -74,22 +80,34 @@ module tiny_axi4_target (
assign s_selected_addr = s_selected_write ? s_write_addr[s_selected] : s_read_addr[s_selected];
assign s_accept = (s_req_q.state == Idle) && enable_i && s_valid;
assign idle_o = (s_req_q.state == Idle) && !s_r_valid && !s_b_valid;
assign s_abort_read_valid = (s_req_q.state == AbortResponse) && !s_req_q.write;
assign s_abort_write_valid = (s_req_q.state == AbortResponse) && s_req_q.write;
assign s_terminal =
(s_req_q.state == Response) ?
(s_req_q.write ? (s_b_valid && s_bready[s_req_q.owner]) :
(s_r_valid && s_rready[s_req_q.owner] && s_r_data[1])) :
(s_req_q.state == AbortResponse) &&
(s_req_q.write ? s_bready[s_req_q.owner] : s_rready[s_req_q.owner]);
assign fault_valid_o = s_terminal && (s_req_q.error_seen || s_req_q.state == AbortResponse);
// Target reset cancels downstream work, never an already captured upstream
// response. Append missing error beats through the same spill registers.
assign s_resp_active = (s_req_q.state == Response) || (s_req_q.state == AbortResponse);
assign s_abort_read_valid = (s_req_q.state == AbortResponse) && !s_req_q.write &&
(s_req_q.read_count <= {1'b0, s_saved_addr.len});
assign s_abort_write_valid = (s_req_q.state == AbortResponse) && s_req_q.write &&
s_req_q.write_done && !s_req_q.b_captured;
assign s_terminal = s_resp_active &&
(s_req_q.write ? (s_b_valid && s_bready[s_req_q.owner]) :
(s_r_valid && s_rready[s_req_q.owner] && s_r_data[1]));
assign fault_valid_o = s_terminal && s_req_q.error_seen;
assign fault_addr_o = s_req_q.error_addr;
assign fault_master_o = s_req_q.owner;
assign fault_write_o = s_req_q.write;
assign fault_instruction_o = !s_req_q.write && s_saved_addr.prot[2];
assign fault_resp_o = s_req_q.error_resp;
assign s_read_capture = target.rvalid && target.rready;
assign s_write_capture = target.bvalid && target.bready;
assign s_rin_valid = ((s_req_q.state == Response) && enable_i &&
!s_req_q.write && target.rvalid) || s_abort_read_valid;
assign s_rin_data = s_abort_read_valid ?
{s_req_id, 32'd0, 2'b11,
(s_req_q.read_count == {1'b0, s_saved_addr.len}), 1'b0} :
{target.rid, target.rdata, target.rresp, target.rlast, target.ruser};
assign s_bin_valid = ((s_req_q.state == Response) && enable_i &&
s_req_q.write && target.bvalid) || s_abort_write_valid;
assign s_bin_data = s_abort_write_valid ? {s_req_id, 2'b11, 1'b0} :
{target.bid, target.bresp, target.buser};
assign s_read_capture = s_rin_valid && s_r_ready;
assign s_write_capture = s_bin_valid && s_b_ready;
round_robin_arbiter #(
.CLIENTS(3)
@@ -154,22 +172,17 @@ module tiny_axi4_target (
assign s_bready[owner] = masters[owner].bready;
assign masters[owner].arready = s_accept && s_grant[owner] && !s_selected_write;
assign masters[owner].awready = s_accept && s_grant[owner] && s_selected_write;
assign masters[owner].wready = (s_req_q.state == Response) && enable_i && s_req_q.write &&
!s_req_q.write_done && (s_req_q.owner == 2'(owner)) && target.wready;
assign masters[owner].rvalid = ((s_req_q.state == Response) && enable_i && !s_req_q.write &&
(s_req_q.owner == 2'(owner)) && s_r_valid) ||
(s_abort_read_valid && (s_req_q.owner == 2'(owner)));
assign masters[owner].rid = s_abort_read_valid ? s_req_id : s_r_data[36];
assign masters[owner].rdata = s_abort_read_valid ? 32'd0 : s_r_data[35:4];
assign masters[owner].rresp = s_abort_read_valid ? 2'b11 : s_r_data[3:2];
assign masters[owner].rlast = s_abort_read_valid ? 1'b1 : s_r_data[1];
assign masters[owner].ruser = s_abort_read_valid ? 1'b0 : s_r_data[0];
assign masters[owner].bvalid = ((s_req_q.state == Response) && enable_i && s_req_q.write &&
(s_req_q.owner == 2'(owner)) && s_b_valid) ||
(s_abort_write_valid && (s_req_q.owner == 2'(owner)));
assign masters[owner].bid = s_abort_write_valid ? s_req_id : s_b_data[3];
assign masters[owner].bresp = s_abort_write_valid ? 2'b11 : s_b_data[2:1];
assign masters[owner].buser = s_abort_write_valid ? 1'b0 : s_b_data[0];
assign masters[owner].wready = ((s_req_q.state == Response) && enable_i && s_req_q.write &&
!s_req_q.write_done && (s_req_q.owner == 2'(owner)) && target.wready) ||
((s_req_q.state == AbortWrite) && !s_req_q.write_done &&
(s_req_q.owner == 2'(owner)));
assign masters[owner].rvalid = s_resp_active && !s_req_q.write &&
(s_req_q.owner == 2'(owner)) && s_r_valid;
assign {masters[owner].rid, masters[owner].rdata, masters[owner].rresp,
masters[owner].rlast, masters[owner].ruser} = s_r_data;
assign masters[owner].bvalid = s_resp_active && s_req_q.write &&
(s_req_q.owner == 2'(owner)) && s_b_valid;
assign {masters[owner].bid, masters[owner].bresp, masters[owner].buser} = s_b_data;
end
assign target.awaddr = s_saved_addr.addr;
@@ -209,12 +222,12 @@ module tiny_axi4_target (
) u_read_response (
.clk_i (clk_i),
.rst_n_i(rst_n_i),
.flush_i(!enable_i),
.valid_i((s_req_q.state == Response) && !s_req_q.write && target.rvalid),
.flush_i(1'b0),
.valid_i(s_rin_valid),
.ready_o(s_r_ready),
.data_i ({target.rid, target.rdata, target.rresp, target.rlast, target.ruser}),
.data_i (s_rin_data),
.valid_o(s_r_valid),
.ready_i((s_req_q.state == Response) && !s_req_q.write && s_rready[s_req_q.owner]),
.ready_i(s_resp_active && !s_req_q.write && s_rready[s_req_q.owner]),
.data_o (s_r_data)
);
spill_register #(
@@ -222,12 +235,12 @@ module tiny_axi4_target (
) u_write_response (
.clk_i (clk_i),
.rst_n_i(rst_n_i),
.flush_i(!enable_i),
.valid_i((s_req_q.state == Response) && s_req_q.write && target.bvalid),
.flush_i(1'b0),
.valid_i(s_bin_valid),
.ready_o(s_b_ready),
.data_i ({target.bid, target.bresp, target.buser}),
.data_i (s_bin_data),
.valid_o(s_b_valid),
.ready_i((s_req_q.state == Response) && s_req_q.write && s_bready[s_req_q.owner]),
.ready_i(s_resp_active && s_req_q.write && s_bready[s_req_q.owner]),
.data_o (s_b_data)
);
always_comb begin
@@ -244,42 +257,49 @@ module tiny_axi4_target (
end
Address: begin
if (!enable_i) begin
s_req_d.state = AbortResponse;
s_req_d.error_seen = 1'b1;
s_req_d.error_addr = s_req_addr;
s_req_d.error_resp = 2'b11;
s_req_d.state = s_req_q.write ? AbortWrite : AbortResponse;
end else if (s_req_q.write ? target.awready : target.arready) s_req_d.state = Response;
end
Response: begin
if (!enable_i) begin
s_req_d.state = AbortResponse;
s_req_d.error_seen = 1'b1;
s_req_d.error_addr = s_req_addr;
s_req_d.error_resp = 2'b11;
s_req_d.state = (s_req_q.write && !s_req_q.write_done) ? AbortWrite : AbortResponse;
end
if (target.wvalid && target.wready) begin
s_req_d.write_beat = s_req_q.write_beat + 8'd1;
if (target.wlast || (s_req_q.write_beat == s_saved_addr.len)) s_req_d.write_done = 1'b1;
end
if (s_read_capture) begin
if (s_saved_addr.burst == 2'b01)
s_req_d.read_addr = s_req_q.read_addr + (32'd1 << s_saved_addr.size);
if (!s_req_q.error_seen && (target.rresp != 2'b00)) begin
s_req_d.error_seen = 1'b1;
s_req_d.error_addr = s_req_q.read_addr;
s_req_d.error_resp = target.rresp;
if (s_terminal) s_req_d.state = Idle;
end
AbortWrite: begin
if (s_wvalid[s_req_q.owner] && !s_req_q.write_done) begin
s_req_d.write_beat = s_req_q.write_beat + 8'd1;
if (s_wlast[s_req_q.owner] || (s_req_q.write_beat == s_saved_addr.len)) begin
s_req_d.write_done = 1'b1;
s_req_d.state = AbortResponse;
end
end
if (s_write_capture && !s_req_q.error_seen && (target.bresp != 2'b00)) begin
s_req_d.error_seen = 1'b1;
s_req_d.error_addr = s_saved_addr.addr;
s_req_d.error_resp = target.bresp;
end
if (s_terminal) s_req_d.state = Idle;
end
AbortResponse: if (s_terminal) s_req_d.state = Idle;
default: s_req_d.state = Idle;
endcase
if (s_read_capture) begin
s_req_d.read_count = s_req_q.read_count + 9'd1;
if (s_saved_addr.burst == 2'b01)
s_req_d.read_addr = s_req_q.read_addr + (32'd1 << s_saved_addr.size);
if (!s_req_q.error_seen && (s_rin_data[3:2] != 2'b00)) begin
s_req_d.error_seen = 1'b1;
s_req_d.error_addr = s_req_q.read_addr;
s_req_d.error_resp = s_rin_data[3:2];
end
end
if (s_write_capture) begin
s_req_d.b_captured = 1'b1;
if (!s_req_q.error_seen && (s_bin_data[2:1] != 2'b00)) begin
s_req_d.error_seen = 1'b1;
s_req_d.error_addr = s_req_addr;
s_req_d.error_resp = s_bin_data[2:1];
end
end
end
dffr #(
.DATA_WIDTH($bits(request_t))
@@ -334,17 +354,17 @@ module tiny_axi4_target (
end
`endif
`ifdef HAVE_SVA
assert property (@(posedge clk_i) disable iff (!rst_n_i)
assert property (@(posedge clk_i) disable iff (!rst_n_i || !enable_i)
target.wvalid && !target.wready |=> target.wvalid &&
$stable(
{target.wdata, target.wstrb, target.wlast, target.wuser}
));
assert property (@(posedge clk_i) disable iff (!rst_n_i)
assert property (@(posedge clk_i) disable iff (!rst_n_i || !enable_i)
target.arvalid && !target.arready |=> target.arvalid &&
$stable(
{target.araddr, target.arlen, target.arid, target.arsize, target.arburst}
));
assert property (@(posedge clk_i) disable iff (!rst_n_i)
assert property (@(posedge clk_i) disable iff (!rst_n_i || !enable_i)
target.awvalid && !target.awready |=> target.awvalid &&
$stable(
{target.awaddr, target.awlen, target.awid, target.awsize, target.awburst}
tests/rtl/tiny_r2_p5_fabric_formal.sv
+30 -6
View File
@@ -2,9 +2,16 @@ module tiny_r2_p5_fabric_formal (
input logic clk_i,
rst_n_i
);
`ifdef TINY_P5_RESET_FORMAL
localparam bit TargetReset = 1'b1;
`else
localparam bit TargetReset = 1'b0;
`endif
logic started = 0;
(* anyseq *) logic [2:0] arvalid, awvalid, wvalid, rready, bready;
(* anyseq *) logic [2:0][1:0] length;
(* anyseq *)logic [2:0][1:0] length;
(* anyseq *)logic target_reset_n;
wire target_enable = !TargetReset || target_reset_n;
axi4_if #(
.ADDR_WIDTH(32),
.DATA_WIDTH(32),
@@ -33,7 +40,7 @@ module tiny_r2_p5_fabric_formal (
tiny_axi4_target u_target (
.clk_i (clk_i),
.rst_n_i (rst_n_i),
.enable_i (1'b1),
.enable_i (target_enable),
.masters (masters),
.target (target),
.idle_o (idle),
@@ -48,11 +55,13 @@ module tiny_r2_p5_fabric_formal (
.Response(2'b10)
) u_endpoint (
.clk_i (clk_i),
.rst_n_i(rst_n_i),
.rst_n_i(rst_n_i && target_enable),
.axi4 (target)
);
for (genvar m = 0; m < 3; m++) begin : gen_master
logic outstanding = 0;
logic [2:0] remaining = 0;
logic write_data_pending = 0;
wire accept=(masters[m].arvalid && masters[m].arready)||(masters[m].awvalid && masters[m].awready);
wire done=(masters[m].rvalid && masters[m].rready && masters[m].rlast)||
(masters[m].bvalid && masters[m].bready);
@@ -88,15 +97,30 @@ module tiny_r2_p5_fabric_formal (
assign masters[m].rready = rready[m];
assign masters[m].bready = bready[m];
always_ff @(posedge clk_i) begin
if (!rst_n_i) outstanding <= 0;
else begin
if (!rst_n_i) begin
outstanding <= 0;
remaining <= 0;
write_data_pending <= 0;
end else begin
if (masters[m].arvalid && masters[m].arready) remaining <= {1'b0, length[m]} + 3'd1;
if (masters[m].rvalid) begin
assert (remaining != 0);
assert (masters[m].rlast == (remaining == 1));
if (masters[m].rready) remaining <= remaining - 3'd1;
end
if (masters[m].awvalid && masters[m].awready) write_data_pending <= 1;
if (masters[m].wvalid && masters[m].wready) write_data_pending <= 0;
if (masters[m].bvalid) assert (!write_data_pending);
if (accept) outstanding <= 1;
if (done) outstanding <= 0;
assert (!(accept && outstanding));
assert (!done || outstanding);
assert (!(masters[m].arready && masters[m].awready));
if (done) begin
assert (fault && fault_owner == 2'(m) && fault_resp == 2);
assert (fault && fault_owner == 2'(m));
if (TargetReset)
assert (fault_resp == 2 || fault_resp == 3);
else assert (fault_resp == 2);
assert (fault_addr == 32'h30000000 + 32'(m) * 32'h100);
end
end
tests/rtl/tiny_r2_p5_reset_tb.sv
+405 -168
View File
@@ -1,11 +1,8 @@
`timescale 1ns / 1ps
module tiny_r2_p5_reset_tb;
logic clk_i = 0;
logic rst_n_i = 0;
logic target_rst_n[23];
logic clk_i = 0, rst_n_i = 0;
always #5 clk_i = !clk_i;
logic target_rst_n[23];
axi4_if #(
.ADDR_WIDTH(32),
.DATA_WIDTH(32),
@@ -24,29 +21,35 @@ module tiny_r2_p5_reset_tb;
.aclk (clk_i),
.aresetn(target_rst_n)
);
apb4_if apb (
.pclk (clk_i),
.presetn(target_rst_n[12])
);
logic [22:0] hold_address = '0, hold_read = '0, hold_write = '0, hold_b = '0;
integer error_beat[23];
integer captures[23], addresses[23], writes[23];
logic [5:0] fault_valid, fault_instruction;
logic [ 5:0][31:0] fault_addr;
logic [ 5:0][ 1:0] fault_resp;
logic [ 2:0] owner_idle;
logic [22:0] target_idle;
logic [63:0] cpu_wait, dma_wait;
logic hold_address[23];
logic hold_read [23];
logic hold_write [23];
logic hold_b [23];
logic [2:0] arvalid = '0, rready = '0, awvalid = '0, wvalid = '0, bready = '0;
logic [2:0][31:0] araddr = '0, awaddr = '0, wdata = '0;
logic [2:0][7:0] arlen = '0, awlen = '0;
logic [2:0][2:0] arsize = '0, awsize = '0;
logic [2:0][1:0] arburst = '0, awburst = '0;
logic [2:0] arlock = '0, awlock = '0;
logic [2:0] arid = '0, awid = '0;
logic [2:0][3:0] wstrb = '0;
logic [2:0] wlast = '0;
logic [2:0][2:0] arprot = '0;
logic [2:0] arready, awready, rvalid, bvalid;
logic [2:0][1:0] rresp, bresp;
logic [2:0] rlast;
logic [2:0] arvalid = 0, awvalid = 0, wvalid = 0, rready = 0, bready = 0;
logic [2:0][31:0] araddr = 0, awaddr = 0, wdata = 0;
logic [2:0][7:0] arlen = 0, awlen = 0;
logic [2:0] wlast = 0;
wire [2:0] arready, awready, wready, rvalid, bvalid, rlast, rid, bid;
wire [2:0][1:0] rresp, bresp;
wire [2:0][31:0] rdata;
integer faults [6];
logic [5:0][31:0] last_fault_addr;
logic [5:0][ 1:0] last_fault_resp;
integer cases = 0;
logic dma_start = 0, dma_valid = 0, dma_start_ready, dma_ready, dma_busy, dma_done;
logic [31:0] dma_addr = 0, dma_data = 0;
logic [4:0] dma_beats = 1;
logic [1:0] dma_resp;
logic dma_id_error;
tiny_axi4_fabric u_dut (
.clk_i (clk_i),
@@ -66,185 +69,414 @@ module tiny_r2_p5_reset_tb;
.dma_wait_o (dma_wait)
);
for (genvar owner = 0; owner < 3; owner++) begin : gen_master
assign masters[owner].araddr = araddr[owner];
assign masters[owner].arlen = arlen[owner];
assign masters[owner].arsize = arsize[owner];
assign masters[owner].arburst = arburst[owner];
assign masters[owner].arlock = arlock[owner];
assign masters[owner].arid = arid[owner];
assign masters[owner].arvalid = arvalid[owner];
assign masters[owner].arprot = arprot[owner];
assign masters[owner].awaddr = awaddr[owner];
assign masters[owner].awlen = awlen[owner];
assign masters[owner].awsize = awsize[owner];
assign masters[owner].awburst = awburst[owner];
assign masters[owner].awlock = awlock[owner];
assign masters[owner].awid = awid[owner];
assign masters[owner].awvalid = awvalid[owner];
assign masters[owner].wdata = wdata[owner];
assign masters[owner].wstrb = wstrb[owner];
assign masters[owner].wlast = wlast[owner];
assign masters[owner].wvalid = wvalid[owner];
assign masters[owner].rready = rready[owner];
assign masters[owner].bready = bready[owner];
assign masters[owner].arcache = '0;
assign masters[owner].arqos = '0;
assign masters[owner].arregion = '0;
assign masters[owner].aruser = '0;
assign masters[owner].awcache = '0;
assign masters[owner].awprot = '0;
assign masters[owner].awqos = '0;
assign masters[owner].awregion = '0;
assign masters[owner].awuser = '0;
assign masters[owner].wuser = '0;
assign arready[owner] = masters[owner].arready;
assign awready[owner] = masters[owner].awready;
assign rvalid[owner] = masters[owner].rvalid;
assign rresp[owner] = masters[owner].rresp;
assign rlast[owner] = masters[owner].rlast;
assign bvalid[owner] = masters[owner].bvalid;
assign bresp[owner] = masters[owner].bresp;
// Production master: BREADY cannot rise until its last W handshake.
dma_axi4_master u_dma (
.clk_i (clk_i),
.rst_n_i (rst_n_i),
.clear_i (1'b0),
.read_start_valid_i (1'b0),
.read_start_ready_o (),
.read_addr_i (32'd0),
.read_beats_i (5'd1),
.read_fixed_i (1'b0),
.read_busy_o (),
.read_beat_valid_o (),
.read_beat_ready_i (1'b0),
.read_data_o (),
.read_resp_o (),
.read_last_o (),
.read_expected_last_o(),
.read_id_error_o (),
.read_done_o (),
.write_start_valid_i (dma_start),
.write_start_ready_o (dma_start_ready),
.write_addr_i (dma_addr),
.write_beats_i (dma_beats),
.write_fixed_i (1'b0),
.write_busy_o (dma_busy),
.write_data_valid_i (dma_valid),
.write_data_ready_o (dma_ready),
.write_data_i (dma_data),
.write_strb_i (4'hf),
.write_done_o (dma_done),
.write_resp_o (dma_resp),
.write_id_error_o (dma_id_error),
.axi4 (masters[1])
);
for (genvar m = 0; m < 3; m++) begin : gen_master
if (m != 1) begin : gen_manual
assign masters[m].araddr = araddr[m];
assign masters[m].arlen = arlen[m];
assign masters[m].arsize = 2;
assign masters[m].arburst = 1;
assign masters[m].arid = 1;
assign masters[m].arvalid = arvalid[m];
assign masters[m].arlock = 0;
assign masters[m].arprot = 0;
assign masters[m].arcache = 0;
assign masters[m].arqos = 0;
assign masters[m].arregion = 0;
assign masters[m].aruser = 0;
assign masters[m].awaddr = awaddr[m];
assign masters[m].awlen = awlen[m];
assign masters[m].awsize = 2;
assign masters[m].awburst = 1;
assign masters[m].awid = 1;
assign masters[m].awvalid = awvalid[m];
assign masters[m].awlock = 0;
assign masters[m].awprot = 0;
assign masters[m].awcache = 0;
assign masters[m].awqos = 0;
assign masters[m].awregion = 0;
assign masters[m].awuser = 0;
assign masters[m].wdata = wdata[m];
assign masters[m].wstrb = 15;
assign masters[m].wvalid = wvalid[m];
assign masters[m].wlast = wlast[m];
assign masters[m].wuser = 0;
assign masters[m].rready = rready[m];
assign masters[m].bready = bready[m];
end
assign arready[m] = masters[m].arready;
assign awready[m] = masters[m].awready;
assign wready[m] = masters[m].wready;
assign rvalid[m] = masters[m].rvalid;
assign bvalid[m] = masters[m].bvalid;
assign rlast[m] = masters[m].rlast;
assign rid[m] = masters[m].rid;
assign bid[m] = masters[m].bid;
assign rresp[m] = masters[m].rresp;
assign bresp[m] = masters[m].bresp;
assign rdata[m] = masters[m].rdata;
// Independent upstream scoreboards also run in Icarus without SVA.
integer rleft = 0, wleft = 0, bleft = 0;
logic rheld = 0, bheld = 0;
logic [36:0] saved_r;
logic [ 3:0] saved_b;
always @(posedge clk_i) begin
if (!rst_n_i) begin
rleft = 0;
wleft = 0;
bleft = 0;
rheld = 0;
bheld = 0;
end else begin
if (rheld && (!masters[m].rvalid ||
{masters[m].rid, masters[m].rdata, masters[m].rresp,
masters[m].rlast, masters[m].ruser} !== saved_r))
$fatal(1, "held R response changed");
if (bheld && (!masters[m].bvalid ||
{masters[m].bid, masters[m].bresp, masters[m].buser} !== saved_b))
$fatal(1, "held B response changed");
if (masters[m].arvalid && masters[m].arready) begin
if (rleft != 0) $fatal(1, "duplicate read admission");
rleft = integer'(masters[m].arlen) + 1;
end
if (masters[m].awvalid && masters[m].awready) begin
if (bleft != 0) $fatal(1, "duplicate write admission");
wleft = integer'(masters[m].awlen) + 1;
bleft = 1;
end
if (masters[m].bvalid && (bleft != 1 || wleft != 0))
$fatal(1, "B before complete W drain or duplicate B");
if (masters[m].wvalid && masters[m].wready) begin
if (wleft <= 0 || masters[m].wlast != (wleft == 1)) $fatal(1, "W count/last mismatch");
wleft--;
end
if (masters[m].rvalid) begin
if (rleft <= 0 || masters[m].rlast != (rleft == 1)) $fatal(1, "R count/last mismatch");
if (masters[m].rready) rleft--;
end
if (masters[m].bvalid && masters[m].bready) bleft--;
rheld = masters[m].rvalid && !masters[m].rready;
bheld = masters[m].bvalid && !masters[m].bready;
saved_r = {
masters[m].rid, masters[m].rdata, masters[m].rresp, masters[m].rlast, masters[m].ruser
};
saved_b = {masters[m].bid, masters[m].bresp, masters[m].buser};
end
end
end
for (genvar target = 0; target < 23; target++) begin : gen_target
tiny_r2_p5_reset_target_model u_model (
.clk_i (clk_i),
.rst_n_i (target_rst_n[target]),
.hold_address_i(hold_address[target]),
.hold_read_i (hold_read[target]),
.hold_write_i (hold_write[target]),
.hold_b_i (hold_b[target]),
.axi4 (targets[target])
);
for (genvar t = 0; t < 23; t++) begin : gen_target
if (t == 12) begin : gen_apb
tiny_axi42apb4 u_bridge (
.clk_i (clk_i),
.rst_n_i(target_rst_n[t]),
.axi4 (targets[t]),
.apb4 (apb)
);
end else begin : gen_memory
tiny_r2_p5_reset_target_model u_model (
.clk_i (clk_i),
.rst_n_i (target_rst_n[t]),
.hold_address_i(hold_address[t]),
.hold_read_i (hold_read[t]),
.hold_write_i (hold_write[t]),
.hold_b_i (hold_b[t]),
.error_beat_i (error_beat[t]),
.axi4 (targets[t])
);
end
always @(posedge clk_i) begin
if (rst_n_i) begin
if (targets[t].arvalid && targets[t].arready || targets[t].awvalid && targets[t].awready)
addresses[t]++;
if (targets[t].wvalid && targets[t].wready) writes[t]++;
if (targets[t].rvalid && targets[t].rready) captures[t]++;
if (!target_rst_n[t] && (targets[t].arvalid || targets[t].awvalid ||
targets[t].wvalid || targets[t].rready || targets[t].bready))
$fatal(1, "downstream handshake during target reset");
end
end
end
assign apb.pready = apb.psel && apb.penable && !hold_read[12] && !hold_b[12];
assign apb.prdata = 32'hcafe_f00d;
assign apb.pslverr = 0;
always @(posedge clk_i) begin
if (rst_n_i) begin
for (integer e = 0; e < 6; e++) begin
if (fault_valid[e]) begin
faults[e]++;
last_fault_addr[e] = fault_addr[e];
last_fault_resp[e] = fault_resp[e];
end
end
end
end
task automatic reset_read(input logic [31:0] address, input int target);
@(negedge clk_i);
araddr[0] = address;
arlen[0] = 0;
arsize[0] = 2;
arburst[0] = 1;
arid[0] = 0;
arvalid[0] = 1;
do @(posedge clk_i); while (!arready[0]);
@(negedge clk_i);
arvalid[0] = 0;
repeat (2) @(posedge clk_i);
if (owner_idle[0] || target_idle[target]) $fatal(1, "read was not retained");
target_rst_n[target] = 0;
task automatic quiet;
repeat (4) @(negedge clk_i);
if (owner_idle != 7 || target_idle != 23'h7fffff || rvalid != 0 || bvalid != 0)
$fatal(1, "credit/response not retired");
endtask
task automatic receive_read(input int index, input int beats, input logic [1:0] expected,
input logic [31:0] data);
do @(posedge clk_i); while (!rvalid[0]);
if (rresp[0] != 2'b11 || !rlast[0]) $fatal(1, "reset read did not terminate with DECERR");
@(negedge clk_i);
repeat (3) @(negedge clk_i);
if (rid[0] !== 1'b1 || rresp[0] !== expected || rdata[0] !== data ||
rlast[0] !== (index == beats - 1))
$fatal(
1,
"read data/ID/response mismatch index=%0d expected=%0d got=%0d",
index,
expected,
rresp[0]
);
rready[0] = 1;
@(posedge clk_i);
@(negedge clk_i);
rready[0] = 0;
target_rst_n[target] = 1;
repeat (2) @(posedge clk_i);
if (!owner_idle[0]) $fatal(1, "read credit was not released after reset");
rready[0] = 0;
endtask
task automatic reset_write(input logic [31:0] address, input int target);
task automatic read_case(input logic [31:0] address, input int t, input int beats,
input bit buffered, input bit before_address, input bit inject_reset);
integer first_capture, prefix, before_faults, before_addresses;
logic [ 1:0] expected;
logic [31:0] data;
@(negedge clk_i);
awaddr[1] = address;
awlen[1] = 0;
awsize[1] = 2;
awburst[1] = 1;
awid[1] = 1;
awvalid[1] = 1;
do @(posedge clk_i); while (!awready[1]);
@(negedge clk_i);
awvalid[1] = 0;
repeat (2) @(posedge clk_i);
if (owner_idle[1] || target_idle[target]) $fatal(1, "write was not retained");
target_rst_n[target] = 0;
do @(posedge clk_i); while (!bvalid[1]);
if (bresp[1] != 2'b11) $fatal(1, "reset write did not terminate with DECERR");
bready[1] = 1;
@(posedge clk_i);
@(negedge clk_i);
bready[1] = 0;
target_rst_n[target] = 1;
repeat (2) @(posedge clk_i);
if (!owner_idle[1]) $fatal(1, "write credit was not released after reset");
endtask
task automatic reset_buffered_read;
@(negedge clk_i);
araddr[0] = 32'h30000000;
arlen[0] = 0;
arsize[0] = 2;
arburst[0] = 1;
arid[0] = 0;
arvalid[0] = 1;
first_capture = captures[t];
before_faults = faults[0];
before_addresses = addresses[t];
hold_address[t] = before_address;
hold_read[t] = !buffered && inject_reset;
araddr[0] = address;
arlen[0] = 8'(beats - 1);
arvalid[0] = 1;
do @(posedge clk_i); while (!arready[0]);
@(negedge clk_i);
arvalid[0] = 0;
do @(posedge clk_i); while (!rvalid[0]);
if (rresp[0] != 2'b00) $fatal(1, "buffered read did not reach response spill");
target_rst_n[0] = 0;
do @(posedge clk_i); while (!rvalid[0]);
if (rresp[0] != 2'b11 || !rlast[0]) $fatal(1, "buffered response was replayed after reset");
rready[0] = 1;
if (buffered) begin
wait (rvalid[0]);
repeat (5) @(negedge clk_i);
end else if (!before_address) begin
wait (addresses[t] > before_addresses);
@(negedge clk_i);
end
prefix = captures[t] - first_capture;
if (inject_reset) begin
target_rst_n[t] = 0;
before_addresses = addresses[t];
repeat (3) @(negedge clk_i);
// Release the downstream reset while the upstream is still stalled.
// The cancelled session must never be issued again after release.
if (t != 0) target_rst_n[t] = 1;
hold_address[t] = 0;
hold_read[t] = 0;
repeat (4) @(negedge clk_i);
if (addresses[t] != before_addresses) $fatal(1, "cancelled AR replayed");
end
for (integer n = 0; n < beats; n++) begin
expected = inject_reset && n >= prefix ? 3 : (n == error_beat[t] ? 2 : 0);
data = expected == 3 ? 0 : (t == 12 ? 32'hcafe_f00d : (address + 32'(4 * n)) ^ 32'h10000000);
receive_read(n, beats, expected, data);
end
target_rst_n[t] = 1;
quiet();
if (inject_reset && (prefix < beats || (error_beat[t] >= 0 && error_beat[t] < prefix))) begin
expected = (error_beat[t] >= 0 && error_beat[t] < prefix) ? 2 : 3;
if (faults[0] != before_faults + 1 || last_fault_resp[0] != expected ||
last_fault_addr[0] != address + 32'(4 * (expected == 2 ? error_beat[t] : prefix)))
$fatal(1, "first failing read beat metadata/count lost");
end else if (faults[0] != before_faults) $fatal(1, "spurious read fault");
cases++;
endtask
task automatic send_word(input int n, input int beats);
@(negedge clk_i);
wdata[2] = 32'ha5000000 + 32'(n);
wlast[2] = n == beats - 1;
wvalid[2] = 1;
do @(posedge clk_i); while (!wready[2]);
@(negedge clk_i);
wvalid[2] = 0;
endtask
task automatic write_case(input logic [31:0] address, input int t, input int beats,
input int prefix, input bit buffered, input bit before_address);
integer before_faults, after_writes;
@(negedge clk_i);
before_faults = faults[5];
hold_address[t] = before_address;
hold_b[t] = !buffered;
awaddr[2] = address;
awlen[2] = 8'(beats - 1);
awvalid[2] = 1;
do @(posedge clk_i); while (!awready[2]);
@(negedge clk_i);
awvalid[2] = 0;
for (integer n = 0; n < prefix; n++) send_word(n, beats);
if (buffered) begin
wait (bvalid[2]);
repeat (3) @(negedge clk_i);
end
target_rst_n[t] = 0;
after_writes = writes[t];
repeat (3) @(negedge clk_i);
if (t != 0) target_rst_n[t] = 1;
hold_address[t] = 0;
hold_b[t] = 0;
for (integer n = prefix; n < beats; n++) begin
if (bvalid[2]) $fatal(1, "write response before remaining data");
send_word(n, beats);
end
do @(posedge clk_i); while (!bvalid[2]);
@(negedge clk_i);
repeat (5) @(negedge clk_i);
if (bresp[2] != (buffered ? 0 : 3) || bid[2] !== 1'b1 || writes[t] != after_writes)
$fatal(1, "write response/ID or downstream session replay");
bready[2] = 1;
@(posedge clk_i);
@(negedge clk_i);
rready[0] = 0;
target_rst_n[0] = 1;
repeat (2) @(posedge clk_i);
if (!owner_idle[0]) $fatal(1, "buffered read credit was not released after reset");
bready[2] = 0;
target_rst_n[t] = 1;
quiet();
if (faults[5] != before_faults + (buffered ? 0 : 1)) $fatal(1, "write fault count mismatch");
cases++;
endtask
task automatic dma_case(input logic [31:0] address, input int t, input int beats,
input int prefix);
integer before_faults, after_writes;
@(negedge clk_i);
before_faults = faults[3];
hold_b[t] = 1;
dma_addr = address;
dma_beats = 5'(beats);
dma_start = 1;
do @(posedge clk_i); while (!dma_start_ready);
@(negedge clk_i);
dma_start = 0;
wait (!owner_idle[1]);
@(negedge clk_i);
for (integer n = 0; n < beats; n++) begin
if (n == prefix) begin
target_rst_n[t] = 0;
after_writes = writes[t];
repeat (3) @(negedge clk_i);
target_rst_n[t] = 1;
hold_b[t] = 0;
end
dma_data = 32'h5a000000 + 32'(n);
dma_valid = 1;
do @(posedge clk_i); while (!dma_ready);
@(negedge clk_i);
dma_valid = 0;
end
do @(posedge clk_i); while (!dma_done);
if (dma_resp != 3 || dma_id_error) $fatal(1, "production DMA did not terminate with error");
@(negedge clk_i);
quiet();
if (dma_busy || writes[t] != after_writes || faults[3] != before_faults + 1)
$fatal(1, "production DMA write drain/credit/count failure");
cases++;
endtask
initial begin
for (integer target = 0; target < 23; target++) begin
target_rst_n[target] = 0;
hold_address[target] = 0;
hold_read[target] = 0;
hold_write[target] = 0;
hold_b[target] = 0;
for (integer t = 0; t < 23; t++) begin
target_rst_n[t] = 0;
captures[t] = 0;
addresses[t] = 0;
writes[t] = 0;
error_beat[t] = -1;
end
hold_read[0] = 1;
hold_write[12] = 1;
for (integer e = 0; e < 6; e++) faults[e] = 0;
repeat (4) @(negedge clk_i);
rst_n_i = 1;
for (integer target = 0; target < 23; target++) target_rst_n[target] = 1;
reset_read(32'h30000000, 0);
hold_read[0] = 0;
reset_buffered_read();
reset_write(32'h10009000, 12);
if (fault_valid != 0) $fatal(1, "fault pulse was not consumed");
for (integer t = 0; t < 23; t++) target_rst_n[t] = 1;
// SRAM and XPI: address cancellation, missing 16 beats, two captured
// beats under backpressure, and already captured successful completion.
for (integer t = 0; t < 5; t += 4) begin
read_case(t == 0 ? 32'h30000000 : 32'h50000000, t, 16, 0, 1, 1);
read_case(t == 0 ? 32'h30000000 : 32'h50000000, t, 16, 0, 0, 1);
read_case(t == 0 ? 32'h30000000 : 32'h50000000, t, 16, 1, 0, 1);
read_case(t == 0 ? 32'h30000000 : 32'h50000000, t, 1, 1, 0, 1);
read_case(t == 0 ? 32'h30000000 : 32'h50000000, t, 1, 1, 0, 0);
write_case(t == 0 ? 32'h30000000 : 32'h50000000, t, 16, 0, 0, 1);
write_case(t == 0 ? 32'h30000000 : 32'h50000000, t, 16, 2, 0, 0);
write_case(t == 0 ? 32'h30000000 : 32'h50000000, t, 16, 16, 0, 0);
write_case(t == 0 ? 32'h30000000 : 32'h50000000, t, 1, 1, 1, 0);
dma_case(t == 0 ? 32'h30000000 : 32'h50000000, t, 16, 2);
end
error_beat[0] = 1;
read_case(32'h30000000, 0, 16, 1, 0, 1);
error_beat[0] = -1;
// Actual APB bridge, with a withheld peripheral completion.
read_case(32'h10009000, 12, 1, 0, 1, 1);
read_case(32'h10009000, 12, 1, 0, 0, 1);
read_case(32'h10009000, 12, 1, 1, 0, 1);
write_case(32'h10009000, 12, 1, 0, 0, 1);
write_case(32'h10009000, 12, 1, 1, 0, 0);
write_case(32'h10009000, 12, 1, 1, 1, 0);
dma_case(32'h10009000, 12, 1, 0);
$display("P5_RESET cases=%0d production_dma=3 burst_beats=16 held_RB=1 first_fault=1", cases);
$display("SIM_TEST_PASS Tiny P5 target reset isolation");
$finish;
end
initial begin
repeat (2000) @(posedge clk_i);
$fatal(1, "SIM_TEST_TIMEOUT Tiny P5 target reset isolation");
repeat (20000) @(posedge clk_i);
$fatal(1, "SIM_TEST_TIMEOUT Tiny P5 target reset isolation cases=%0d", cases);
end
endmodule
module tiny_r2_p5_reset_target_model (
input logic clk_i,
input logic rst_n_i,
input logic hold_address_i,
input logic hold_read_i,
input logic hold_write_i,
input logic hold_b_i,
rst_n_i,
hold_address_i,
hold_read_i,
hold_write_i,
hold_b_i,
input integer error_beat_i,
axi4_if.slave axi4
);
logic active = 0;
logic writing = 0;
logic write_done = 0;
logic id = 0;
logic active = 0, writing = 0, write_done = 0, id = 0;
logic [31:0] address = 0;
logic [ 7:0] length = 0;
logic [ 7:0] beat = 0;
logic [7:0] length = 0, beat = 0;
assign axi4.arready = !active && !hold_address_i && rst_n_i;
assign axi4.awready = !active && !hold_address_i && !axi4.arvalid && rst_n_i;
assign axi4.wready = active && writing && !write_done && !hold_write_i && rst_n_i;
assign axi4.ruser = 0;
assign axi4.buser = 0;
always @(posedge clk_i) begin
always @(posedge clk_i or negedge rst_n_i) begin
if (!rst_n_i) begin
active <= 0;
writing <= 0;
@@ -270,7 +502,6 @@ module tiny_r2_p5_reset_target_model (
active <= 1;
writing <= 1;
write_done <= 0;
address <= axi4.awaddr;
length <= axi4.awlen;
beat <= 0;
id <= axi4.awid;
@@ -279,17 +510,22 @@ module tiny_r2_p5_reset_target_model (
axi4.rvalid <= 1;
axi4.rid <= id;
axi4.rdata <= 32'h10000000 ^ address;
axi4.rresp <= 0;
axi4.rresp <= integer'(beat) == error_beat_i ? 2 : 0;
axi4.rlast <= beat == length;
end
if (axi4.rvalid && axi4.rready) begin
axi4.rvalid <= 0;
active <= 0;
if (axi4.rlast) active <= 0;
else begin
beat <= beat + 1;
address <= address + 4;
end
end
if (axi4.wvalid && axi4.wready) begin
write_done <= 1;
if (beat == length) write_done <= 1;
else beat <= beat + 1;
end
if (active && writing && write_done && !hold_b_i) begin
if (active && writing && write_done && !axi4.bvalid && !hold_b_i) begin
axi4.bvalid <= 1;
axi4.bid <= id;
axi4.bresp <= 0;
@@ -297,6 +533,7 @@ module tiny_r2_p5_reset_target_model (
if (axi4.bvalid && axi4.bready) begin
axi4.bvalid <= 0;
active <= 0;
write_done <= 0;
end
end
end
tests/test_publication_tiny.py
+18
View File
@@ -54,6 +54,24 @@ def test_common_register_default_remains_mini_compatible():
assert "SOC_SYSCTRL_TEST_STATUS_OFFSET" in constants
@pytest.mark.parametrize("before,after", [
("s_req_q.write_done && !s_req_q.b_captured", "1'b1"),
("s_r_valid && s_rready[s_req_q.owner] && s_r_data[1]", "s_r_valid"),
(".flush_i(1'b0)", ".flush_i(!enable_i)"),
])
def test_target_reset_contract_rejects_unsafe_completion(tmp_path, before, after):
contract = tiny.read(ROOT / tiny.BOOK / "source-contract.json")
binding = next(item for item in contract["bindings"]
if item["file"] == "rtl/tiny/top/tiny_axi4_target.sv")
path = tmp_path / binding["file"]
path.parent.mkdir(parents=True)
original = (ROOT / binding["file"]).read_text()
assert before in original
path.write_text(original.replace(before, after))
with pytest.raises(ValueError, match="Tiny behavior binding changed"):
tiny.require_snippets(tmp_path, binding["file"], binding["text"])
def test_reset_update_does_not_bypass_reviewed_snapshot(monkeypatch):
original = tiny.subprocess.check_output
checked = []
tests/test_tiny_r2_p5.py
+6 -3
View File
@@ -71,9 +71,11 @@ def test_concurrent_fabric(tmp_path, simulator):
@pytest.mark.parametrize("simulator", ["iverilog", "verilator"])
def test_target_reset_isolation(tmp_path, simulator):
files, includes = sources(tmp_path)
files.append(ROOT / "rtl/ip/peripheral/dma_axi4_master.sv")
files.append(ROOT / "tests/rtl/tiny_r2_p5_reset_tb.sv")
log = simulate(tmp_path, simulator, "tiny_r2_p5_reset_tb", files, includes)
assert "SIM_TEST_PASS Tiny P5 target reset isolation" in log
assert "P5_RESET cases=28 production_dma=3 burst_beats=16 held_RB=1 first_fault=1" in log
@pytest.mark.parametrize("simulator", ["iverilog", "verilator"])
@@ -103,14 +105,15 @@ def test_real_cpu_dma_progress_and_abort(tmp_path, simulator):
assert "hart_reset=1 abort_drained=1" in log
@pytest.mark.parametrize("kind", ["fabric", "fault"])
@pytest.mark.parametrize("kind", ["fabric", "fabric_reset", "fault"])
def test_protocol_proofs(tmp_path, kind):
for tool in ("sv2v", "yosys"):
assert shutil.which(tool), f"required tool unavailable: {tool}"
files, includes = sources(tmp_path)
top = f"tiny_r2_p5_{kind}_formal"
top = f"tiny_r2_p5_{'fabric' if kind == 'fabric_reset' else kind}_formal"
files.append(ROOT / f"tests/rtl/{top}.sv")
converted = subprocess.run(["sv2v", "-DFORMAL", "-DSV_ASSRT_DISABLE", *includes,
reset_define = ["-DTINY_P5_RESET_FORMAL"] if kind == "fabric_reset" else []
converted = subprocess.run(["sv2v", "-DFORMAL", "-DSV_ASSRT_DISABLE", *reset_define, *includes,
*(str(p) for p in files)], text=True, capture_output=True, timeout=180)
(tmp_path / "sv2v.log").write_text(converted.stderr)
assert converted.returncode == 0, converted.stderr