From 43b235dc3d98696fb80b2fc9f5737b3532730ee6 Mon Sep 17 00:00:00 2001 From: "Samuel A. Falvo II" Date: Sat, 29 Aug 2020 10:28:12 -0700 Subject: [PATCH] WIP: prep for 64-bit insns --- src/soc/fu/mul/formal/proof_main_stage.py | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/soc/fu/mul/formal/proof_main_stage.py b/src/soc/fu/mul/formal/proof_main_stage.py index ca07a9f6..8b576c1d 100644 --- a/src/soc/fu/mul/formal/proof_main_stage.py +++ b/src/soc/fu/mul/formal/proof_main_stage.py @@ -125,17 +125,16 @@ class Driver(Elaboratable): # mulli, mullw(o)(u), mulld(o)(u) with m.Case(MicrOp.OP_MUL_L64): expected_ov = Signal() + prod = Signal(64) + expected_product = Signal.like(prod) with m.If(rec.is_32bit): - prod = Signal(64) - expected_product = Signal.like(prod) - - # unsigned lo64 - mullwu + # unsigned lo32 - mullwu with m.If(~rec.is_signed): comb += expected_product.eq(a[0:32] * b[0:32]) comb += Assert(dut.o.o.data[0:64] == expected_product[0:64]) - # signed lo64 - mullw + # signed lo32 - mullw with m.Else(): comb += prod.eq(abs32_a[0:64] * abs32_b[0:64]) comb += expected_product.eq(Mux(a[31] ^ b[31], -prod, prod)) @@ -146,7 +145,12 @@ class Driver(Elaboratable): comb += Assert(dut.o.xer_ov.data == Repl(expected_ov, 2)) with m.Else(): # is 64-bit - pass + # unsigned lo64 - mulldu + with m.If(~rec.is_signed): + pass + + with m.Else(): + pass return m -- 2.30.2