From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Wed, 15 Jul 2020 10:49:52 +0000 (+0100)
Subject: use Record Assert and also check muxid
X-Git-Tag: div_pipeline~33
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b9bf80737f94469f387ae3df24e223f505c9c2bc;p=soc.git

use Record Assert and also check muxid
see https://bugs.libre-soc.org/show_bug.cgi?id=429#c3
---

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))