From: Michael Nolan Date: Fri, 8 May 2020 15:03:34 +0000 (-0400) Subject: Begin adding input stage of alu X-Git-Tag: div_pipeline~1347 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=26dfc9d27388c99f147d8c55e6c933fa91add592;p=soc.git Begin adding input stage of alu --- 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 + +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