From: Samuel A. Falvo II <kc5tja@arrl.net>
Date: Fri, 21 Aug 2020 02:54:20 +0000 (-0700)
Subject: MUL pipeline: account for overflow flags.  WIP
X-Git-Tag: semi_working_ecp5~287
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=632fd65bedcc1e6638374995ef59b55c2ba858ea;p=soc.git

MUL pipeline: account for overflow flags.  WIP
---

diff --git a/src/soc/fu/mul/formal/proof_main_stage.py b/src/soc/fu/mul/formal/proof_main_stage.py
index e9f50593..7ca876d4 100644
--- a/src/soc/fu/mul/formal/proof_main_stage.py
+++ b/src/soc/fu/mul/formal/proof_main_stage.py
@@ -124,16 +124,19 @@ class Driver(Elaboratable):
 
             # 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)
+                expected_product = Signal(64)
+                expected_ov = Signal()
 
+                with m.If(rec.is_32bit):
                     # 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])
 
+                        m31 = expected_product[31:64]
+                        comb += expected_ov.eq(m31.bool() & ~m31.all())
+                        comb += Assert(dut.o.xer_ov.data == Repl(expected_ov, 2))
+
                     # signed lo64 - mulw
                     with m.Else():
                         pass