Skip to content

Commit

Permalink
Merge pull request #259 from pulp-platform/axi_intf_page_assert
Browse files Browse the repository at this point in the history 
AXI_BUS_DV: Assert burst on one page
  • Loading branch information
@micprog
micprog authored Jul 25, 2024
2 parents 71ed21a + ca46950 commit 556737b
Show file tree
Hide file tree
Showing 4 changed files with 142 additions and 108 deletions.
2 changes: 2 additions & 0 deletions CHANGELOG.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,14 @@ and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.
### Added
- `axi_sim_mem`: Increase number of request ports, add multiport interface variant.
- `axi_bus_compare`: Optionally consider AXI `size` field to only compare used data.
- `AXI_BUS_DV`: Add property checking that bursts do not cross 4KiB page boundaries.

### Fixed
- `axi_bus_compare`: Fix mismatch detection.
- `axi_to_detailed_mem`: Only respond with `exokay` if `lock` was set on the request.
Bump `common_cells` for `mem_to_banks` fix.
- `axi_dw_downsizer`: Fix `i_forward_b_beats_queue` underflow.
- `axi_test`: Ensure random requests do not cross 4KiB page boundaries.

## 0.39.3 - 2024-05-08
### Added
Expand Down
10 changes: 10 additions & 0 deletions src/axi_intf.sv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -249,6 +249,16 @@ interface AXI_BUS_DV #(
assert property (@(posedge clk_i) ( r_valid && ! r_ready |=> $stable(r_last)));
assert property (@(posedge clk_i) ( r_valid && ! r_ready |=> $stable(r_user)));
assert property (@(posedge clk_i) ( r_valid && ! r_ready |=> r_valid));
// Address-Channel Assertions: The address of the last beat of a burst must be on the same 4 KiB
// page as the address of the first beat of a burst. Bus is always word-aligned, word < page.
assert property (@(posedge clk_i) aw_valid |-> (aw_burst != axi_pkg::BURST_INCR) || (
axi_pkg::beat_addr(aw_addr, aw_size, aw_len, aw_burst, 0) >> 12 == // lowest beat address
axi_pkg::beat_addr(aw_addr, aw_size, aw_len, aw_burst, aw_len) >> 12 // highest beat address
)) else $error("AW burst crossing 4 KiB page boundary detected, which is illegal!");
assert property (@(posedge clk_i) ar_valid |-> (aw_burst != axi_pkg::BURST_INCR) || (
axi_pkg::beat_addr(ar_addr, ar_size, ar_len, ar_burst, 0) >> 12 == // lowest beat address
axi_pkg::beat_addr(ar_addr, ar_size, ar_len, ar_burst, ar_len) >> 12 // highest beat address
)) else $error("AR burst crossing 4 KiB page boundary detected, which is illegal!");
`endif
// pragma translate_on

Expand Down
198 changes: 103 additions & 95 deletions src/axi_test.sv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -905,14 +905,9 @@ package axi_test;
addr + len <= mem_region.addr_end;
}; assert(rand_success);

if (ax_beat.ax_burst == axi_pkg::BURST_FIXED) begin
if (((addr + 2**ax_beat.ax_size) & PFN_MASK) == (addr & PFN_MASK)) begin
break;
end
end else begin // BURST_INCR
if (((addr + 2**ax_beat.ax_size * (ax_beat.ax_len + 1)) & PFN_MASK) == (addr & PFN_MASK)) begin
break;
end
if (axi_pkg::beat_addr(addr, ax_beat.ax_size, ax_beat.ax_len, ax_beat.ax_burst, 0) >> 12 ==
axi_pkg::beat_addr(addr, ax_beat.ax_size, ax_beat.ax_len, ax_beat.ax_burst, ax_beat.ax_len) >> 12) begin
break;
end
end
end else begin
Expand All @@ -937,14 +932,9 @@ package axi_test;
addr + ((len + 1) << size) <= mem_region.addr_end;
}; assert(rand_success);

if (ax_beat.ax_burst == axi_pkg::BURST_FIXED) begin
if (((addr + 2**ax_beat.ax_size) & PFN_MASK) == (addr & PFN_MASK)) begin
break;
end
end else begin // BURST_INCR, BURST_WRAP
if (((addr + 2**ax_beat.ax_size * (ax_beat.ax_len + 1)) & PFN_MASK) == (addr & PFN_MASK)) begin
break;
end
if (axi_pkg::beat_addr(addr, ax_beat.ax_size, ax_beat.ax_len, ax_beat.ax_burst, 0) >> 12 ==
axi_pkg::beat_addr(addr, ax_beat.ax_size, ax_beat.ax_len, ax_beat.ax_burst, ax_beat.ax_len) >> 12) begin
break;
end
end
end
Expand All @@ -961,98 +951,116 @@ package axi_test;

task rand_atop_burst(inout ax_beat_t beat);
automatic logic rand_success;
beat.ax_atop[5:4] = $random();
if (beat.ax_atop[5:4] != 2'b00 && !AXI_BURST_INCR) begin
// We can emit ATOPs only if INCR bursts are allowed.
$warning("ATOP suppressed because INCR bursts are disabled!");
beat.ax_atop[5:4] = 2'b00;
end
if (beat.ax_atop[5:4] != 2'b00) begin // ATOP
// Determine `ax_atop`.
if (beat.ax_atop[5:4] == axi_pkg::ATOP_ATOMICSTORE ||
beat.ax_atop[5:4] == axi_pkg::ATOP_ATOMICLOAD) begin
// Endianness
beat.ax_atop[3] = $random();
// Atomic operation
beat.ax_atop[2:0] = $random();
end else begin // Atomic{Swap,Compare}
beat.ax_atop[3:1] = '0;
beat.ax_atop[0] = $random();
forever begin
beat.ax_atop[5:4] = $random();
if (beat.ax_atop[5:4] != 2'b00 && !AXI_BURST_INCR) begin
// We can emit ATOPs only if INCR bursts are allowed.
$warning("ATOP suppressed because INCR bursts are disabled!");
beat.ax_atop[5:4] = 2'b00;
end
// Determine `ax_size` and `ax_len`.
if (2**beat.ax_size < AXI_STRB_WIDTH) begin
// Transaction does *not* occupy full data bus, so we must send just one beat. [E1.1.3]
beat.ax_len = '0;
end else begin
automatic int unsigned bytes;
if (beat.ax_atop == axi_pkg::ATOP_ATOMICCMP) begin
// Total data transferred in burst can be 2, 4, 8, 16, or 32 B.
automatic int unsigned log_bytes;
rand_success = std::randomize(log_bytes) with {
log_bytes > 0; 2**log_bytes <= 32;
}; assert(rand_success);
bytes = 2**log_bytes;
if (beat.ax_atop[5:4] != 2'b00) begin // ATOP
// Determine `ax_atop`.
if (beat.ax_atop[5:4] == axi_pkg::ATOP_ATOMICSTORE ||
beat.ax_atop[5:4] == axi_pkg::ATOP_ATOMICLOAD) begin
// Endianness
beat.ax_atop[3] = $random();
// Atomic operation
beat.ax_atop[2:0] = $random();
end else begin // Atomic{Swap,Compare}
beat.ax_atop[3:1] = '0;
beat.ax_atop[0] = $random();
end
// Determine `ax_size` and `ax_len`.
if (2**beat.ax_size < AXI_STRB_WIDTH) begin
// Transaction does *not* occupy full data bus, so we must send just one beat. [E1.1.3]
beat.ax_len = '0;
end else begin
// Total data transferred in burst can be 1, 2, 4, or 8 B.
if (AXI_STRB_WIDTH >= 8) begin
bytes = AXI_STRB_WIDTH;
end else begin
automatic int unsigned bytes;
if (beat.ax_atop == axi_pkg::ATOP_ATOMICCMP) begin
// Total data transferred in burst can be 2, 4, 8, 16, or 32 B.
automatic int unsigned log_bytes;
rand_success = std::randomize(log_bytes); assert(rand_success);
log_bytes = log_bytes % (4 - $clog2(AXI_STRB_WIDTH)) - $clog2(AXI_STRB_WIDTH);
rand_success = std::randomize(log_bytes) with {
log_bytes > 0; 2**log_bytes <= 32;
}; assert(rand_success);
bytes = 2**log_bytes;
end else begin
// Total data transferred in burst can be 1, 2, 4, or 8 B.
if (AXI_STRB_WIDTH >= 8) begin
bytes = AXI_STRB_WIDTH;
end else begin
automatic int unsigned log_bytes;
rand_success = std::randomize(log_bytes); assert(rand_success);
log_bytes = log_bytes % (4 - $clog2(AXI_STRB_WIDTH)) - $clog2(AXI_STRB_WIDTH);
bytes = 2**log_bytes;
end
end
beat.ax_len = bytes / AXI_STRB_WIDTH - 1;
end
beat.ax_len = bytes / AXI_STRB_WIDTH - 1;
end
// Determine `ax_addr` and `ax_burst`.
if (beat.ax_atop == axi_pkg::ATOP_ATOMICCMP) begin
// The address must be aligned to half the outbound data size. [E1.1.3]
beat.ax_addr = beat.ax_addr & ~((1'b1 << beat.ax_size) - 1);
// If the address is aligned to the total size of outgoing data, the burst type must be
// INCR. Otherwise, it must be WRAP. [E1.1.3]
beat.ax_burst = (beat.ax_addr % ((beat.ax_len+1) * 2**beat.ax_size) == 0) ?
axi_pkg::BURST_INCR : axi_pkg::BURST_WRAP;
// If we are not allowed to emit WRAP bursts, align the address to the total size of
// outgoing data and fall back to INCR.
if (beat.ax_burst == axi_pkg::BURST_WRAP && !AXI_BURST_WRAP) begin
beat.ax_addr -= (beat.ax_addr % ((beat.ax_len+1) * 2**beat.ax_size));
// Determine `ax_addr` and `ax_burst`.
if (beat.ax_atop == axi_pkg::ATOP_ATOMICCMP) begin
// The address must be aligned to half the outbound data size. [E1.1.3]
beat.ax_addr = beat.ax_addr & ~((1'b1 << beat.ax_size) - 1);
// If the address is aligned to the total size of outgoing data, the burst type must be
// INCR. Otherwise, it must be WRAP. [E1.1.3]
beat.ax_burst = (beat.ax_addr % ((beat.ax_len+1) * 2**beat.ax_size) == 0) ?
axi_pkg::BURST_INCR : axi_pkg::BURST_WRAP;
// If we are not allowed to emit WRAP bursts, align the address to the total size of
// outgoing data and fall back to INCR.
if (beat.ax_burst == axi_pkg::BURST_WRAP && !AXI_BURST_WRAP) begin
beat.ax_addr -= (beat.ax_addr % ((beat.ax_len+1) * 2**beat.ax_size));
beat.ax_burst = axi_pkg::BURST_INCR;
end
end else begin
// The address must be aligned to the data size. [E1.1.3]
beat.ax_addr = beat.ax_addr & ~((1'b1 << (beat.ax_size+1)) - 1);
// Only INCR allowed.
beat.ax_burst = axi_pkg::BURST_INCR;
end
end else begin
// The address must be aligned to the data size. [E1.1.3]
beat.ax_addr = beat.ax_addr & ~((1'b1 << (beat.ax_size+1)) - 1);
// Only INCR allowed.
beat.ax_burst = axi_pkg::BURST_INCR;
// Make sure that the burst does not cross a 4KiB boundary.
if (axi_pkg::beat_addr(beat.ax_addr, beat.ax_size, beat.ax_len, beat.ax_burst, 0) >> 12 ==
axi_pkg::beat_addr(beat.ax_addr, beat.ax_size, beat.ax_len, beat.ax_burst, beat.ax_len) >> 12) begin
break;
end else begin
beat = new_rand_burst(1'b0);
end
end
end
endtask

function void rand_excl_ar(inout ax_beat_t ar_beat);
ar_beat.ax_lock = $random();
if (ar_beat.ax_lock) begin
automatic logic rand_success;
automatic int unsigned n_bytes;
automatic size_t size;
automatic addr_t addr_mask;
// In an exclusive burst, the number of bytes to be transferred must be a power of 2, i.e.,
// 1, 2, 4, 8, 16, 32, 64, or 128 bytes, and the burst length must not exceed 16 transfers.
static int unsigned ul = (AXI_STRB_WIDTH < 8) ? 4 + $clog2(AXI_STRB_WIDTH) : 7;
rand_success = std::randomize(n_bytes) with {
n_bytes >= 1;
n_bytes <= ul;
}; assert(rand_success);
n_bytes = 2**n_bytes;
rand_success = std::randomize(size) with {
size >= 0;
2**size <= n_bytes;
2**size <= AXI_STRB_WIDTH;
n_bytes / 2**size <= 16;
}; assert(rand_success);
ar_beat.ax_size = size;
ar_beat.ax_len = n_bytes / 2**size;
// The address must be aligned to the total number of bytes in the burst.
ar_beat.ax_addr = ar_beat.ax_addr & ~(n_bytes-1);
forever begin
ar_beat.ax_lock = $random();
if (ar_beat.ax_lock) begin
automatic logic rand_success;
automatic int unsigned n_bytes;
automatic size_t size;
automatic addr_t addr_mask;
// In an exclusive burst, the number of bytes to be transferred must be a power of 2, i.e.,
// 1, 2, 4, 8, 16, 32, 64, or 128 bytes, and the burst length must not exceed 16 transfers.
static int unsigned ul = (AXI_STRB_WIDTH < 8) ? 4 + $clog2(AXI_STRB_WIDTH) : 7;
rand_success = std::randomize(n_bytes) with {
n_bytes >= 1;
n_bytes <= ul;
}; assert(rand_success);
n_bytes = 2**n_bytes;
rand_success = std::randomize(size) with {
size >= 0;
2**size <= n_bytes;
2**size <= AXI_STRB_WIDTH;
n_bytes / 2**size <= 16;
}; assert(rand_success);
ar_beat.ax_size = size;
ar_beat.ax_len = n_bytes / 2**size;
// The address must be aligned to the total number of bytes in the burst.
ar_beat.ax_addr = ar_beat.ax_addr & ~(n_bytes-1);
end
// Make sure that the burst does not cross a 4KiB boundary.
if (axi_pkg::beat_addr(ar_beat.ax_addr, ar_beat.ax_size, ar_beat.ax_len, ar_beat.ax_burst, 0) >> 12 ==
axi_pkg::beat_addr(ar_beat.ax_addr, ar_beat.ax_size, ar_beat.ax_len, ar_beat.ax_burst, ar_beat.ax_len) >> 12) begin
break;
end else begin
ar_beat = new_rand_burst(1'b1);
end
end
endfunction

Expand Down
40 changes: 27 additions & 13 deletions test/tb_axi_sim_mem.sv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -99,18 +99,25 @@ module tb_axi_sim_mem #(
drv.reset_master();
wait (rst_n);
// AW
forever begin
`ifdef XSIM
// std::randomize(aw_beat) may behave differently to aw_beat.randomize() wrt. limited ranges
// Keeping alternate implementation for XSIM only
rand_success = std::randomize(aw_beat); assert (rand_success);
// std::randomize(aw_beat) may behave differently to aw_beat.randomize() wrt. limited ranges
// Keeping alternate implementation for XSIM only
rand_success = std::randomize(aw_beat); assert (rand_success);
`else
rand_success = aw_beat.randomize(); assert (rand_success);
rand_success = aw_beat.randomize(); assert (rand_success);
`endif
aw_beat.ax_addr >>= $clog2(StrbWidth); // align address with data width
aw_beat.ax_addr <<= $clog2(StrbWidth);
aw_beat.ax_len = $urandom();
aw_beat.ax_size = $clog2(StrbWidth);
aw_beat.ax_burst = axi_pkg::BURST_INCR;
aw_beat.ax_addr >>= $clog2(StrbWidth); // align address with data width
aw_beat.ax_addr <<= $clog2(StrbWidth);
aw_beat.ax_len = $urandom();
aw_beat.ax_size = $clog2(StrbWidth);
aw_beat.ax_burst = axi_pkg::BURST_INCR;
// Make sure that the burst does not cross a 4KiB boundary.
if (axi_pkg::beat_addr(aw_beat.ax_addr, aw_beat.ax_size, aw_beat.ax_len, aw_beat.ax_burst, 0) >> 12 ==
axi_pkg::beat_addr(aw_beat.ax_addr, aw_beat.ax_size, aw_beat.ax_len, aw_beat.ax_burst, aw_beat.ax_len) >> 12) begin
break;
end
end
drv.send_aw(aw_beat);
// W beats
for (int unsigned i = 0; i <= aw_beat.ax_len; i++) begin
Expand All @@ -132,10 +139,17 @@ module tb_axi_sim_mem #(
drv.recv_b(b_beat);
assert(b_beat.b_resp == axi_pkg::RESP_OKAY);
// AR
ar_beat.ax_addr = aw_beat.ax_addr;
ar_beat.ax_len = aw_beat.ax_len;
ar_beat.ax_size = aw_beat.ax_size;
ar_beat.ax_burst = aw_beat.ax_burst;
forever begin
ar_beat.ax_addr = aw_beat.ax_addr;
ar_beat.ax_len = aw_beat.ax_len;
ar_beat.ax_size = aw_beat.ax_size;
ar_beat.ax_burst = aw_beat.ax_burst;
// Make sure that the burst does not cross a 4KiB boundary.
if (axi_pkg::beat_addr(ar_beat.ax_addr, ar_beat.ax_size, ar_beat.ax_len, ar_beat.ax_burst, 0) >> 12 ==
axi_pkg::beat_addr(ar_beat.ax_addr, ar_beat.ax_size, ar_beat.ax_len, ar_beat.ax_burst, ar_beat.ax_len) >> 12) begin
break;
end
end
drv.send_ar(ar_beat);
// R beats
for (int unsigned i = 0; i <= ar_beat.ax_len; i++) begin
Expand Down

0 comments on commit 556737b

Please sign in to comment.