From 7b87d8012c5b4785ebde2c870e0b250f896e05de Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung <dl@m-labs.hk>
Date: Tue, 10 Nov 2020 13:00:18 +0800
Subject: [PATCH] Add unbounded proof for 2 lanes

---
 rtio/test/sed/output_network.py | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/rtio/test/sed/output_network.py b/rtio/test/sed/output_network.py
index 7703651..e7e5ae6 100644
--- a/rtio/test/sed/output_network.py
+++ b/rtio/test/sed/output_network.py
@@ -116,6 +116,10 @@ class OutputNetworkTestCase(FHDLTestCase):
         #     OutputNetworkSpec(8, 2, [("data", 32), ("channel", 3)]),
         #     mode="bmc", depth=40)
         # Unbounded proofs
+        # 2 lanes
+        self.assertFormal(
+            OutputNetworkSpec(2, 2, [("data", 32), ("channel", 3)]),
+            mode="prove", depth=latency(2))
         # 4 lanes
         self.assertFormal(
             OutputNetworkSpec(4, 2, [("data", 32), ("channel", 3)]),