From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Fri, 22 May 2020 18:59:59 +0000 (+0100)
Subject: test branch ctr ok flag
X-Git-Tag: div_pipeline~929
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6c74707101355960956055ee586e81c26914d2f0;p=soc.git

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 699efd57..ca8271f0 100644
--- 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