From e53352eb1b4bc81dca2bef7471a618f91fb02b0b Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Mon, 25 May 2020 14:08:20 -0400 Subject: [PATCH] Begin working on proof for compunit/fu --- src/soc/fu/{ => compunits}/compunits.py | 0 src/soc/fu/compunits/formal/.gitignore | 1 + src/soc/fu/compunits/formal/proof_fu.py | 107 +++++++++++++++++++ src/soc/fu/compunits/formal/test_compunit.py | 48 +++++++++ 4 files changed, 156 insertions(+) rename src/soc/fu/{ => compunits}/compunits.py (100%) create mode 100644 src/soc/fu/compunits/formal/.gitignore create mode 100644 src/soc/fu/compunits/formal/proof_fu.py create mode 100644 src/soc/fu/compunits/formal/test_compunit.py diff --git a/src/soc/fu/compunits.py b/src/soc/fu/compunits/compunits.py similarity index 100% rename from src/soc/fu/compunits.py rename to src/soc/fu/compunits/compunits.py 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() -- 2.30.2