OP_CMP is requesting a change of the output register (should not do that)

[soc.git] / src / soc / fu / alu / formal / proof_main_stage.py

diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py
index 0257d6f001225e11eb8234eedcb45c33929df1eb..08e742597d965234eb0bf523a8c14d8aff6f40cd 100644 (file)
--- a/src/soc/fu/alu/formal/proof_main_stage.py
+++ b/src/soc/fu/alu/formal/proof_main_stage.py
@@ -116,6 +116,7 @@ class Driver(Elaboratable):
                 # CMP is defined as not taking in carry
                 comb += Assume(ca_in == 0)
                 comb += Assert(o == (a+b)[0:64])
+                comb += o_ok.eq(0) # must not change output reg
 
             with m.Case(InternalOp.OP_CMPEQB):
                 src1 = a[0:8]