Change page crossing assertion, bus is always word-aligned

pulp-platform · Jul 17, 2024 · 545cfa1 · 545cfa1
1 parent 63ad5fb
commit 545cfa1
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 38 deletions.
diff --git 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
@@ -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
@@ -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