Added assertions to all interfaces that interact with the simulation

Author: JonasDann

hw/hdl/pkg/assert_macros.svh

@@ -0,0 +1,44 @@
+/**
+ * This file is part of the Coyote <https://github.com/fpgasystems/Coyote>
+ *
+ * MIT Licence
+ * Copyright (c) 2021-2025, Systems Group, ETH Zurich
+ * All rights reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+`ifndef COYOTE_ASSERT_MACROS_SVH
+`define COYOTE_ASSERT_MACROS_SVH
+
+`define STRINGIFY(x) $sformatf("%0s", `"x`")
+
+`define ASSERT_NOT_UNDEFINED(sig) \
+assert property (@(posedge aclk) disable iff (!aresetn) \
+    !$isunknown(sig)) \
+else $fatal(1, "Signal %s needs to not be undefined!", `STRINGIFY(sig));
+
+`define ASSERT_STABLE(sig, sig_valid, sig_ready) \
+assert property (@(posedge aclk) disable iff (!aresetn) \
+    (sig_valid && !sig_ready && $past(aresetn)) |=> $stable(sig)) \
+else $fatal(1, "Signal %s needs to be stable while valid && !ready (old = 0b%0b, new = 0b%0b)!", `STRINGIFY(sig), $past(sig), sig);
+
+`define ASSERT_SIGNAL_STABLE(sig) `ASSERT_STABLE(sig, tvalid, tready)
+
+`endif

hw/hdl/pkg/axi_intf.sv

@@ -31,6 +31,8 @@
 
 import lynxTypes::*;
 
+`include "libstf_macros.svh"
+
 // ----------------------------------------------------------------------------
 // AXI4
 // ----------------------------------------------------------------------------
@@ -325,6 +327,35 @@ clocking cbs @(posedge aclk);
     output awready, arready, rresp, rdata, rvalid, wready, bresp, bvalid;
 endclocking
 
+// Assertions
+`ASSERT_STABLE(awaddr, awvalid, awready);
+`ASSERT_STABLE(awprot, awvalid, awready);
+`ASSERT_STABLE(awqos, awvalid, awready);
+`ASSERT_STABLE(awregion, awvalid, awready);
+`ASSERT_NOT_UNDEFINED(awvalid);
+`ASSERT_NOT_UNDEFINED(awready);
+
+`ASSERT_STABLE(araddr, arvalid, arready);
+`ASSERT_STABLE(arprot, arvalid, arready);
+`ASSERT_STABLE(arqos, arvalid, arready);
+`ASSERT_STABLE(arregion, arvalid, arready);
+`ASSERT_NOT_UNDEFINED(arvalid);
+`ASSERT_NOT_UNDEFINED(arready);
+
+`ASSERT_STABLE(wdata, wvalid, wready);
+`ASSERT_STABLE(wstrb, wvalid, wready);
+`ASSERT_NOT_UNDEFINED(wvalid);
+`ASSERT_NOT_UNDEFINED(wready);
+
+`ASSERT_STABLE(rresp, rvalid, rready);
+`ASSERT_STABLE(rdata, rvalid, rready);
+`ASSERT_NOT_UNDEFINED(rvalid);
+`ASSERT_NOT_UNDEFINED(rready);
+
+`ASSERT_STABLE(bresp, bvalid, bready);
+`ASSERT_NOT_UNDEFINED(bvalid);
+`ASSERT_NOT_UNDEFINED(bready);
+
 endinterface
 
 // ----------------------------------------------------------------------------
@@ -373,6 +404,13 @@ modport s (
     output tready
 );
 
+// Assertions
+`ASSERT_SIGNAL_STABLE(tdata);
+`ASSERT_SIGNAL_STABLE(tkeep);
+`ASSERT_SIGNAL_STABLE(tlast);
+`ASSERT_NOT_UNDEFINED(tvalid);
+`ASSERT_NOT_UNDEFINED(tready);
+
 endinterface
 
 
@@ -439,6 +477,14 @@ clocking cbs @(posedge aclk);
     output tready;
 endclocking
 
+// Assertions
+`ASSERT_SIGNAL_STABLE(tdata);
+`ASSERT_SIGNAL_STABLE(tid);
+`ASSERT_SIGNAL_STABLE(tkeep);
+`ASSERT_SIGNAL_STABLE(tlast);
+`ASSERT_NOT_UNDEFINED(tvalid);
+`ASSERT_NOT_UNDEFINED(tready);
+
 endinterface
 
 // ----------------------------------------------------------------------------

hw/hdl/pkg/lynx_intf.sv

@@ -31,6 +31,8 @@
 
 import lynxTypes::*;
 
+`include "libstf_macros.svh"
+
 // ----------------------------------------------------------------------------
 // Generic meta interface
 // ----------------------------------------------------------------------------
@@ -81,6 +83,11 @@ clocking cbs @(posedge aclk);
     output ready;
 endclocking
 
+// Assertions
+`ASSERT_STABLE(data, valid, ready);
+`ASSERT_NOT_UNDEFINED(valid);
+`ASSERT_NOT_UNDEFINED(ready);
+
 endinterface
 
 // ----------------------------------------------------------------------------