From a1e4a0914899ef730726c682334e4aeaf7b804b6 Mon Sep 17 00:00:00 2001 From: "Samuel A. Falvo II" Date: Mon, 10 Aug 2020 14:17:08 -0700 Subject: [PATCH] WIP!! Make MUL pipeline proof run again. Removed existing set of tests, as they didn't seem to be relevant (appeared to be copy-and-paste template code). Next steps is to go through main_stage.py and implement corresponding proofs. --- src/soc/fu/mul/formal/proof_main_stage.py | 101 +++++++++++----------- 1 file changed, 50 insertions(+), 51 deletions(-) diff --git a/src/soc/fu/mul/formal/proof_main_stage.py b/src/soc/fu/mul/formal/proof_main_stage.py index 890475a6..fd99fcd6 100644 --- a/src/soc/fu/mul/formal/proof_main_stage.py +++ b/src/soc/fu/mul/formal/proof_main_stage.py @@ -7,9 +7,9 @@ from nmigen.asserts import Assert, AnyConst, Assume, Cover from nmutil.formaltest import FHDLTestCase from nmigen.cli import rtlil -from soc.fu.shift_rot.main_stage import ShiftRotMainStage -from soc.fu.alu.pipe_data import ALUPipeSpec -from soc.fu.alu.alu_input_record import CompALUOpSubset +from soc.fu.mul.pipe_data import CompMULOpSubset, MulPipeSpec +from soc.fu.mul.main_stage import MulMainStage2 + from soc.decoder.power_enums import MicrOp import unittest @@ -25,76 +25,75 @@ class Driver(Elaboratable): m = Module() comb = m.d.comb - rec = CompALUOpSubset() - recwidth = 0 + rec = CompMULOpSubset() + # Setup random inputs for dut.op + recwidth = 0 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 = ShiftRotMainStage(pspec) + pspec = MulPipeSpec(id_wid=2) + m.submodules.dut = dut = MulMainStage2(pspec) # convenience variables - a = dut.i.rs - b = dut.i.rb - ra = dut.i.ra - carry_in = dut.i.xer_ca[0] - carry_in32 = dut.i.xer_ca[1] - so_in = dut.i.xer_so - carry_out = dut.o.xer_ca - o = dut.o.o +# a = dut.i.rs +# b = dut.i.rb +# ra = dut.i.ra +# carry_in = dut.i.xer_ca[0] +# carry_in32 = dut.i.xer_ca[1] +# so_in = dut.i.xer_so +# carry_out = dut.o.xer_ca +# o = dut.o.o # setup random inputs - comb += [a.eq(AnyConst(64)), - b.eq(AnyConst(64)), - carry_in.eq(AnyConst(1)), - carry_in32.eq(AnyConst(1)), - so_in.eq(AnyConst(1))] +# comb += [a.eq(AnyConst(64)), +# b.eq(AnyConst(64)), +# carry_in.eq(AnyConst(1)), +# carry_in32.eq(AnyConst(1)), +# so_in.eq(AnyConst(1))] comb += dut.i.ctx.op.eq(rec) # Assert that op gets copied from the input to output - for rec_sig in rec.ports(): - name = rec_sig.name - dut_sig = getattr(dut.o.ctx.op, name) - comb += Assert(dut_sig == rec_sig) + comb += Assert(dut.o.ctx.op == dut.i.ctx.op) + comb += Assert(dut.o.ctx.muxid == dut.i.ctx.muxid) # signed and signed/32 versions of input a - a_signed = Signal(signed(64)) - a_signed_32 = Signal(signed(32)) - comb += a_signed.eq(a) - comb += a_signed_32.eq(a[0:32]) +# a_signed = Signal(signed(64)) +# a_signed_32 = Signal(signed(32)) +# comb += a_signed.eq(a) +# comb += a_signed_32.eq(a[0:32]) # main assertion of arithmetic operations - with m.Switch(rec.insn_type): - with m.Case(MicrOp.OP_SHL): - comb += Assume(ra == 0) - with m.If(rec.is_32bit): - comb += Assert(o[0:32] == ((a << b[0:6]) & 0xffffffff)) - comb += Assert(o[32:64] == 0) - with m.Else(): - comb += Assert(o == ((a << b[0:7]) & ((1 << 64)-1))) - with m.Case(MicrOp.OP_SHR): - comb += Assume(ra == 0) - with m.If(~rec.is_signed): - with m.If(rec.is_32bit): - comb += Assert(o[0:32] == (a[0:32] >> b[0:6])) - comb += Assert(o[32:64] == 0) - with m.Else(): - comb += Assert(o == (a >> b[0:7])) - with m.Else(): - with m.If(rec.is_32bit): - comb += Assert(o[0:32] == (a_signed_32 >> b[0:6])) - comb += Assert(o[32:64] == Repl(a[31], 32)) - with m.Else(): - comb += Assert(o == (a_signed >> b[0:7])) +# with m.Switch(rec.insn_type): +# with m.Case(MicrOp.OP_SHL): +# comb += Assume(ra == 0) +# with m.If(rec.is_32bit): +# comb += Assert(o[0:32] == ((a << b[0:6]) & 0xffffffff)) +# comb += Assert(o[32:64] == 0) +# with m.Else(): +# comb += Assert(o == ((a << b[0:7]) & ((1 << 64)-1))) +# with m.Case(MicrOp.OP_SHR): +# comb += Assume(ra == 0) +# with m.If(~rec.is_signed): +# with m.If(rec.is_32bit): +# comb += Assert(o[0:32] == (a[0:32] >> b[0:6])) +# comb += Assert(o[32:64] == 0) +# with m.Else(): +# comb += Assert(o == (a >> b[0:7])) +# with m.Else(): +# with m.If(rec.is_32bit): +# comb += Assert(o[0:32] == (a_signed_32 >> b[0:6])) +# comb += Assert(o[32:64] == Repl(a[31], 32)) +# with m.Else(): +# comb += Assert(o == (a_signed >> b[0:7])) return m -class ALUTestCase(FHDLTestCase): +class MulTestCase(FHDLTestCase): def test_formal(self): module = Driver() self.assertFormal(module, mode="bmc", depth=2) -- 2.30.2