From 26dfc9d27388c99f147d8c55e6c933fa91add592 Mon Sep 17 00:00:00 2001
From: Michael Nolan <mtnolan2640@gmail.com>
Date: Fri, 8 May 2020 11:03:34 -0400
Subject: [PATCH] Begin adding input stage of alu

---
 src/soc/alu/formal/.gitignore           |  1 +
 src/soc/alu/formal/proof_input_stage.py | 59 +++++++++++++++++++++++++
 src/soc/alu/input_stage.py              | 23 ++++++++++
 3 files changed, 83 insertions(+)
 create mode 100644 src/soc/alu/formal/.gitignore
 create mode 100644 src/soc/alu/formal/proof_input_stage.py
 create mode 100644 src/soc/alu/input_stage.py

diff --git a/src/soc/alu/formal/.gitignore b/src/soc/alu/formal/.gitignore
new file mode 100644
index 00000000..150f68c8
--- /dev/null
+++ b/src/soc/alu/formal/.gitignore
@@ -0,0 +1 @@
+*/*
diff --git a/src/soc/alu/formal/proof_input_stage.py b/src/soc/alu/formal/proof_input_stage.py
new file mode 100644
index 00000000..faf68e07
--- /dev/null
+++ b/src/soc/alu/formal/proof_input_stage.py
@@ -0,0 +1,59 @@
+# Proof of correctness for partitioned equal signal combiner
+# Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
+
+from nmigen import Module, Signal, Elaboratable, Mux
+from nmigen.asserts import Assert, AnyConst, Assume, Cover
+from nmigen.test.utils import FHDLTestCase
+from nmigen.cli import rtlil
+
+from soc.alu.input_stage import ALUInputStage
+from soc.alu.pipe_data import ALUPipeSpec
+from soc.alu.alu_input_record import CompALUOpSubset
+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
+
+        pspec = ALUPipeSpec()
+        m.submodules.dut = dut = ALUInputStage(pspec)
+
+        rec = CompALUOpSubset()
+
+        for p in rec.ports():
+            width = p.width
+            comb += p.eq(AnyConst(width))
+
+        comb += dut.i.op.eq(rec)
+
+        for p in rec.ports():
+            name = p.name
+            rec_sig = p
+            dut_sig = getattr(dut.o.op, name)
+            comb += Assert(dut_sig == rec_sig)
+
+
+        return m
+
+class GTCombinerTestCase(FHDLTestCase):
+    def test_gt_combiner(self):
+        module = Driver()
+        self.assertFormal(module, mode="bmc", depth=4)
+        self.assertFormal(module, mode="cover", depth=4)
+    def test_ilang(self):
+        dut = Driver()
+        vl = rtlil.convert(dut, ports=[])
+        with open("input_stage.il", "w") as f:
+            f.write(vl)
+
+
+if __name__ == '__main__':
+    unittest.main()
diff --git a/src/soc/alu/input_stage.py b/src/soc/alu/input_stage.py
new file mode 100644
index 00000000..5bcff4f2
--- /dev/null
+++ b/src/soc/alu/input_stage.py
@@ -0,0 +1,23 @@
+from nmigen import (Module, Signal, Cat, Const, Mux, Repl, signed,
+                    unsigned)
+from nmutil.pipemodbase import PipeModBase
+from soc.alu.pipe_data import ALUInitialData
+
+
+class ALUInputStage(PipeModBase):
+    def __init__(self, pspec):
+        super().__init__(pspec, "input")
+
+    def ispec(self):
+        return ALUInitialData(self.pspec)
+
+    def ospec(self):
+        return ALUInitialData(self.pspec)
+
+    def elaborate(self, platform):
+        m = Module()
+        comb = m.d.comb
+
+        comb += self.o.op.eq(self.i.op)
+
+        return m
-- 
2.30.2