test branch ctr ok flag

diff --git a/src/soc/fu/branch/formal/proof_main_stage.py b/src/soc/fu/branch/formal/proof_main_stage.py
index 699efd574d7d9c592ec9df9de4b32ae00af17a97..ca8271f01179fe94de4371dcec86361c6562bc8f 100644 (file)
--- a/src/soc/fu/branch/formal/proof_main_stage.py
+++ b/src/soc/fu/branch/formal/proof_main_stage.py
@@ -151,6 +151,7 @@ class Driver(Elaboratable):
                 # Check that CTR is decremented
                 with m.If(~BO[2]):
                     comb += Assert(dut.o.ctr.data == ctr_next)
+                comb += Assert(dut.o.ctr.ok != BO[2])
 
 
         return m