formal proof rename on XER flags

diff --git a/src/soc/fu/alu/formal/proof_output_stage.py b/src/soc/fu/alu/formal/proof_output_stage.py
index 9e33f14891550040f3f145863842e94f8ee2897b..ff838d9192aa1a8146dab49cf0abc5126a1c71f3 100644 (file)
--- a/src/soc/fu/alu/formal/proof_output_stage.py
+++ b/src/soc/fu/alu/formal/proof_output_stage.py
@@ -43,12 +43,12 @@ class Driver(Elaboratable):
         cr0 = Signal(4)
         so = Signal()
         comb += [dut.i.o.eq(o),
-                 dut.i.carry_out.eq(carry_out),
-                 dut.i.so.eq(so),
-                 dut.i.carry_out32.eq(carry_out32),
+                 dut.i.xer_ca[0].eq(carry_out),
+                 dut.i.xer_so.eq(so),
+                 dut.i.xer_ca[1].eq(carry_out32),
                  dut.i.cr0.eq(cr0),
-                 dut.i.ov.eq(ov),
-                 dut.i.ov32.eq(ov32),
+                 dut.i.xer_ov[0].eq(ov),
+                 dut.i.xer_ov[1].eq(ov32),
                  o.eq(AnyConst(64)),
                  carry_out.eq(AnyConst(1)),
                  carry_out32.eq(AnyConst(1)),

diff --git a/src/soc/fu/logical/formal/proof_main_stage.py b/src/soc/fu/logical/formal/proof_main_stage.py
index 7db2c40af51b24dc9017231e44ab3f7e08c8767b..456ff815348a80f243bcdeddf1d51d1fc78a5092 100644 (file)
--- a/src/soc/fu/logical/formal/proof_main_stage.py
+++ b/src/soc/fu/logical/formal/proof_main_stage.py
@@ -51,14 +51,15 @@ 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_in = dut.i.xer_ca[0]
+        carry_in32 = dut.i.xer_ca[1]
+        so_in = dut.i.xer_so
         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)