Increase BMC depth for sorting network assertions

rtio/sed/output_network.py

@@ -119,12 +119,10 @@ class OutputNetwork(Elaboratable):
             f_past_valid = Signal()
             m.d.sync += f_past_valid.eq(1)
 
-            # TODO: assert outputs is a permutation of inputs
-
-            # Channel numbers for outputs are sorted in increasing order
+            # Valid nodes always come first in outputs
             with m.If(f_past_valid):
-                # TODO: Get the below (bogus) assertion to fail
-                m.d.comb += Assert(self.output[7].payload.channel == 0)
+                for i in range(lane_count - 1):
+                    m.d.comb += Assert(self.output[i].valid | ~self.output[i + 1].valid) # TODO: Figure out why this is failing
 
     def elaborate(self, platform):
         return self.m

rtio/test/sed/output_network.py

@@ -12,7 +12,7 @@ class OutputNetworkTestCase(FHDLTestCase):
         # Bounded model check
         self.assertFormal(
             OutputNetwork(16, 2, [("data", 32), ("channel", 3)], fv_mode=True),
-            mode="bmc", depth=10)
+            mode="bmc", depth=40)
         # TODO: unbounded proof
 
 OutputNetworkTestCase().verify()