From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Sat, 4 Jul 2020 19:45:45 +0000 (+0100)
Subject: more updating spr1/spr2 to fast1/fast2
X-Git-Tag: div_pipeline~162^2~81
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a696530bf6c52863eff6bf8d0c19f373e7d5e979;p=soc.git

more updating spr1/spr2 to fast1/fast2
---

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)