AXI_BUS_DV: Assert burst on one page

CHANGELOG.md

@@ -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

src/axi_intf.sv

@@ -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
 

src/axi_test.sv

@@ -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
@@ -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
@@ -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
 

test/tb_axi_sim_mem.sv

@@ -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
@@ -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