Begin adding CR proof

diff --git a/src/soc/fu/cr/formal/.gitignore b/src/soc/fu/cr/formal/.gitignore
new file mode 100644 (file)
index 0000000..150f68c
--- /dev/null
+++ b/src/soc/fu/cr/formal/.gitignore
@@ -0,0 +1 @@
+*/*

diff --git a/src/soc/fu/cr/formal/proof_main_stage.py b/src/soc/fu/cr/formal/proof_main_stage.py
new file mode 100644 (file)
index 0000000..caf4529
--- /dev/null
+++ b/src/soc/fu/cr/formal/proof_main_stage.py
@@ -0,0 +1,80 @@
+# Proof of correctness for partitioned equal signal combiner
+# Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
+
+from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
+                    signed, Array)
+from nmigen.asserts import Assert, AnyConst, Assume, Cover
+from nmigen.test.utils import FHDLTestCase
+from nmigen.cli import rtlil
+
+from soc.fu.cr.main_stage import CRMainStage
+from soc.fu.alu.pipe_data import ALUPipeSpec
+from soc.fu.alu.alu_input_record import CompALUOpSubset
+from soc.decoder.power_enums import InternalOp
+import unittest
+
+
+# This defines a module to drive the device under test and assert
+# properties about its outputs
+class Driver(Elaboratable):
+    def __init__(self):
+        # inputs and outputs
+        pass
+
+    def elaborate(self, platform):
+        m = Module()
+        comb = m.d.comb
+
+        rec = CompALUOpSubset()
+        recwidth = 0
+        # Setup random inputs for dut.op
+        for p in rec.ports():
+            width = p.width
+            recwidth += width
+            comb += p.eq(AnyConst(width))
+
+        pspec = ALUPipeSpec(id_wid=2, op_wid=recwidth)
+        m.submodules.dut = dut = CRMainStage(pspec)
+
+        a = dut.i.a
+        cr = dut.i.cr
+        cr_o = dut.o.cr
+
+        # setup random inputs
+        comb += [a.eq(AnyConst(64)),
+                 cr.eq(AnyConst(64))]
+
+        comb += dut.i.ctx.op.eq(rec)
+
+        # Assert that op gets copied from the input to output
+        for rec_sig in rec.ports():
+            name = rec_sig.name
+            dut_sig = getattr(dut.o.ctx.op, name)
+            comb += Assert(dut_sig == rec_sig)
+
+        cr_arr = Array([cr[i] for i in range(32)])
+        cr_o_arr = Array([cr[i] for i in range(32)])
+
+        with m.Switch(rec.insn_type):
+            with m.Case(InternalOp.OP_MTCRF):
+                xfx_fields = dut.fields.FormXFX
+                FXM = xfx_fields.FXM[0:-1]
+                for i in range(8):
+                    with m.If(FXM[i]):
+                        comb += Assert(cr_o[4*i:4*i+4] == a[4*i:4*i+4])
+        return m
+
+
+class CRTestCase(FHDLTestCase):
+    def test_formal(self):
+        module = Driver()
+        self.assertFormal(module, mode="bmc", depth=2)
+    def test_ilang(self):
+        dut = Driver()
+        vl = rtlil.convert(dut, ports=[])
+        with open("cr_main_stage.il", "w") as f:
+            f.write(vl)
+
+
+if __name__ == '__main__':
+    unittest.main()

diff --git a/src/soc/fu/cr/pipe_data.py b/src/soc/fu/cr/pipe_data.py
index 2b240263ab0cc9badbbeaa4e180cfba382c7bdb2..a955cdad0ad1faacff2ba9eeb8866e62e47628c3 100644 (file)
--- a/src/soc/fu/cr/pipe_data.py
+++ b/src/soc/fu/cr/pipe_data.py
@@ -27,7 +27,7 @@ class CROutputData(IntegerData):
     def __init__(self, pspec):
         super().__init__(pspec)
         self.o = Signal(64, reset_less=True) # RA
     def __init__(self, pspec):
         super().__init__(pspec)
         self.o = Signal(64, reset_less=True) # RA

-        self.cr = Signal(32, reset_less=True) # CR in
+        self.cr = Signal(32, reset_less=True, name="cr_out") # CR in

 
     def __iter__(self):
         yield from super().__iter__()
 
     def __iter__(self):
         yield from super().__iter__()