From: Michael Nolan Date: Mon, 25 May 2020 18:08:20 +0000 (-0400) Subject: Begin working on proof for compunit/fu X-Git-Tag: div_pipeline~831 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e53352eb1b4bc81dca2bef7471a618f91fb02b0b;p=soc.git Begin working on proof for compunit/fu --- diff --git a/src/soc/fu/compunits.py b/src/soc/fu/compunits.py deleted file mode 100644 index bfaa693a..00000000 --- a/src/soc/fu/compunits.py +++ /dev/null @@ -1,126 +0,0 @@ -################################################################### -"""Function Units Construction - -This module pulls all of the pipelines together (soc.fu.*) and, using -the regspec and Computation Unit APIs, constructs Scoreboard-aware -Function Units that may systematically and automatically be wired up -to appropriate Register Files. - -Two types exist: - -* Single-cycle Function Units. these are FUs that will only block for - one cycle. it is expected that multiple of these be instantiated, - because they are simple and trivial, and not many gates. - - - ALU, Logical: definitely several - - CR: not so many needed (perhaps) - - Branch: one or two of these (depending on speculation run-ahead) - - Trap: yeah really only one of these - - ShiftRot (perhaps not too many of these) - -* Multi-cycle (and FSM) Function Units. these are FUs that can only - handle a limited number of values, and take several cycles to complete. - Given that under Scoreboard Management, start and completion must be - fully managed, a "Reservation Station" style approach is required: - *one* multiple-stage (N stage) pipelines need a minimum of N (plural) - "CompUnit" front-ends. this includes: - - - MUL (all versions including MAC) - - DIV (including modulo) - -In either case, there will be multiple MultiCompUnits: it's just that -single-cycle ones are instantiated individually (one single-cycle pipeline -per MultiCompUnit, and multi-cycle ones need to be instantiated en-masse, -where *only one* actual pipeline (or FSM) has *multiple* Reservation -Stations. - -see: - -* https://libre-soc.org/3d_gpu/architecture/regfile/ section on regspecs - -""" - -from nmigen.cli import rtlil -from soc.experiment.compalu_multi import MultiCompUnit - -# pipeline / spec imports - -from soc.fu.alu.pipeline import ALUBasePipe -from soc.fu.alu.pipe_data import ALUPipeSpec - -from soc.fu.cr.pipeline import CRBasePipe -from soc.fu.cr.pipe_data import CRPipeSpec - -from soc.fu.branch.pipeline import BranchBasePipe -from soc.fu.branch.pipe_data import BranchPipeSpec - -from soc.fu.shift_rot.pipeline import ShiftRotBasePipe -from soc.fu.shift_rot.pipe_data import ShiftRotPipeSpec - - -################################################################### -###### FunctionUnitBaseSingle - use to make single-stge pipes ##### - -class FunctionUnitBaseSingle(MultiCompUnit): - """FunctionUnitBaseSingle - - main "glue" class that brings everything together. - ONLY use this class for single-stage pipelines. - - * :speckls: - the specification. contains regspec and op subset info, - and contains common "stuff" like the pipeline ctx, - what type of nmutil pipeline base is to be used (etc) - * :pipekls: - the type of pipeline. actually connects things together - - note that it is through MultiCompUnit.get_in/out that we *actually* - connect up the association between regspec variable names (defined - in the pipe_data). - """ - def __init__(self, speckls, pipekls): - pspec = speckls(id_wid=2) # spec (NNNPipeSpec instance) - opsubset = pspec.opsubsetkls # get the operand subset class - regspec = pspec.regspec # get the regspec - alu = pipekls(pspec) # create actual NNNBasePipe - super().__init__(regspec, alu, opsubset) # pass to MultiCompUnit - - -############################################################## -# TODO: ReservationStations-based (FunctionUnitBaseConcurrent) - -class FunctionUnitBaseMulti: - pass - - -###################################################################### -###### actual Function Units: these are "single" stage pipelines ##### - -class ALUFunctionUnit(FunctionUnitBaseSingle): - def __init__(self): super().__init__(ALUPipeSpec, ALUBasePipe) - -class CRFunctionUnit(FunctionUnitBaseSingle): - def __init__(self): super().__init__(CRPipeSpec, CRBasePipe) - -class BranchFunctionUnit(FunctionUnitBaseSingle): - def __init__(self): super().__init__(BranchPipeSpec, BranchBasePipe) - -class ShiftRotFunctionUnit(FunctionUnitBaseSingle): - def __init__(self): super().__init__(ShiftRotPipeSpec, ShiftRotBasePipe) - -##################################################################### -###### actual Function Units: these are "multi" stage pipelines ##### - -# TODO: ReservationStations-based. - - -def tst_single_fus_il(): - for (name, kls) in (('alu', ALUFunctionUnit), - ('cr', CRFunctionUnit), - ('branch', BranchFunctionUnit), - ('shiftrot', ShiftRotFunctionUnit)): - fu = kls() - vl = rtlil.convert(fu, ports=fu.ports()) - with open("fu_%s.il" % name, "w") as f: - f.write(vl) - -if __name__ == '__main__': - tst_single_fus_il() diff --git a/src/soc/fu/compunits/compunits.py b/src/soc/fu/compunits/compunits.py new file mode 100644 index 00000000..bfaa693a --- /dev/null +++ b/src/soc/fu/compunits/compunits.py @@ -0,0 +1,126 @@ +################################################################### +"""Function Units Construction + +This module pulls all of the pipelines together (soc.fu.*) and, using +the regspec and Computation Unit APIs, constructs Scoreboard-aware +Function Units that may systematically and automatically be wired up +to appropriate Register Files. + +Two types exist: + +* Single-cycle Function Units. these are FUs that will only block for + one cycle. it is expected that multiple of these be instantiated, + because they are simple and trivial, and not many gates. + + - ALU, Logical: definitely several + - CR: not so many needed (perhaps) + - Branch: one or two of these (depending on speculation run-ahead) + - Trap: yeah really only one of these + - ShiftRot (perhaps not too many of these) + +* Multi-cycle (and FSM) Function Units. these are FUs that can only + handle a limited number of values, and take several cycles to complete. + Given that under Scoreboard Management, start and completion must be + fully managed, a "Reservation Station" style approach is required: + *one* multiple-stage (N stage) pipelines need a minimum of N (plural) + "CompUnit" front-ends. this includes: + + - MUL (all versions including MAC) + - DIV (including modulo) + +In either case, there will be multiple MultiCompUnits: it's just that +single-cycle ones are instantiated individually (one single-cycle pipeline +per MultiCompUnit, and multi-cycle ones need to be instantiated en-masse, +where *only one* actual pipeline (or FSM) has *multiple* Reservation +Stations. + +see: + +* https://libre-soc.org/3d_gpu/architecture/regfile/ section on regspecs + +""" + +from nmigen.cli import rtlil +from soc.experiment.compalu_multi import MultiCompUnit + +# pipeline / spec imports + +from soc.fu.alu.pipeline import ALUBasePipe +from soc.fu.alu.pipe_data import ALUPipeSpec + +from soc.fu.cr.pipeline import CRBasePipe +from soc.fu.cr.pipe_data import CRPipeSpec + +from soc.fu.branch.pipeline import BranchBasePipe +from soc.fu.branch.pipe_data import BranchPipeSpec + +from soc.fu.shift_rot.pipeline import ShiftRotBasePipe +from soc.fu.shift_rot.pipe_data import ShiftRotPipeSpec + + +################################################################### +###### FunctionUnitBaseSingle - use to make single-stge pipes ##### + +class FunctionUnitBaseSingle(MultiCompUnit): + """FunctionUnitBaseSingle + + main "glue" class that brings everything together. + ONLY use this class for single-stage pipelines. + + * :speckls: - the specification. contains regspec and op subset info, + and contains common "stuff" like the pipeline ctx, + what type of nmutil pipeline base is to be used (etc) + * :pipekls: - the type of pipeline. actually connects things together + + note that it is through MultiCompUnit.get_in/out that we *actually* + connect up the association between regspec variable names (defined + in the pipe_data). + """ + def __init__(self, speckls, pipekls): + pspec = speckls(id_wid=2) # spec (NNNPipeSpec instance) + opsubset = pspec.opsubsetkls # get the operand subset class + regspec = pspec.regspec # get the regspec + alu = pipekls(pspec) # create actual NNNBasePipe + super().__init__(regspec, alu, opsubset) # pass to MultiCompUnit + + +############################################################## +# TODO: ReservationStations-based (FunctionUnitBaseConcurrent) + +class FunctionUnitBaseMulti: + pass + + +###################################################################### +###### actual Function Units: these are "single" stage pipelines ##### + +class ALUFunctionUnit(FunctionUnitBaseSingle): + def __init__(self): super().__init__(ALUPipeSpec, ALUBasePipe) + +class CRFunctionUnit(FunctionUnitBaseSingle): + def __init__(self): super().__init__(CRPipeSpec, CRBasePipe) + +class BranchFunctionUnit(FunctionUnitBaseSingle): + def __init__(self): super().__init__(BranchPipeSpec, BranchBasePipe) + +class ShiftRotFunctionUnit(FunctionUnitBaseSingle): + def __init__(self): super().__init__(ShiftRotPipeSpec, ShiftRotBasePipe) + +##################################################################### +###### actual Function Units: these are "multi" stage pipelines ##### + +# TODO: ReservationStations-based. + + +def tst_single_fus_il(): + for (name, kls) in (('alu', ALUFunctionUnit), + ('cr', CRFunctionUnit), + ('branch', BranchFunctionUnit), + ('shiftrot', ShiftRotFunctionUnit)): + fu = kls() + vl = rtlil.convert(fu, ports=fu.ports()) + with open("fu_%s.il" % name, "w") as f: + f.write(vl) + +if __name__ == '__main__': + tst_single_fus_il() diff --git a/src/soc/fu/compunits/formal/.gitignore b/src/soc/fu/compunits/formal/.gitignore new file mode 100644 index 00000000..150f68c8 --- /dev/null +++ b/src/soc/fu/compunits/formal/.gitignore @@ -0,0 +1 @@ +*/* diff --git a/src/soc/fu/compunits/formal/proof_fu.py b/src/soc/fu/compunits/formal/proof_fu.py new file mode 100644 index 00000000..0944fbaa --- /dev/null +++ b/src/soc/fu/compunits/formal/proof_fu.py @@ -0,0 +1,107 @@ +from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl, + signed, ResetSignal) +from nmigen.asserts import (Assert, AnyConst, Assume, Cover, Initial, + Rose, Fell, Stable, Past) +from nmigen.test.utils import FHDLTestCase +from nmigen.cli import rtlil +import unittest + +from soc.fu.compunits.compunits import FunctionUnitBaseSingle +from soc.experiment.alu_hier import DummyALU +from soc.experiment.compalu_multi import MultiCompUnit +from soc.fu.alu.alu_input_record import CompALUOpSubset + +class Driver(Elaboratable): + def __init__(self): + pass + + def elaborate(self, platform): + m = Module() + comb = m.d.comb + sync = m.d.sync + alu = DummyALU(16) + m.submodules.dut = dut = MultiCompUnit(16, alu, + CompALUOpSubset) + + go_rd = dut.rd.go + rd_rel = dut.rd.rel + issue = dut.issue_i + + go_die = dut.go_die_i + + rst = ResetSignal() + + init = Initial() + + has_issued = Signal(reset=0) + + + + with m.If(init): + comb += Assume(has_issued == 0) + comb += Assume(issue == 0) + comb += Assume(go_rd == 0) + comb += Assume(rst == 1) + with m.Else(): + comb += Assume(rst == 0) + + # Property One: Rd_rel should never be asserted before issue + + # detect when issue has been raised and remember it + with m.If(issue): + sync += has_issued.eq(1) + comb += Cover(has_issued) + # If issue has never been raised, then rd_rel should never be raised + with m.If(rd_rel != 0): + comb += Assert(has_issued) + + + # Property Two: when rd_rel is asserted, it should stay + # that way until a go_rd + with m.If((Past(go_rd) == 0) & ~Past(go_die)): + comb += Assert(~Fell(rd_rel)) + + # Property Three: when a bit in rd_rel is asserted, and + # the corresponding bit in go_rd is asserted, then that + # bit of rd_rel should be deasserted + for i in range(2): + with m.If(Past(go_rd)[i] & (Past(rd_rel) != 0)): + comb += Assert(rd_rel[i] == ~Past(go_rd)[i]) + + # Property Four: Similarly, if rd_rel is asserted, + # asserting go_die should make rd_rel be deasserted + + with m.If(Past(rd_rel) != 0): + with m.If(Past(go_die)): + comb += Assert(rd_rel == 0) + + # Property + + comb += Cover(Fell(rd_rel)) + + # Assume no instruction is issued until rd_rel is + # released. Idk if this is valid + + with m.If((rd_rel != 0) | (Past(rd_rel) != 0)): + comb += Assume(issue == 0) + + + + + + return m + +class FUTestCase(FHDLTestCase): + def test_formal(self): + module = Driver() + self.assertFormal(module, mode="bmc", depth=5) + self.assertFormal(module, mode="cover", depth=5) + def test_ilang(self): + dut = MultiCompUnit(16, DummyALU(16), CompALUOpSubset) + vl = rtlil.convert(dut, ports=dut.ports()) + with open("multicompunit.il", "w") as f: + f.write(vl) + + +if __name__ == '__main__': + unittest.main() diff --git a/src/soc/fu/compunits/formal/test_compunit.py b/src/soc/fu/compunits/formal/test_compunit.py new file mode 100644 index 00000000..2e6850aa --- /dev/null +++ b/src/soc/fu/compunits/formal/test_compunit.py @@ -0,0 +1,48 @@ +from nmigen import Signal, Module +from nmigen.back.pysim import Simulator, Delay, Settle +from nmigen.test.utils import FHDLTestCase +from nmigen.cli import rtlil +from soc.fu.compunits.compunits import FunctionUnitBaseSingle +from soc.experiment.alu_hier import DummyALU +from soc.experiment.compalu_multi import MultiCompUnit +from soc.fu.alu.alu_input_record import CompALUOpSubset +from soc.decoder.power_enums import InternalOp +import unittest + +class MaskGenTestCase(FHDLTestCase): + def test_maskgen(self): + m = Module() + comb = m.d.comb + alu = DummyALU(16) + m.submodules.dut = dut = MultiCompUnit(16, alu, + CompALUOpSubset) + sim = Simulator(m) + + def process(): + yield dut.src1_i.eq(0x5) + yield dut.src2_i.eq(0x5) + yield dut.issue_i.eq(1) + yield dut.oper_i.insn_type.eq(InternalOp.OP_ADD) + yield + yield dut.issue_i.eq(0) + yield + while True: + yield + rd_rel = yield dut.rd.rel + if rd_rel != 0: + break + yield dut.rd.go.eq(0xfff) + yield + yield dut.rd.go.eq(0) + for i in range(10): + yield + + + + sim.add_clock(1e-6) + sim.add_sync_process(process) + with sim.write_vcd("compunit.vcd", "compunit.gtkw", traces=dut.ports()): + sim.run() + +if __name__ == '__main__': + unittest.main()