From 7d16e4157873bb5ad17c0bb9a0d646b15b0e2b1b Mon Sep 17 00:00:00 2001
From: Michael Nolan <mtnolan2640@gmail.com>
Date: Wed, 20 May 2020 14:32:29 -0400
Subject: [PATCH] Begin adding CR proof

---
 src/soc/fu/cr/formal/.gitignore          |  1 +
 src/soc/fu/cr/formal/proof_main_stage.py | 80 ++++++++++++++++++++++++
 src/soc/fu/cr/pipe_data.py               |  2 +-
 3 files changed, 82 insertions(+), 1 deletion(-)
 create mode 100644 src/soc/fu/cr/formal/.gitignore
 create mode 100644 src/soc/fu/cr/formal/proof_main_stage.py

diff --git a/src/soc/fu/cr/formal/.gitignore b/src/soc/fu/cr/formal/.gitignore
new file mode 100644
index 00000000..150f68c8
--- /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
index 00000000..caf45290
--- /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 2b240263..a955cdad 100644
--- 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
-        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__()
-- 
2.30.2