From be2a8cb07f1719ef3c3b6df5cfc15f54479257b0 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Fri, 22 May 2020 19:52:55 +0100 Subject: [PATCH] cleaner way to test link register ok --- src/soc/fu/branch/formal/proof_main_stage.py | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/soc/fu/branch/formal/proof_main_stage.py b/src/soc/fu/branch/formal/proof_main_stage.py index 218e4dfa..699efd57 100644 --- a/src/soc/fu/branch/formal/proof_main_stage.py +++ b/src/soc/fu/branch/formal/proof_main_stage.py @@ -128,11 +128,9 @@ class Driver(Elaboratable): comb += Assert(nia_o.data == imm) with m.Else(): comb += Assert(nia_o.data == (cia + imm)[0:64]) + comb += Assert(lr_o.ok == rec.lk) with m.If(rec.lk): comb += Assert(lr_o.data == (cia + 4)[0:64]) - comb += Assert(lr_o.ok == 1) - with m.Else(): - comb += Assert(lr_o.ok == 0) # Check that CTR is decremented with m.If(~BO[2]): @@ -146,11 +144,9 @@ class Driver(Elaboratable): comb += Assert(nia_o.data == spr1) # make sure branch+link works + comb += Assert(lr_o.ok == rec.lk) with m.If(rec.lk): comb += Assert(lr_o.data == (cia + 4)[0:64]) - comb += Assert(lr_o.ok == 1) - with m.Else(): - comb += Assert(lr_o.ok == 0) # Check that CTR is decremented with m.If(~BO[2]): -- 2.30.2