add running instructions

[soc.git] / src / soc / fu / shift_rot / formal / proof_main_stage.py

diff --git a/src/soc/fu/shift_rot/formal/proof_main_stage.py b/src/soc/fu/shift_rot/formal/proof_main_stage.py
index 8e2952fc6fd015bf1b52ce662c3bb2f816fb9a88..7ef3258fabb04fa254b65df395b1c5945e4c3d46 100644 (file)
--- a/src/soc/fu/shift_rot/formal/proof_main_stage.py
+++ b/src/soc/fu/shift_rot/formal/proof_main_stage.py
@@ -3,6 +3,13 @@
 """
 Links:
 * https://bugs.libre-soc.org/show_bug.cgi?id=340
+
+run tests with:
+pip install pytest
+pip install pytest-xdist
+pytest -n auto src/soc/fu/shift_rot/formal/proof_main_stage.py
+because that tells pytest to run the tests in parallel, it will take a few
+minutes instead of an hour.
 """
 
 import unittest
@@ -114,7 +121,7 @@ def rotl32(v, amt):
 # properties about its outputs
 class Driver(Elaboratable):
     def __init__(self, which):
-        assert isinstance(which, TstOp)
+        assert isinstance(which, TstOp) or which is None
         self.which = which
 
     def elaborate(self, platform):
@@ -152,11 +159,17 @@ class Driver(Elaboratable):
         comb += Assert(dut.o.ctx.op == dut.i.ctx.op)
         comb += Assert(dut.o.ctx.muxid == dut.i.ctx.muxid)
 
-        # we're only checking a particular operation:
-        comb += Assume(dut.i.ctx.op.insn_type == self.which.op)
+        if self.which is None:
+            for i in TstOp:
+                comb += Assume(dut.i.ctx.op.insn_type != i.op)
+            comb += Assert(~dut.o.o.ok)
+        else:
+            # we're only checking a particular operation:
+            comb += Assume(dut.i.ctx.op.insn_type == self.which.op)
+            comb += Assert(dut.o.o.ok)
 
-        # dispatch to check fn for each op
-        getattr(self, f"_check_{self.which.name.lower()}")(m, dut)
+            # dispatch to check fn for each op
+            getattr(self, f"_check_{self.which.name.lower()}")(m, dut)
 
         return m
 
@@ -328,6 +341,9 @@ class ALUTestCase(FHDLTestCase):
         self.assertFormal(module, mode="bmc", depth=2)
         self.assertFormal(module, mode="cover", depth=2)
 
+    def test_none(self):
+        self.run_it(None)
+
     def test_shl(self):
         self.run_it(TstOp.SHL)