From 280b76066dbea6ac44df096a768040b8231e8fb9 Mon Sep 17 00:00:00 2001 From: "Samuel A. Falvo II" Date: Sat, 29 Aug 2020 16:53:49 -0700 Subject: [PATCH] Qualify XER_OV output in proof --- src/soc/fu/mul/formal/proof_main_stage.py | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/src/soc/fu/mul/formal/proof_main_stage.py b/src/soc/fu/mul/formal/proof_main_stage.py index 873a1636..9631bca2 100644 --- a/src/soc/fu/mul/formal/proof_main_stage.py +++ b/src/soc/fu/mul/formal/proof_main_stage.py @@ -8,6 +8,9 @@ from nmutil.formaltest import FHDLTestCase from nmutil.stageapi import StageChain from nmigen.cli import rtlil +from soc.decoder.power_fields import DecodeFields +from soc.decoder.power_fieldsn import SignalBitRange + from soc.fu.mul.pipe_data import CompMULOpSubset, MulPipeSpec from soc.fu.mul.pre_stage import MulMainStage1 from soc.fu.mul.main_stage import MulMainStage2 @@ -58,6 +61,7 @@ class Driver(Elaboratable): b = dut.i.rb o = dut.o.o.data xer_ov_o = dut.o.xer_ov.data + xer_ov_ok = dut.o.xer_ov.ok # For 32- and 64-bit parameters, work out the absolute values of the # input parameters for signed multiplies. Needed for signed @@ -104,6 +108,15 @@ class Driver(Elaboratable): comb += dut.i.ctx.op.eq(rec) + # Gain access to the OE field of XO-format instructions. + fields = DecodeFields(SignalBitRange, [dut.i.ctx.op.insn]) + fields.create_specs() + + enable_overflow = fields.FormXO.OE[0:-1] + + with m.If(~enable_overflow): + comb += Assert(~xer_ov_ok) + # Assert that op gets copied from the input to output comb += Assert(dut.o.ctx.op == dut.i.ctx.op) comb += Assert(dut.o.ctx.muxid == dut.i.ctx.muxid) @@ -213,7 +226,9 @@ class Driver(Elaboratable): m31 = exp_prod[31:64] comb += expected_ov.eq(m31.bool() & ~m31.all()) - comb += Assert(xer_ov_o == Repl(expected_ov, 2)) + with m.If(enable_overflow): + comb += Assert(xer_ov_o == Repl(expected_ov, 2)) + comb += Assert(xer_ov_ok) with m.Else(): # is 64-bit; mulld expected_ov = Signal() @@ -264,7 +279,9 @@ class Driver(Elaboratable): m63 = exp_prod[63:128] comb += expected_ov.eq(m63.bool() & ~m63.all()) - comb += Assert(xer_ov_o == Repl(expected_ov, 2)) + with m.If(enable_overflow): + comb += Assert(xer_ov_o == Repl(expected_ov, 2)) + comb += Assert(xer_ov_ok) return m -- 2.30.2