From 63ffead2c4d28def2f89bc250a69903eb61f1986 Mon Sep 17 00:00:00 2001
From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Sun, 24 May 2020 13:09:54 +0100
Subject: [PATCH] cleanup/code-munge on ALU main stage proof

---
 src/soc/fu/alu/formal/proof_main_stage.py | 35 ++++++++++++-----------
 1 file changed, 18 insertions(+), 17 deletions(-)

diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py
index 0534de4c..b63e958e 100644
--- a/src/soc/fu/alu/formal/proof_main_stage.py
+++ b/src/soc/fu/alu/formal/proof_main_stage.py
@@ -37,19 +37,20 @@ class Driver(Elaboratable):
         # convenience variables
         a = dut.i.a
         b = dut.i.b
-        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]
-        ov_out = dut.o.xer_ov.data[0]
-        ov_out32 = dut.o.xer_ov.data[1]
+        ca_in = dut.i.xer_ca[0]   # CA carry in
+        ca32_in = dut.i.xer_ca[1] # CA32 carry in 32
+        so_in = dut.i.xer_so      # SO sticky overflow
+
+        ca_o = dut.o.xer_ca.data[0]   # CA carry out
+        ca32_o = dut.o.xer_ca.data[1] # CA32 carry out32
+        ov_o = dut.o.xer_ov.data[0]   # OV overflow
+        ov32_o = dut.o.xer_ov.data[1] # OV32 overflow32
         o = dut.o.o
 
         # setup random inputs
         comb += [a.eq(AnyConst(64)),
                  b.eq(AnyConst(64)),
-                 carry_in.eq(AnyConst(0b11)),
+                 ca_in.eq(AnyConst(0b11)),
                  so_in.eq(AnyConst(1))]
 
         comb += dut.i.ctx.op.eq(rec)
@@ -68,29 +69,29 @@ class Driver(Elaboratable):
 
         comb += Assume(a[32:64] == 0)
         comb += Assume(b[32:64] == 0)
+
         # main assertion of arithmetic operations
         with m.Switch(rec.insn_type):
             with m.Case(InternalOp.OP_ADD):
 
-                comb += Assert(Cat(o, carry_out) == (a + b + carry_in))
+                comb += Assert(Cat(o, ca_o) == (a + b + ca_in))
 
-                # CA32 - XXX note this fails! replace with carry_in and it works
-                comb += Assert((a[0:32] + b[0:32] + carry_in)[32]
-                               == carry_out32)
+                # CA32 - XXX note this fails! replace with ca_in and it works
+                comb += Assert((a[0:32] + b[0:32] + ca_in)[32] == ca32_o)
 
                 # From microwatt execute1.vhdl line 130
-                comb += Assert(ov_out == ((carry_out ^ o[-1]) &
-                                          ~(a[-1] ^ b[-1])))
-                comb += Assert(ov_out32 == ((carry_out32 ^ o[31]) &
-                                            ~(a[31] ^ b[31])))
+                comb += Assert(ov_o == ((ca_o ^ o[-1]) & ~(a[-1] ^ b[-1])))
+                comb += Assert(ov32_o == ((ca32_o ^ o[31]) & ~(a[31] ^ b[31])))
+
             with m.Case(InternalOp.OP_EXTS):
                 for i in [1, 2, 4]:
                     with m.If(rec.data_len == i):
                         comb += Assert(o[0:i*8] == a[0:i*8])
                         comb += Assert(o[i*8:64] == Repl(a[i*8-1], 64-(i*8)))
+
             with m.Case(InternalOp.OP_CMP):
                 # CMP is defined as not taking in carry
-                comb += Assume(carry_in == 0)
+                comb += Assume(ca_in == 0)
                 comb += Assert(o == (a+b)[0:64])
 
             with m.Case(InternalOp.OP_CMPEQB):
-- 
2.30.2