First FV property for trap unit

diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py
new file mode 100644 (file)
index 0000000..89a0ebb
--- /dev/null
+++ b/src/soc/fu/trap/formal/proof_main_stage.py
@@ -0,0 +1,52 @@
+# Proof of correctness for trap pipeline, main stage
+
+
+"""
+Links:
+* https://bugs.libre-soc.org/show_bug.cgi?id=421
+"""
+
+
+import unittest
+
+from nmigen import Elaboratable, Module
+from nmigen.asserts import Assert, AnyConst
+from nmigen.cli import rtlil
+
+from nmutil.formaltest import FHDLTestCase
+
+from soc.fu.trap.main_stage import TrapMainStage
+from soc.fu.trap.pipe_data import TrapPipeSpec
+
+
+class Driver(Elaboratable):
+    """
+    """
+
+    def elaborate(self, platform):
+        m = Module()
+        comb = m.d.comb
+
+        pspec = TrapPipeSpec(id_wid=2)
+
+        m.submodules.dut = dut = TrapMainStage(pspec)
+
+        comb += dut.i.ctx.matches(dut.o.ctx)
+
+        return m
+
+
+class TrapMainStageTestCase(FHDLTestCase):
+    def test_formal(self):
+        self.assertFormal(Driver(), mode="bmc", depth=10)
+        self.assertFormal(Driver(), mode="cover", depth=10)
+
+    def test_ilang(self):
+        vl = rtlil.convert(Driver(), ports=[])
+        with open("trap_main_stage.il", "w") as f:
+            f.write(vl)
+
+
+if __name__ == '__main__':
+    unittest.main()
+