From 6c74707101355960956055ee586e81c26914d2f0 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Fri, 22 May 2020 19:59:59 +0100 Subject: [PATCH] test branch ctr ok flag --- src/soc/fu/branch/formal/proof_main_stage.py | 1 + 1 file changed, 1 insertion(+) 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 -- 2.30.2