From: Samuel A. Falvo II <kc5tja@arrl.net>
Date: Sat, 29 Aug 2020 23:27:54 +0000 (-0700)
Subject: Fix test breakage in MUL proofs
X-Git-Tag: semi_working_ecp5~225^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5b7fbaa29b5a670704a0007ed521e8e50e409732;p=soc.git

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 7b80e344..873a1636 100644
--- 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):