From: Samuel A. Falvo II <kc5tja@arrl.net>
Date: Mon, 10 Aug 2020 21:17:08 +0000 (-0700)
Subject: WIP!!  Make MUL pipeline proof run again.
X-Git-Tag: semi_working_ecp5~405
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a1e4a0914899ef730726c682334e4aeaf7b804b6;p=soc.git

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.
---

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)