From: Samuel A. Falvo II <kc5tja@arrl.net>
Date: Tue, 14 Jul 2020 19:17:45 +0000 (-0700)
Subject: SPR: FV that should fail currently passes
X-Git-Tag: div_pipeline~41
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=769a8d5444f46cd093ff03645658198eaa8bd76d;p=soc.git

SPR: FV that should fail currently passes

WIP.  Cannot figure out why this is not failing.  Code review requested.
---

diff --git a/src/soc/fu/spr/formal/proof_main_stage.py b/src/soc/fu/spr/formal/proof_main_stage.py
new file mode 100644
index 00000000..0c7d5231
--- /dev/null
+++ b/src/soc/fu/spr/formal/proof_main_stage.py
@@ -0,0 +1,54 @@
+# Proof of correctness for SPR pipeline, main stage
+
+
+"""
+Links:
+* https://bugs.libre-soc.org/show_bug.cgi?id=418
+"""
+
+from os import getenv
+
+from unittest import skipUnless
+
+from nmigen import (Elaboratable, Module)
+from nmigen.asserts import Assert
+from nmigen.cli import rtlil
+
+from nmutil.formaltest import FHDLTestCase
+
+from soc.fu.spr.main_stage import SPRMainStage
+from soc.fu.spr.pipe_data import SPRPipeSpec
+
+
+class Driver(Elaboratable):
+    """
+    Defines a module to drive the device under test and assert properties
+    about its outputs.
+    """
+
+    def elaborate(self, platform):
+        m = Module()
+        comb = m.d.comb
+
+        dut = SPRMainStage(SPRPipeSpec(id_wid=2))
+
+        # Output context is the same as the input context.
+        comb += Assert(dut.o.ctx != dut.i.ctx)
+
+        return m
+
+
+class SPRMainStageTestCase(FHDLTestCase):
+    @skipUnless(getenv("FORMAL_SPR"), "Exercise SPR formal tests [WIP]")
+    def test_formal(self):
+        self.assertFormal(Driver(), mode="bmc", depth=100)
+        self.assertFormal(Driver(), mode="cover", depth=100)
+
+    def test_ilang(self):
+        vl = rtlil.convert(Driver(), ports=[])
+        with open("spr_main_stage.il", "w") as f:
+            f.write(vl)
+
+
+if __name__ == '__main__':
+    unittest.main()