X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Fsoc%2Ffu%2Fbranch%2Fformal%2Fproof_main_stage.py;h=394c43469d62d72c70d99c8185381e6bc9f35deb;hb=a696530bf6c52863eff6bf8d0c19f373e7d5e979;hp=7a94c1d3e594bdf5b016cd4af5efce8ee951c7a2;hpb=f29f936e39ad4f6f797723752756b0dc8b497fda;p=soc.git

diff --git a/src/soc/fu/branch/formal/proof_main_stage.py b/src/soc/fu/branch/formal/proof_main_stage.py
index 7a94c1d3..394c4346 100644
--- a/src/soc/fu/branch/formal/proof_main_stage.py
+++ b/src/soc/fu/branch/formal/proof_main_stage.py
@@ -57,11 +57,11 @@ class Driver(Elaboratable):
         cr_arr = Array([cr[(7-i)*4:(7-i)*4+4] for i in range(8)])
         cr_bit_arr = Array([cr[31-i] for i in range(32)])
 
-        cia, cr_in, spr1, spr2 = dut.i.cia, dut.i.cr, dut.i.spr1, dut.i.spr2
-        ctr = spr1
+        cia, cr_in, fast1, fast2 = dut.i.cia, dut.i.cr, dut.i.fast1, dut.i.fast2
+        ctr = fast1
         lr_o, nia_o = dut.o.lr, dut.o.nia
 
-        comb += [spr2.eq(AnyConst(64)),
+        comb += [fast2.eq(AnyConst(64)),
                  ctr.eq(AnyConst(64)),
                  cia.eq(AnyConst(64))]
 
@@ -157,7 +157,7 @@ class Driver(Elaboratable):
 
                 with m.If(nia_o.ok):
                     # make sure we branch to the spr input
-                    comb += Assert(nia_o.data == spr1)
+                    comb += Assert(nia_o.data == fast1)
 
                     # make sure branch+link works
                     comb += Assert(lr_o.ok == rec.lk)