From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Wed, 20 May 2020 16:50:32 +0000 (+0100)
Subject: update to new names for XER fields
X-Git-Tag: div_pipeline~1027
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0494047481f41a47fd8c221500f998d54f6e702a;p=soc.git

update to new names for XER fields
---

diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py
index 3bc06e6f..91aaac5b 100644
--- a/src/soc/fu/alu/formal/proof_main_stage.py
+++ b/src/soc/fu/alu/formal/proof_main_stage.py
@@ -39,16 +39,17 @@ class Driver(Elaboratable):
         # convenience variables
         a = dut.i.a
         b = dut.i.b
-        carry_in = dut.i.carry_in
-        so_in = dut.i.so
-        carry_out = dut.o.xer_co.data[0]
-        carry_out32 = dut.o.xer_co.data[1]
+        carry_in = dut.i.xer_ca[0]
+        carry_in32 = dut.i.xer_ca[1]
+        so_in = dut.i.xer_so
+        carry_out = dut.o.xer_ca.data[0]
+        carry_out32 = dut.o.xer_ca.data[1]
         o = dut.o.o
 
         # setup random inputs
         comb += [a.eq(AnyConst(64)),
                  b.eq(AnyConst(64)),
-                 carry_in.eq(AnyConst(1)),
+                 carry_in.eq(AnyConst(0b11)),
                  so_in.eq(AnyConst(1))]
 
         comb += dut.i.ctx.op.eq(rec)
@@ -73,8 +74,8 @@ class Driver(Elaboratable):
 
                 comb += Assert(Cat(o, carry_out) == (a + b + carry_in))
 
-                # CA32
-                comb += Assert((a[0:32] + b[0:32] + carry_in)[32]
+                # CA32 - XXX note this fails! replace with carry_in and it works
+                comb += Assert((a[0:32] + b[0:32] + carry_in32)[32]
                                == carry_out32)
             with m.Case(InternalOp.OP_EXTS):
                 for i in [1, 2, 4]: