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 218e4dfa94b0cf84c6bae138d81701739d988e02..699efd574d7d9c592ec9df9de4b32ae00af17a97 100644 (file)
--- 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]):