diff --git a/src/axi_intf.sv b/src/axi_intf.sv index b464abfee..273e9baae 100644 --- a/src/axi_intf.sv +++ b/src/axi_intf.sv @@ -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 diff --git a/src/axi_test.sv b/src/axi_test.sv index f26557c9b..10caf777b 100644 --- a/src/axi_test.sv +++ b/src/axi_test.sv @@ -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 @@ -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 @@ -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 @@ -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 diff --git a/test/tb_axi_sim_mem.sv b/test/tb_axi_sim_mem.sv index af6f2a354..76ddb03f8 100644 --- a/test/tb_axi_sim_mem.sv +++ b/test/tb_axi_sim_mem.sv @@ -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 @@ -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