New handshake assertions; i/f X checks conditional upon valid signals

chipsalliance · Jul 25, 2024 · d467e3a · d467e3a
1 parent d4582ae
commit d467e3a
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 23 deletions.
diff --git a/src/axi/rtl/axi_sub_rd.sv b/src/axi/rtl/axi_sub_rd.sv
@@ -344,21 +344,25 @@ module axi_sub_rd import axi_pkg::*; #(
     // --------------------------------------- //
     // Formal Properties                       //
     // --------------------------------------- //
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARADDR , s_axi_if.araddr , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARBURST, s_axi_if.arburst, clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARSIZE , s_axi_if.arsize , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARLEN  , s_axi_if.arlen  , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARUSER , s_axi_if.aruser , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARID   , s_axi_if.arid   , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARLOCK , s_axi_if.arlock , clk, !rst_n)
     `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARVALID, s_axi_if.arvalid, clk, !rst_n)
     `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARREADY, s_axi_if.arready, clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RDATA  , s_axi_if.rdata  , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RRESP  , s_axi_if.rresp  , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RID    , s_axi_if.rid    , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RLAST  , s_axi_if.rlast  , clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARADDR , (s_axi_if.arvalid ? s_axi_if.araddr  : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARBURST, (s_axi_if.arvalid ? s_axi_if.arburst : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARSIZE , (s_axi_if.arvalid ? s_axi_if.arsize  : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARLEN  , (s_axi_if.arvalid ? s_axi_if.arlen   : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARUSER , (s_axi_if.arvalid ? s_axi_if.aruser  : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARID   , (s_axi_if.arvalid ? s_axi_if.arid    : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARLOCK , (s_axi_if.arvalid ? s_axi_if.arlock  : '0), clk, !rst_n)
     `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RVALID , s_axi_if.rvalid , clk, !rst_n)
     `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RREADY , s_axi_if.rready , clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RDATA  , (s_axi_if.rvalid ? s_axi_if.rdata : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RRESP  , (s_axi_if.rvalid ? s_axi_if.rresp : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RID    , (s_axi_if.rvalid ? s_axi_if.rid   : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RLAST  , (s_axi_if.rvalid ? s_axi_if.rlast : '0), clk, !rst_n)
+
+    // Handshake rules
+    `CALIPTRA_ASSERT      (AXI_SUB_AR_HSHAKE_ERR, s_axi_if.arvalid && !s_axi_if.arready => s_axi_if.arvalid, clk, !rst_n)
+    `CALIPTRA_ASSERT      (AXI_SUB_R_HSHAKE_ERR,  s_axi_if.rvalid  && !s_axi_if.rready  => s_axi_if.rvalid,  clk, !rst_n)
 
     `CALIPTRA_ASSERT_NEVER(ERR_AXI_RD_DROP  , dp_rvalid[0] && !dp_rready[0], clk, !rst_n)
     `CALIPTRA_ASSERT_NEVER(ERR_AXI_RD_X     , dp_rvalid[0] && $isunknown({dp_rdata[0],dp_xfer_ctx[0]}), clk, !rst_n)

diff --git a/src/axi/rtl/axi_sub_wr.sv b/src/axi/rtl/axi_sub_wr.sv
@@ -316,24 +316,29 @@ module axi_sub_wr import axi_pkg::*; #(
     // --------------------------------------- //
     // Formal Properties                       //
     // --------------------------------------- //
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWADDR , s_axi_if.awaddr , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWBURST, s_axi_if.awburst, clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWSIZE , s_axi_if.awsize , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWLEN  , s_axi_if.awlen  , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWUSER , s_axi_if.awuser , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWID   , s_axi_if.awid   , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWLOCK , s_axi_if.awlock , clk, !rst_n)
     `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWVALID, s_axi_if.awvalid, clk, !rst_n)
     `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWREADY, s_axi_if.awready, clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_WDATA  , s_axi_if.wdata  , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_WSTRB  , s_axi_if.wstrb  , clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWADDR , (s_axi_if.awvalid ? s_axi_if.awaddr  : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWBURST, (s_axi_if.awvalid ? s_axi_if.awburst : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWSIZE , (s_axi_if.awvalid ? s_axi_if.awsize  : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWLEN  , (s_axi_if.awvalid ? s_axi_if.awlen   : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWUSER , (s_axi_if.awvalid ? s_axi_if.awuser  : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWID   , (s_axi_if.awvalid ? s_axi_if.awid    : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_AWLOCK , (s_axi_if.awvalid ? s_axi_if.awlock  : '0), clk, !rst_n)
     `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_WVALID , s_axi_if.wvalid , clk, !rst_n)
     `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_WREADY , s_axi_if.wready , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_WLAST  , s_axi_if.wlast  , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_BRESP  , s_axi_if.bresp  , clk, !rst_n)
-    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_BID    , s_axi_if.bid    , clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_WDATA  , (s_axi_if.wvalid ? s_axi_if.wdata : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_WSTRB  , (s_axi_if.wvalid ? s_axi_if.wstrb : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_WLAST  , (s_axi_if.wvalid ? s_axi_if.wlast : '0), clk, !rst_n)
     `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_BVALID , s_axi_if.bvalid , clk, !rst_n)
     `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_BREADY , s_axi_if.bready , clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_BRESP  , (s_axi_if.bvalid ? s_axi_if.bresp : '0), clk, !rst_n)
+    `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_BID    , (s_axi_if.bvalid ? s_axi_if.bid   : '0), clk, !rst_n)
+
+    // Handshake rules
+    `CALIPTRA_ASSERT      (AXI_SUB_AW_HSHAKE_ERR, s_axi_if.awvalid && !s_axi_if.awready => s_axi_if.awvalid, clk, !rst_n)
+    `CALIPTRA_ASSERT      (AXI_SUB_W_HSHAKE_ERR,  s_axi_if.wvalid  && !s_axi_if.wready  => s_axi_if.wvalid,  clk, !rst_n)
+    `CALIPTRA_ASSERT      (AXI_SUB_B_HSHAKE_ERR,  s_axi_if.bvalid  && !s_axi_if.bready  => s_axi_if.bvalid,  clk, !rst_n)
 
     // Exclusive access rules:
     //   - Must have an address that is aligned to burst byte count