Fix test breakage in MUL proofs

diff --git a/src/soc/fu/mul/formal/proof_main_stage.py b/src/soc/fu/mul/formal/proof_main_stage.py
index 7b80e344905fd45e8848e2642ec9abcabb4d7af5..873a163670d7be91e2fd78ce6503867e30b55b26 100644 (file)
--- a/src/soc/fu/mul/formal/proof_main_stage.py
+++ b/src/soc/fu/mul/formal/proof_main_stage.py
@@ -110,7 +110,7 @@ class Driver(Elaboratable):
 
         # Assert that XER_SO propagates through as well.
         # Doesn't mean that the ok signal is always set though.
-        comb += Assert(xer_ov_o == dut.i.xer_so)
+        comb += Assert(dut.o.xer_so.data == dut.i.xer_so)
 
         # main assertion of arithmetic operations
         with m.Switch(rec.insn_type):