From 2d801d1aef3aebceacee1426fdbeb714962aded4 Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung <dl@m-labs.hk>
Date: Mon, 9 Nov 2020 11:47:47 +0800
Subject: [PATCH] Add unbounded proof for output network with 4 lanes

---
 README.md                       |  2 +-
 rtio/test/sed/output_network.py | 19 ++++++++++++++-----
 2 files changed, 15 insertions(+), 6 deletions(-)

diff --git a/README.md b/README.md
index 7dd3b92..1050166 100644
--- a/README.md
+++ b/README.md
@@ -26,7 +26,7 @@ $ python -m rtio.test.sed.output_network
 - - [x] `rtio.sed.layouts`
 - - [x] `rtio.sed.output_network`
 - - [x] `rtio.sed.output_driver`
-- [ ] Add suitable assertions for verification (BMC / unbounded proof?)
+- [ ] Add suitable assertions for verification
 - - [ ] `rtio.cri` (`Interface` and `CRIDecoder` only)
 - - [x] `rtio.sed.output_network` - Sorting network (high priority)
 - - [ ] `rtio.sed.output_driver`
diff --git a/rtio/test/sed/output_network.py b/rtio/test/sed/output_network.py
index 0139598..57d2327 100644
--- a/rtio/test/sed/output_network.py
+++ b/rtio/test/sed/output_network.py
@@ -8,9 +8,13 @@ Verification tasks for OutputNetwork
 """
 
 class OutputNetworkSpec(Elaboratable):
+    def __init__(self, lane_count, seqn_width, layout_payload):
+        self.lane_count = lane_count
+        self.seqn_width = seqn_width
+        self.layout_payload = layout_payload
     def elaborate(self, platform):
         m = Module()
-        m.submodules.output_network = output_network = OutputNetwork(4, 2, [("data", 32), ("channel", 3)])
+        m.submodules.output_network = output_network = OutputNetwork(self.lane_count, self.seqn_width, self.layout_payload)
 
         # Model arbitrary inputs for network nodes
         for i in range(output_network.lane_count):
@@ -130,10 +134,15 @@ class OutputNetworkSpec(Elaboratable):
 
 class OutputNetworkTestCase(FHDLTestCase):
     def verify(self):
-        # Bounded model check
+        # Bounded proofs
+        # 8 lanes (failing)
+        # self.assertFormal(
+        #     OutputNetworkSpec(8, 2, [("data", 32), ("channel", 3)]),
+        #     mode="bmc", depth=40)
+        # Unbounded proofs
+        # 4 lanes
         self.assertFormal(
-            OutputNetworkSpec(),
-            mode="bmc", depth=40)
-        # TODO: unbounded proof
+            OutputNetworkSpec(4, 2, [("data", 32), ("channel", 3)]),
+            mode="prove", depth=latency(4))
 
 OutputNetworkTestCase().verify()