From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Fri, 22 May 2020 18:52:55 +0000 (+0100)
Subject: cleaner way to test link register ok
X-Git-Tag: div_pipeline~930
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=be2a8cb07f1719ef3c3b6df5cfc15f54479257b0;p=soc.git

cleaner way to test link register ok
---

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]):