Add output stage

diff --git a/src/soc/alu/formal/proof_output_stage.py b/src/soc/alu/formal/proof_output_stage.py
new file mode 100644 (file)
index 0000000..50fc4e4
--- /dev/null
+++ b/src/soc/alu/formal/proof_output_stage.py
@@ -0,0 +1,91 @@
+# Proof of correctness for partitioned equal signal combiner
+# Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
+
+from nmigen import Module, Signal, Elaboratable, Mux, Cat
+from nmigen.asserts import Assert, AnyConst, Assume, Cover
+from nmigen.test.utils import FHDLTestCase
+from nmigen.cli import rtlil
+
+from soc.alu.output_stage import ALUOutputStage
+from soc.alu.pipe_data import ALUPipeSpec
+from soc.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 = ALUOutputStage(pspec)
+
+        o = Signal(64)
+        carry_out = Signal()
+        carry_out32 = Signal()
+        ov = Signal()
+        ov32 = Signal()
+        cr0 = Signal(4)
+        so = Signal()
+        comb += [dut.i.o.eq(o),
+                 dut.i.carry_out.eq(carry_out),
+                 dut.i.so.eq(so),
+                 dut.i.carry_out32.eq(carry_out32),
+                 dut.i.cr0.eq(cr0),
+                 dut.i.ov.eq(ov),
+                 dut.i.ov32.eq(ov32),
+                 o.eq(AnyConst(64)),
+                 carry_out.eq(AnyConst(1)),
+                 carry_out32.eq(AnyConst(1)),
+                 ov.eq(AnyConst(1)),
+                 ov32.eq(AnyConst(1)),
+                 cr0.eq(AnyConst(4)),
+                 so.eq(AnyConst(1))]
+
+        comb += dut.i.ctx.op.eq(rec)
+
+        with m.If(dut.i.ctx.op.invert_out):
+            comb += Assert(dut.o.o == ~o)
+        with m.Else():
+            comb += Assert(dut.o.o == o)
+
+
+        # Assert that op gets copied from the input to output
+        for p in rec.ports():
+            name = p.name
+            rec_sig = p
+            dut_sig = getattr(dut.o.ctx.op, name)
+            comb += Assert(dut_sig == rec_sig)
+
+
+        return m
+
+class GTCombinerTestCase(FHDLTestCase):
+    def test_formal(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("output_stage.il", "w") as f:
+            f.write(vl)
+
+
+if __name__ == '__main__':
+    unittest.main()

diff --git a/src/soc/alu/output_stage.py b/src/soc/alu/output_stage.py
new file mode 100644 (file)
index 0000000..cb63b0e
--- /dev/null
+++ b/src/soc/alu/output_stage.py
@@ -0,0 +1,44 @@
+from nmigen import (Module, Signal, Cat)
+from nmutil.pipemodbase import PipeModBase
+from soc.alu.pipe_data import ALUInputData, ALUOutputData
+from ieee754.part.partsig import PartitionedSignal
+from soc.decoder.power_enums import InternalOp
+
+
+class ALUOutputStage(PipeModBase):
+    def __init__(self, pspec):
+        super().__init__(pspec, "output")
+
+    def ispec(self):
+        return ALUOutputData(self.pspec)
+
+    def ospec(self):
+        return ALUOutputData(self.pspec)
+
+    def elaborate(self, platform):
+        m = Module()
+        comb = m.d.comb
+
+        o = Signal.like(self.i.o)
+        with m.If(self.i.ctx.op.invert_out):
+            comb += o.eq(~self.i.o)
+        with m.Else():
+            comb += o.eq(self.i.o)
+
+        is_zero = Signal(reset_less=True)
+        is_positive = Signal(reset_less=True)
+        is_negative = Signal(reset_less=True)
+        so = Signal(reset_less=True)
+
+        comb += is_zero.eq(o == 0)
+        comb += is_positive.eq(~is_zero & ~o[63])
+        comb += is_negative.eq(~is_zero & o[63])
+        comb += so.eq(self.i.so | self.i.ov)
+
+        comb += self.o.o.eq(o)
+        comb += self.o.cr0.eq(Cat(is_negative, is_positive, is_zero, so))
+        comb += self.o.so.eq(so)
+
+        comb += self.o.ctx.eq(self.i.ctx)
+
+        return m

diff --git a/src/soc/alu/pipe_data.py b/src/soc/alu/pipe_data.py
index 1601bcb333e2a3c175df46cee6083708a6599626..fa48f4ee8b0d750759f509d47df1663278634674 100644 (file)
--- a/src/soc/alu/pipe_data.py
+++ b/src/soc/alu/pipe_data.py
@@ -43,7 +43,7 @@ class ALUInputData(IntegerData):
 class ALUOutputData(IntegerData):
     def __init__(self, pspec):
         super().__init__(pspec)
-        self.o = Signal(64, reset_less=True)
+        self.o = Signal(64, reset_less=True, name="stage_o")
         self.carry_out = Signal(reset_less=True)
         self.carry_out32 = Signal(reset_less=True)
         self.cr0 = Signal(4, reset_less=True)