From 0d9771ee4544ce13e985d5d01cea959297732907 Mon Sep 17 00:00:00 2001 From: "Samuel A. Falvo II" Date: Thu, 20 Aug 2020 15:30:17 -0700 Subject: [PATCH] MUL pipeline proof: signed mulhw --- src/soc/fu/mul/formal/proof_main_stage.py | 29 ++++++++++------------- 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/src/soc/fu/mul/formal/proof_main_stage.py b/src/soc/fu/mul/formal/proof_main_stage.py index 0b1fe15d..4d59c84a 100644 --- 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 -- 2.30.2