AXI-Stream Formal Properties

.gitignore

@@ -0,0 +1,4 @@
+# Output folders from SymbiYosys (by task name convention)
+*_bmc/
+*_cover/
+*_prove/

CONTRIBUTING.md

@@ -9,5 +9,6 @@ Before submitting a pull request, please note the following points:
 
 * Before starting work, make sure an issue has been created first, and assign yourself (or leave some other marker in the issue) to indicate that you are working on the issue. This reduces duplication of work.
 * If you are submitting a bugfix, link the original issue(s) that you are aiming to fix. If you are adding new features, link the issue(s) in which the features were discussed.
+* Always use SymbiYosys tasks (even when there is only one), and choose task names that end with `_bmc`, `_cover`, or `_prove`. This allows the SymbiYosys output directories to be picked up by the `.gitignore` file.
 * Public-facing interfaces to a module follow the naming conventions of the standard they are based on, but names for internal items do not have to. An example of this is that AXI-Stream properties use the terms "master" and "slave" in their name (as these are the names used in the specification), but internal signals should use alternative labels such as "tx"/"send" and "rx"/"receive".
-* Pull requests are not merged until they have been reviewed and approved by at least one other person.
+* Pull requests into `main` are not merged until they have been reviewed and approved by at least one other person. Commits to `main` should only be used to update the status table or to update meta documents like `CONTRIBUTING.md` (though such changes should be discussed with the community first).

README.md

@@ -12,16 +12,17 @@ Key to emojis:
 
  * :x: : Item is not started
  * :heavy_minus_sign: : Item is in progress
- * :heavy_check_mark: : Item is completed
+ * :heavy_plus_sign: : Item is completed but has not been tested sufficiently
+ * :heavy_check_mark: : Item is completed and has been tested sufficiently
 
 All entries may contain an issue number tracking progress on the item.
 
 Item | Wishbone 4 Classic | Wishbone 4 Pipelined | AXI4-Stream | AXI4-Lite | AXI4
 ---- | ------------------ | -------------------- | ----------- | --------- | ----
-Formal Property Set (SVA) | :x: | :x: | :x: | :x: | :x:
-Formal Property Set (PSL) | :x: | :x: | :x: | :x: | :x:
+Formal Property Set (SVA) | :x: | :x: | :heavy_plus_sign: (#1, #3, #4) | :x: | :x:
+Formal Property Set (PSL) | :x: | :x: | :heavy_minus_sign: (#1, awaiting #3 merge) | :x: | :x:
 Bus Summary | :x: | :x: | :x: | :x: | :x:
-Example Cores (expand list later) | :x: | :x: | :x: | :x: | :x:
+Example Cores (expand list later) | :x: | :x: | :x: (#5) | :x: | :x:
 
 ## Bus Standards
 

property_sets/axi_stream/axi_stream_master_monitor.v

@@ -0,0 +1,202 @@
+`default_nettype none
+
+/*
+ * A set of formal properties for the master port of AXI-Stream.
+ * AXI4-Stream, Version 1.0, Issue A
+ */
+
+/*
+ * Section 2.1 Signal list
+ * Section 3.1 Default value signaling
+ * Notes on defaults for specific signals in port list below
+ */
+module axi_stream_master_monitor #(
+    parameter byte_width = 4,
+    parameter id_width = 0,
+    parameter dest_width = 0,
+    parameter user_width = 0,
+    // Section 3.1.5 Optional TDATA
+    // no TDATA -> no TSTRB (but TKEEP can still exist)
+    // TKEEP width when byte_width=0
+    parameter keep_width = 0,
+
+    // TODO: properties untested for multiclock environments
+    parameter USE_ASYNC_RESET = 1'b0,
+    // Section 2.2.1 Handshake process
+    // Master cannot wait on TREADY to signal TVALID
+    // Cycle count for TREADY to be kept low initially, after which TVALID should be high
+    // Set to 0 to disable this check
+    parameter MAX_DELAY_TREADY_NO_TVALID = 16
+) (
+    input wire aclk,
+    input wire aresetn,
+
+    input wire tvalid,
+    // Section 3.1.1 Optional TREADY
+    // Having a tready port is recommended
+`ifndef VERILATOR
+    input wire tready = 1'b1,
+`else
+    input wire tready,
+`endif
+
+    input wire [(8*byte_width-1):0] tdata,
+    // Section 3.1.2 Optional TKEEP and TSTRB
+    // TODO: fix optional value declarations
+    input wire [(byte_width-1):0] tstrb,// = tkeep,
+    input wire [(byte_width>0 ? (byte_width-1) : keep_width):0] tkeep,// = {(byte_width-1){1'b1}},
+
+    // Section 3.1.3 Optional TLAST
+    // Recommended default TLAST value situation-dependent
+    input wire tlast,
+
+    // Section 3.1.4 Optional TID, TDEST, and TUSER
+    // Signals omitted by setting widths to 0
+    input wire [(id_width-1):0] tid,
+    input wire [(dest_width-1):0] tdest,
+    input wire [(user_width-1):0] tuser
+
+    // TODO add output signals for byte counts, etc.
+);
+`define TX_ASSERT assert
+`define NOT_RESET_FOR_REGISTERED ($past(aresetn) && (!USE_ASYNC_RESET || aresetn))
+
+    reg past_valid = 1'b0;
+    always @(posedge aclk)
+        past_valid <= 1'b1;
+
+    reg not_in_reset;
+
+    /* 
+     * If in async mode, reset is registered by async flip flop
+     * If in sync mode, reset is registered by sync flip flop
+     *
+     * WARNING: Only use this in combinational blocks
+     * Use in registered blocks makes this incorrect by a clock cycle delay
+     * Use `NOT_RESET_FOR_REGISTERED for registered blocks
+     */
+    generate
+        if (USE_ASYNC_RESET)
+            always @(posedge aclk or negedge aresetn)
+            begin
+                if (!aresetn)
+                    not_in_reset <= 1'b0;
+                else
+                    not_in_reset <= aresetn;
+            end
+        else
+            always @(posedge aclk)
+            begin
+                not_in_reset <= aresetn;
+            end
+    endgenerate
+    // TODO reset signal generation is quite messy right now
+
+    // Section 2.2.1 Handshake process
+
+    // Once TVALID is asserted it must be held until TVALID && TREADY
+    always @(posedge aclk)
+    begin
+        // Write this as (TVALID falls implies previous data transfer or reset)
+        if (past_valid && $fell(tvalid))
+        begin
+            `TX_ASSERT($past(tvalid && tready) || !`NOT_RESET_FOR_REGISTERED);
+        end
+    end
+
+    // Master cannot wait on TREADY to signal TVALID
+    // Property below modified from @awygle's suggestion
+    generate
+    if (MAX_DELAY_TREADY_NO_TVALID < 4096 && MAX_DELAY_TREADY_NO_TVALID > 0)
+    begin
+        reg f_ever_ready = 1'b0;
+        reg [11:0] delay_counter = 0;
+        always @(posedge aclk)
+        begin
+            if (!aresetn)
+                f_ever_ready <= 1'b0;
+            else if (tready)
+                f_ever_ready <= 1'b1;
+        end
+        always @(posedge aclk)
+        begin
+            // Else if check to prevent weirdness with overflow
+            // 4096 cycles should be plenty enough though
+            if (!aresetn)
+                delay_counter <= 0;
+            else if (delay_counter < 12'hfff)
+                delay_counter <= delay_counter + 1;
+        end
+
+        always @(*)
+        begin
+            // Helper assert to justify lack of past_valid for below property
+            if (delay_counter > 0)
+                assert(past_valid);
+        end
+
+        // Check that TVALID has been raised even if TREADY has been held low
+        // In isolation, this checks the required property
+        // In a full system (where TREADY may be tied high) a false hypothesis allows the property to pass vacuously
+        // TODO: optional assumption for slave properties?
+        always @(*)
+        begin
+            if (delay_counter == MAX_DELAY_TREADY_NO_TVALID
+                    && !f_ever_ready && not_in_reset)
+                assert(tvalid);
+        end
+    end
+    else if (MAX_DELAY_TREADY_NO_TVALID != 0)
+        $error("MAX_DELAY_TREADY_NO_TVALID too large");
+    endgenerate
+
+    // When TVALID && !TREADY, data signals must be stable
+    always @(posedge aclk)
+    begin
+        if (past_valid && `NOT_RESET_FOR_REGISTERED && $past(tvalid && !tready))
+        begin
+            if (byte_width > 0)
+            begin
+                `TX_ASSERT($stable(tdata));
+                `TX_ASSERT($stable(tstrb));
+            end
+            if (byte_width > 0 || keep_width > 0)
+                `TX_ASSERT($stable(tkeep));
+
+            `TX_ASSERT($stable(tlast));
+
+            if (id_width > 0)
+                `TX_ASSERT($stable(tid));
+            if (dest_width > 0)
+                `TX_ASSERT($stable(tdest));
+            if (user_width > 0)
+                `TX_ASSERT($stable(tuser));
+        end
+    end
+
+    // Section 2.7.1 Clock
+    // Unlike regular AXI there is no requirement for no combinational paths
+
+    // Section 2.7.2 Reset
+    // "A master interface must only begin driving TVALID at a rising ACLK edge following a rising edge at which ARESETn is asserted HIGH."
+    // This timing is handled by the definition of not_in_reset above
+    always @(*)
+    begin
+        if (past_valid && !not_in_reset)
+        begin
+            `TX_ASSERT(!tvalid);
+        end
+    end
+
+    // Section 2.4.3 TKEEP and TSTRB combinations
+    // TSTRB can be asserted only if TKEEP is asserted
+    always @(*)
+    begin
+        if (tvalid)
+        begin
+            `TX_ASSERT(!(~tkeep & tstrb));
+        end
+    end
+endmodule
+`undef TX_ASSERT
+`undef NOT_RESET_FOR_REGISTERED

property_sets/axi_stream/axi_stream_slave_monitor.v

@@ -0,0 +1,153 @@
+`default_nettype none
+
+/*
+ * A set of formal properties for the slave port of AXI-Stream.
+ * AXI4-Stream, Version 1.0, Issue A
+ */
+
+/*
+ * Section 2.1 Signal list
+ * Section 3.1 Default value signaling
+ * Notes on defaults for specific signals in port list below
+ */
+module axi_stream_slave_monitor #(
+    parameter byte_width = 4,
+    parameter id_width = 0,
+    parameter dest_width = 0,
+    parameter user_width = 0,
+    // Section 3.1.5 Optional TDATA
+    // no TDATA -> no TSTRB (but TKEEP can still exist)
+    // TKEEP width when byte_width=0
+    parameter keep_width = 0,
+
+    // TODO: properties untested for multiclock environments
+    parameter USE_ASYNC_RESET = 1'b0
+) (
+    input wire aclk,
+    input wire aresetn,
+
+    input wire tvalid,
+    // Section 3.1.1 Optional TREADY
+    // Having a tready port is recommended
+`ifndef VERILATOR
+    input wire tready = 1'b1,
+`else
+    input wire tready,
+`endif
+
+    input wire [(8*byte_width-1):0] tdata,
+    // Section 3.1.2 Optional TKEEP and TSTRB
+    // TODO: fix optional value declarations
+    input wire [(byte_width-1):0] tstrb,// = tkeep,
+    input wire [(byte_width>0 ? (byte_width-1) : keep_width):0] tkeep,// = {(byte_width-1){1'b1}},
+
+    // Section 3.1.3 Optional TLAST
+    // Recommended default TLAST value situation-dependent
+    input wire tlast,
+
+    // Section 3.1.4 Optional TID, TDEST, and TUSER
+    // Signals omitted by setting widths to 0
+    input wire [(id_width-1):0] tid,
+    input wire [(dest_width-1):0] tdest,
+    input wire [(user_width-1):0] tuser
+
+    // TODO add output signals for byte counts, etc.
+);
+`define TX_ASSERT assume
+`define NOT_RESET_FOR_REGISTERED ($past(aresetn) && (!USE_ASYNC_RESET || aresetn))
+
+    reg past_valid = 1'b0;
+    always @(posedge aclk)
+        past_valid <= 1'b1;
+
+    reg not_in_reset;
+
+    /* 
+     * If in async mode, reset is registered by async flip flop
+     * If in sync mode, reset is registered by sync flip flop
+     *
+     * WARNING: Only use this in combinational blocks
+     * Use in registered blocks makes this incorrect by a clock cycle delay
+     * Use `NOT_RESET_FOR_REGISTERED for registered blocks
+     */
+    generate
+        if (USE_ASYNC_RESET)
+            always @(posedge aclk or negedge aresetn)
+            begin
+                if (!aresetn)
+                    not_in_reset <= 1'b0;
+                else
+                    not_in_reset <= aresetn;
+            end
+        else
+            always @(posedge aclk)
+            begin
+                not_in_reset <= aresetn;
+            end
+    endgenerate
+    // TODO reset signal generation is quite messy right now
+
+    // Section 2.2.1 Handshake process
+
+    // Once TVALID is asserted it must be held until TVALID && TREADY
+    always @(posedge aclk)
+    begin
+        // Write this as (TVALID falls implies previous data transfer or reset)
+        if (past_valid && $fell(tvalid))
+        begin
+            `TX_ASSERT($past(tvalid && tready) || !`NOT_RESET_FOR_REGISTERED);
+        end
+    end
+
+    // Slave can wait on TVALID to signal TREADY
+
+    // When TVALID && !TREADY, data signals must be stable
+    always @(posedge aclk)
+    begin
+        if (past_valid && `NOT_RESET_FOR_REGISTERED && $past(tvalid && !tready))
+        begin
+            if (byte_width > 0)
+            begin
+                `TX_ASSERT($stable(tdata));
+                `TX_ASSERT($stable(tstrb));
+            end
+            if (byte_width > 0 || keep_width > 0)
+                `TX_ASSERT($stable(tkeep));
+
+            `TX_ASSERT($stable(tlast));
+
+            if (id_width > 0)
+                `TX_ASSERT($stable(tid));
+            if (dest_width > 0)
+                `TX_ASSERT($stable(tdest));
+            if (user_width > 0)
+                `TX_ASSERT($stable(tuser));
+        end
+    end
+
+    // Section 2.7.1 Clock
+    // Unlike regular AXI there is no requirement for no combinational paths
+
+    // Section 2.7.2 Reset
+    // "A master interface must only begin driving TVALID at a rising ACLK edge following a rising edge at which ARESETn is asserted HIGH."
+    // This timing is handled by the definition of not_in_reset above
+    always @(*)
+    begin
+        if (past_valid && !not_in_reset)
+        begin
+            `TX_ASSERT(!tvalid);
+        end
+    end
+
+    // Section 2.4.3 TKEEP and TSTRB combinations
+    // TSTRB can be asserted only if TKEEP is asserted
+    always @(*)
+    begin
+        if (tvalid)
+        begin
+            `TX_ASSERT(!(~tkeep & tstrb));
+        end
+    end
+endmodule
+`undef TX_ASSERT
+`undef NOT_RESET_FOR_REGISTERED