From b9bf80737f94469f387ae3df24e223f505c9c2bc Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Wed, 15 Jul 2020 11:49:52 +0100 Subject: [PATCH] use Record Assert and also check muxid see https://bugs.libre-soc.org/show_bug.cgi?id=429#c3 --- src/soc/fu/alu/formal/proof_main_stage.py | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py index 5e70d1e8..a5e8e12f 100644 --- a/src/soc/fu/alu/formal/proof_main_stage.py +++ b/src/soc/fu/alu/formal/proof_main_stage.py @@ -59,13 +59,16 @@ class Driver(Elaboratable): ca_in.eq(AnyConst(0b11)), so_in.eq(AnyConst(1))] + # and for the context muxid + width = dut.i.ctx.muxid.width + comb += dut.i.ctx.muxid.eq(AnyConst(width)) + + # assign the PowerDecode2 operation subset comb += dut.i.ctx.op.eq(rec) - # Assert that op gets copied from the input to output - for rec_sig in rec.ports(): - name = rec_sig.name - dut_sig = getattr(dut.o.ctx.op, name) - comb += Assert(dut_sig == rec_sig) + # check that the operation (op) is passed through (and muxid) + comb += Assert(dut.o.ctx.op == dut.i.ctx.op) + comb += Assert(dut.o.ctx.muxid == dut.i.ctx.muxid) # signed and signed/32 versions of input a a_signed = Signal(signed(64)) -- 2.30.2