Flesh out SPR-related FV properties.

diff --git a/src/soc/fu/spr/formal/proof_main_stage.py b/src/soc/fu/spr/formal/proof_main_stage.py
index b831bc63dfefe24618633b5634fb605e61ce62b9..730ffdbd033917ea29fc0aae2004b70b19f07ae6 100644 (file)
--- a/src/soc/fu/spr/formal/proof_main_stage.py
+++ b/src/soc/fu/spr/formal/proof_main_stage.py
@@ -6,7 +6,9 @@ Links:
 * https://bugs.libre-soc.org/show_bug.cgi?id=418
 """
 
-from nmigen import (Elaboratable, Module)
+import unittest
+
+from nmigen import (Elaboratable, Module, Signal, Cat)
 from nmigen.asserts import Assert, AnyConst, Assume
 from nmigen.cli import rtlil
 
@@ -15,8 +17,15 @@ from nmutil.formaltest import FHDLTestCase
 from soc.fu.spr.main_stage import SPRMainStage
 from soc.fu.spr.pipe_data import SPRPipeSpec
 from soc.fu.spr.spr_input_record import CompSPROpSubset
-from soc.decoder.power_enums import MicrOp
-import unittest
+
+from soc.decoder.power_decoder2 import decode_spr_num
+from soc.decoder.power_enums import MicrOp, SPR, XER_bits
+from soc.decoder.power_fields import DecodeFields
+from soc.decoder.power_fieldsn import SignalBitRange
+
+
+def xer_bit(name):
+    return 63-XER_bits[name]
 
 
 class Driver(Elaboratable):
@@ -40,17 +49,12 @@ class Driver(Elaboratable):
         pspec = SPRPipeSpec(id_wid=2)
         m.submodules.dut = dut = SPRMainStage(pspec)
 
-        # convenience variables
+        # frequently used aliases
         a = dut.i.a
         ca_in = dut.i.xer_ca[0]   # CA carry in
         ca32_in = dut.i.xer_ca[1] # CA32 carry in 32
         so_in = dut.i.xer_so      # SO sticky overflow
-
-        ca_o = dut.o.xer_ca.data[0]   # CA carry out
-        ca32_o = dut.o.xer_ca.data[1] # CA32 carry out32
-        ov_o = dut.o.xer_ov.data[0]   # OV overflow
-        ov32_o = dut.o.xer_ov.data[1] # OV32 overflow32
-        o = dut.o.o.data
+        o = dut.o.o
 
         # setup random inputs
         comb += [a.eq(AnyConst(64)),
@@ -68,12 +72,67 @@ class Driver(Elaboratable):
         comb += Assert(dut.o.ctx.op == dut.i.ctx.op )
         comb += Assert(dut.o.ctx.muxid == dut.i.ctx.muxid )
 
+        # MTSPR
+        fields = DecodeFields(SignalBitRange, [dut.i.ctx.op.insn])
+        fields.create_specs()
+        xfx = fields.FormXFX
+        spr = Signal(len(xfx.SPR))
+        comb += spr.eq(decode_spr_num(xfx.SPR))
+
+        with m.Switch(dut.i.ctx.op.insn_type):
+            with m.Case(MicrOp.OP_MTSPR):
+                with m.Switch(spr):
+                    with m.Case(SPR.CTR, SPR.LR, SPR.TAR, SPR.SRR0, SPR.SRR1):
+                        comb += [
+                            Assert(dut.o.fast1.data == a),
+                            Assert(dut.o.fast1.ok),
+
+                            # If a fast-path SPR is referenced, no other OKs
+                            # can fire.
+                            Assert(~dut.o.xer_so.ok),
+                            Assert(~dut.o.xer_ov.ok),
+                            Assert(~dut.o.xer_ca.ok),
+                        ]
+                    with m.Case(SPR.XER):
+                        comb += [
+                            Assert(dut.o.xer_so.data == a[xer_bit('SO')]),
+                            Assert(dut.o.xer_so.ok),
+                            Assert(dut.o.xer_ov.data == Cat(
+                                a[xer_bit('OV')], a[xer_bit('OV32')]
+                            )),
+                            Assert(dut.o.xer_ov.ok),
+                            Assert(dut.o.xer_ca.data == Cat(
+                                a[xer_bit('CA')], a[xer_bit('CA32')]
+                            )),
+                            Assert(dut.o.xer_ca.ok),
+
+                            # XER is not a fast-path SPR.
+                            Assert(~dut.o.fast1.ok),
+                        ]
+                    # slow SPRs TODO
+            with m.Case(MicrOp.OP_MFSPR):
+                comb += Assert(o.ok)
+                with m.Switch(spr):
+                    with m.Case(SPR.CTR, SPR.LR, SPR.TAR, SPR.SRR0, SPR.SRR1):
+                        comb += Assert(o.data == dut.i.fast1)
+                    with m.Case(SPR.XER):
+                        bits = {
+                            'SO': so_in,
+                            'OV': dut.i.xer_ov[0],
+                            'OV32': dut.i.xer_ov[1],
+                            'CA': ca_in,
+                            'CA32': ca32_in,
+                        }
+                        comb += [
+                            Assert(o[xer_bit(b)] == bits[b])
+                            for b in bits
+                        ]
+                    # slow SPRs TODO
+
         return m
 
 
 class SPRMainStageTestCase(FHDLTestCase):
-    #don't worry about it - tests are run manually anyway.  fail is fine.
-    #@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)