From: Samuel A. Falvo II <kc5tja@arrl.net>
Date: Fri, 21 Aug 2020 01:32:17 +0000 (-0700)
Subject: MUL pipeline proofs: mulli / mullw WIP.
X-Git-Tag: semi_working_ecp5~288^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f0ecc4a1be4044ee1f6ce5efc29f7a5b284634f3;p=soc.git

MUL pipeline proofs: mulli / mullw WIP.
---

diff --git a/src/soc/fu/mul/formal/proof_main_stage.py b/src/soc/fu/mul/formal/proof_main_stage.py
index d7550e41..e9f50593 100644
--- a/src/soc/fu/mul/formal/proof_main_stage.py
+++ b/src/soc/fu/mul/formal/proof_main_stage.py
@@ -122,6 +122,25 @@ class Driver(Elaboratable):
                     comb += expected_product.eq(Mux(a[63] ^ b[63], -prod, prod))
                     comb += Assert(dut.o.o.data[0:64] == expected_product[64:128])
 
+            # mulli, mullw(o)
+            with m.Case(MicrOp.OP_MUL_L64):
+                with m.If(rec.is_32bit):
+                    expected_product = Signal(64)
+#                   expected_o = Signal.like(expected_product)
+
+                    # unsigned lo64 - mulwu
+                    with m.If(~rec.is_signed):
+                        comb += expected_product.eq(a[0:32] * b[0:32])
+#                       comb += expected_o.eq(Repl(expected_product[0:32], 2))
+                        comb += Assert(dut.o.o.data[0:64] == expected_product[0:64])
+
+                    # signed lo64 - mulw
+                    with m.Else():
+                        pass
+
+                with m.Else(): # is 64-bit
+                    pass
+
         return m