From: Michael Nolan <mtnolan2640@gmail.com>
Date: Fri, 22 May 2020 18:43:32 +0000 (-0400)
Subject: Fix link handling in branch proof
X-Git-Tag: div_pipeline~932
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7ce3152d24e0480b2a68df7b25fab5dff205c742;p=soc.git

Fix link handling in branch proof
---

diff --git a/src/soc/fu/branch/formal/proof_main_stage.py b/src/soc/fu/branch/formal/proof_main_stage.py
index 47692a2d..cf720229 100644
--- a/src/soc/fu/branch/formal/proof_main_stage.py
+++ b/src/soc/fu/branch/formal/proof_main_stage.py
@@ -62,7 +62,6 @@ class Driver(Elaboratable):
         i_fields = dut.fields.FormI
         b_fields = dut.fields.FormB
         AA = i_fields.AA[0:-1]
-        LK = i_fields.LK[0:-1]
 
         # Handle CR bit selection
         BI = b_fields.BI[0:-1]
@@ -109,9 +108,12 @@ class Driver(Elaboratable):
                     comb += Assert(nia_o.data == (cia + imm)[0:64])
 
                 # Make sure linking works
-                with m.If(LK & 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)
+                    
             with m.Case(InternalOp.OP_BC):
                 # Assert that branches are conditional
                 comb += Assert(nia_o.ok == (cond_ok & ctr_ok))
@@ -126,9 +128,12 @@ class Driver(Elaboratable):
                         comb += Assert(nia_o.data == imm)
                     with m.Else():
                         comb += Assert(nia_o.data == (cia + imm)[0:64])
-                    with m.If(LK & 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]):
@@ -142,9 +147,11 @@ class Driver(Elaboratable):
                     comb += Assert(nia_o.data == spr1)
 
                     # make sure branch+link works
-                    with m.If(LK & 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]):