From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Wed, 20 May 2020 16:54:34 +0000 (+0100)
Subject: formal proof rename on XER flags
X-Git-Tag: div_pipeline~1026
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2f033d1bb26662cd1dea19a0d723bf021de3e17e;p=soc.git

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 9e33f148..ff838d91 100644
--- 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 7db2c40a..456ff815 100644
--- 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)