Skip to content

Commit

Permalink
Change page crossing assertion, bus is always word-aligned
Browse files Browse the repository at this point in the history
  • Loading branch information
@micprog
micprog committed Jul 17, 2024
1 parent 63ad5fb commit 545cfa1
Show file tree
Hide file tree
Showing 3 changed files with 22 additions and 38 deletions.
24 changes: 10 additions & 14 deletions src/axi_intf.sv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -249,20 +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 highest byte in the last beat of a burst must be
// on the same 4 KiB page as the address of the lowest byte in the first beat of a burst.
assert property (@(posedge clk_i) aw_valid |->
axi_pkg::beat_addr(aw_addr, aw_size, aw_len, aw_burst, 0) >> 12 == (
axi_pkg::beat_addr(aw_addr, aw_size, aw_len, aw_burst, aw_len)
+ axi_pkg::beat_upper_byte(aw_addr, aw_size, aw_len, aw_burst, AXI_STRB_WIDTH, aw_len)
) >> 12
) else $error("AW burst crossing 4 KiB page boundary detected, which is illegal!");
assert property (@(posedge clk_i) ar_valid |->
axi_pkg::beat_addr(ar_addr, ar_size, ar_len, ar_burst, 0) >> 12 == (
axi_pkg::beat_addr(ar_addr, ar_size, ar_len, ar_burst, ar_len)
+ axi_pkg::beat_upper_byte(ar_addr, ar_size, ar_len, ar_burst, AXI_STRB_WIDTH, ar_len)
) >> 12
) else $error("AR burst crossing 4 KiB page boundary detected, which is illegal!");
// 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
24 changes: 8 additions & 16 deletions src/axi_test.sv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -905,10 +905,8 @@ package axi_test;
addr + len <= mem_region.addr_end;
}; assert(rand_success);

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)
+ axi_pkg::beat_upper_byte(addr, ax_beat.ax_size, ax_beat.ax_len, ax_beat.ax_burst, AXI_STRB_WIDTH, ax_beat.ax_len)
) >> 12) begin
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
Expand All @@ -934,10 +932,8 @@ package axi_test;
addr + ((len + 1) << size) <= mem_region.addr_end;
}; assert(rand_success);

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)
+ axi_pkg::beat_upper_byte(addr, ax_beat.ax_size, ax_beat.ax_len, ax_beat.ax_burst, AXI_STRB_WIDTH, ax_beat.ax_len)
) >> 12) begin
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
Expand Down Expand Up @@ -1021,10 +1017,8 @@ package axi_test;
beat.ax_burst = axi_pkg::BURST_INCR;
end
// 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)
+ axi_pkg::beat_upper_byte(beat.ax_addr, beat.ax_size, beat.ax_len, beat.ax_burst, AXI_STRB_WIDTH, beat.ax_len)
) >> 12) begin
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
end
Expand Down Expand Up @@ -1059,10 +1053,8 @@ package axi_test;
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)
+ axi_pkg::beat_upper_byte(ar_beat.ax_addr, ar_beat.ax_size, ar_beat.ax_len, ar_beat.ax_burst, AXI_STRB_WIDTH, ar_beat.ax_len)
) >> 12) begin
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
Expand Down
12 changes: 4 additions & 8 deletions test/tb_axi_sim_mem.sv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -113,10 +113,8 @@ module tb_axi_sim_mem #(
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)
+ axi_pkg::beat_upper_byte(aw_beat.ax_addr, aw_beat.ax_size, aw_beat.ax_len, aw_beat.ax_burst, StrbWidth, aw_beat.ax_len)
) >> 12) begin
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
Expand Down Expand Up @@ -147,10 +145,8 @@ module tb_axi_sim_mem #(
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)
+ axi_pkg::beat_upper_byte(ar_beat.ax_addr, ar_beat.ax_size, ar_beat.ax_len, ar_beat.ax_burst, StrbWidth, ar_beat.ax_len)
) >> 12) begin
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
Expand Down

0 comments on commit 545cfa1

Please sign in to comment.