From 96e7a795020ad8cb99d41709244f48e9f2e992fc Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung <dl@m-labs.hk>
Date: Tue, 10 Nov 2020 12:53:30 +0800
Subject: [PATCH] Remove assertions involving invalid inputs

---
 rtio/test/sed/output_network.py | 48 +++++++++------------------------
 1 file changed, 12 insertions(+), 36 deletions(-)

diff --git a/rtio/test/sed/output_network.py b/rtio/test/sed/output_network.py
index 57d2327..7703651 100644
--- a/rtio/test/sed/output_network.py
+++ b/rtio/test/sed/output_network.py
@@ -35,10 +35,10 @@ class OutputNetworkSpec(Elaboratable):
         m.d.comb += f_output_valid.eq(counter == network_latency)
         
         with m.If(f_output_valid):
-            replacement_occurred = Signal()
+            valid_replacement_occurred = Signal()
             for node in output_network.output:
-                with m.If(node.replace_occured):
-                    m.d.comb += replacement_occurred.eq(1)
+                with m.If(node.valid & node.replace_occured):
+                    m.d.comb += valid_replacement_occurred.eq(1)
             valid_channels_unique = Signal(reset=1)
             for node1 in range(len(output_network.input)):
                 with m.If(Past(output_network.input[node1].valid, clocks=network_latency)):
@@ -48,21 +48,11 @@ class OutputNetworkSpec(Elaboratable):
                             k2 = Past(output_network.input[node2].payload.channel, clocks=network_latency)
                             with m.If(k1 == k2):
                                 m.d.comb += valid_channels_unique.eq(0)
-            invalid_channels_unique = Signal(reset=1)
-            for node1 in range(len(output_network.input)):
-                with m.If(~Past(output_network.input[node1].valid, clocks=network_latency)):
-                    for node2 in range(node1):
-                        with m.If(~Past(output_network.input[node2].valid, clocks=network_latency)):
-                            k1 = Past(output_network.input[node1].payload.channel, clocks=network_latency)
-                            k2 = Past(output_network.input[node2].payload.channel, clocks=network_latency)
-                            with m.If(k1 == k2):
-                                m.d.comb += invalid_channels_unique.eq(0)
-            # If there are no replacements then:
-            # - Input channel numbers are unique among (in)valid nodes
-            # - All inputs make it through the sorting network unmodified
-            with m.If(~replacement_occurred):
+            # Among the valid outputs, if there are no replacements then:
+            # - Channel numbers are unique among valid inputs
+            # - All valid inputs make it through the sorting network unmodified
+            with m.If(~valid_replacement_occurred):
                 m.d.comb += Assert(valid_channels_unique)
-                m.d.comb += Assert(invalid_channels_unique)
                 for input_node in output_network.input:
                     appeared = Signal()
                     for output_node in output_network.output:
@@ -80,18 +70,16 @@ class OutputNetworkSpec(Elaboratable):
                                 m.d.comb += match.eq(0)
                         with m.If(match):
                             m.d.comb += appeared.eq(1)
-                    m.d.comb += Assert(appeared)
-            # Otherwise, if there are replacements:
-            # - There is a channel number collision among the valid or invalid
-            #   nodes
+                    with m.If(Past(input_node.valid, clocks=network_latency)):
+                        m.d.comb += Assert(appeared)
+            # Otherwise:
+            # - There is a channel number collision among the valid inputs
             # - All channel numbers in valid inputs appear exactly once as a
             #   valid output
             # - All valid outputs correspond to a valid input modulo accounting
             #   information
-            # - Channel numbers in invalid inputs not appearing in valid inputs
-            #   as well never appear as a valid output
             with m.Else():
-                m.d.comb += Assert(~valid_channels_unique | ~invalid_channels_unique)
+                m.d.comb += Assert(~valid_channels_unique)
                 for input_node in output_network.input:
                     input_channel_valid_once = Const(0)
                     for node1 in range(len(output_network.output)):
@@ -117,18 +105,6 @@ class OutputNetworkSpec(Elaboratable):
                             with m.If(match):
                                 m.d.comb += found_input.eq(1)
                         m.d.comb += Assert(found_input)
-                for node1 in output_network.input:
-                    with m.If(~Past(node1.valid, clocks=network_latency)):
-                        has_valid_input = Signal()
-                        for node2 in output_network.input:
-                            with m.If(Past(node2.valid, clocks=network_latency) & (Past(node1.payload.channel, clocks=network_latency) == Past(node2.payload.channel, clocks=network_latency))):
-                                m.d.comb += has_valid_input.eq(1)
-                        with m.If(~has_valid_input):
-                            has_valid_output = Signal()
-                            for output_node in output_network.output:
-                                with m.If(output_node.valid & (output_node.payload.channel == Past(node1.payload.channel, clocks=network_latency))):
-                                    m.d.comb += has_valid_output.eq(1)
-                            m.d.comb += Assert(~has_valid_output)
 
         return m