MUL pipeline proof: signed mulhw

diff --git a/src/soc/fu/mul/formal/proof_main_stage.py b/src/soc/fu/mul/formal/proof_main_stage.py
index 0b1fe15d6743a0cae6ff8a85fb2f08fccd14207c..4d59c84ac2595ff9b4b76965150bc451e1b265c6 100644 (file)
--- a/src/soc/fu/mul/formal/proof_main_stage.py
+++ b/src/soc/fu/mul/formal/proof_main_stage.py
@@ -57,12 +57,11 @@ class Driver(Elaboratable):
         # convenience variables
         a = dut.i.ra
         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
+
+        abs32_a = Signal(32)
+        abs32_b = Signal(32)
+        comb += abs32_a.eq(Mux(a[31], -a[0:32], a[0:32]))
+        comb += abs32_b.eq(Mux(b[31], -b[0:32], b[0:32]))
 
         # setup random inputs
         comb += [a.eq(AnyConst(64)),
@@ -79,29 +78,27 @@ class Driver(Elaboratable):
         # Doesn't mean that the ok signal is always set though.
         comb += Assert(dut.o.xer_so.data == dut.i.xer_so)
 
-
-        # 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])
-
         # main assertion of arithmetic operations
         with m.Switch(rec.insn_type):
             with m.Case(MicrOp.OP_MUL_H32):
                 comb += Assume(rec.is_32bit) # OP_MUL_H32 is a 32-bit op
 
+                expected_product = Signal(64)
+                expected_o = Signal.like(expected_product)
+
                 # unsigned hi32 - mulhwu
                 with m.If(~rec.is_signed):
-                    expected_product = Signal(64)
-                    expected_o = Signal(64)
                     comb += expected_product.eq(a[0:32] * b[0:32])
                     comb += expected_o.eq(Repl(expected_product[32:64], 2))
                     comb += Assert(dut.o.o.data[0:64] == expected_o)
 
                 # signed hi32 - mulhw
                 with m.Else():
-                    pass
+                    prod = Signal.like(expected_product)    # intermediate product
+                    comb += prod.eq(abs32_a * abs32_b)
+                    comb += expected_product.eq(Mux(a[31] ^ b[31], -prod, prod))
+                    comb += expected_o.eq(Repl(expected_product[32:64], 2))
+                    comb += Assert(dut.o.o.data[0:64] == expected_o)
 
 
         return m