From 036c91539b0ff74988cb49c17616177463aea061 Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung <dl@m-labs.hk>
Date: Fri, 16 Oct 2020 12:18:09 +0800
Subject: [PATCH] Start preparing assertions for sorting network

---
 rtio/sed/output_network.py      | 30 +++++++++++++++++++++++++++++-
 rtio/test/__init__.py           |  0
 rtio/test/sed/__init__.py       |  0
 rtio/test/sed/output_network.py | 18 ++++++++++++++++++
 4 files changed, 47 insertions(+), 1 deletion(-)
 create mode 100644 rtio/test/__init__.py
 create mode 100644 rtio/test/sed/__init__.py
 create mode 100644 rtio/test/sed/output_network.py

diff --git a/rtio/sed/output_network.py b/rtio/sed/output_network.py
index 9d5198c..9919815 100644
--- a/rtio/sed/output_network.py
+++ b/rtio/sed/output_network.py
@@ -1,5 +1,6 @@
 from nmigen import *
 from nmigen.utils import *
+from nmigen.asserts import *
 
 from rtio.sed import layouts
 
@@ -44,13 +45,23 @@ def cmp_wrap(a, b):
     return Mux((a[-2] == a[-1]) & (b[-2] == b[-1]) & (a[-1] != b[-1]), a[-1], a < b)
 
 class OutputNetwork(Elaboratable):
-    def __init__(self, lane_count, seqn_width, layout_payload):
+    def __init__(self, lane_count, seqn_width, layout_payload, *, fv_mode=False):
         m = Module()
         self.m = m
         self.input = [Record(layouts.output_network_node(seqn_width, layout_payload))
             for _ in range(lane_count)]
         self.output = None
 
+        if fv_mode:
+            # Model arbitrary inputs for network nodes
+            for i in range(lane_count):
+                m.d.comb += self.input[i].valid.eq(AnySeq(1))
+                m.d.comb += self.input[i].seqn.eq(AnySeq(seqn_width))
+                m.d.comb += self.input[i].replace_occured.eq(AnySeq(1))
+                m.d.comb += self.input[i].nondata_replace_occured.eq(AnySeq(1))
+                for field, width in layout_payload:
+                    m.d.comb += getattr(self.input[i].payload, field).eq(AnySeq(width))
+
         step_input = self.input
         for step in boms_steps_pairs(lane_count):
             step_output = []
@@ -98,5 +109,22 @@ class OutputNetwork(Elaboratable):
             self.output = step_output
             step_input = step_output
 
+        if fv_mode:
+            # Sanity checks
+            assert self.output is not None
+            assert len(self.input) == lane_count
+            assert len(self.output) == lane_count
+
+            # Indicator of when Past() is valid
+            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
+            with m.If(f_past_valid):
+                # TODO: Get the below (bogus) assertion to fail
+                m.d.comb += Assert(self.output[7].payload.channel == 0)
+
     def elaborate(self, platform):
         return self.m
diff --git a/rtio/test/__init__.py b/rtio/test/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/rtio/test/sed/__init__.py b/rtio/test/sed/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/rtio/test/sed/output_network.py b/rtio/test/sed/output_network.py
new file mode 100644
index 0000000..180d0fd
--- /dev/null
+++ b/rtio/test/sed/output_network.py
@@ -0,0 +1,18 @@
+from nmigen import *
+from nmigen.asserts import *
+from nmigen.test.utils import *
+from ...sed.output_network import *
+
+"""
+Verification tasks for OutputNetwork
+"""
+
+class OutputNetworkTestCase(FHDLTestCase):
+    def verify(self):
+        # Bounded model check
+        self.assertFormal(
+            OutputNetwork(16, 2, [("data", 32), ("channel", 3)], fv_mode=True),
+            mode="bmc", depth=10)
+        # TODO: unbounded proof
+
+OutputNetworkTestCase().verify()