From: Michael Nolan <mtnolan2640@gmail.com>
Date: Wed, 20 May 2020 16:44:46 +0000 (-0400)
Subject: Add overflow handling and proof
X-Git-Tag: div_pipeline~1023
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4f001ab2ae1133e275d782676248a7a9e14f801b;p=soc.git

Add overflow handling and proof
---

diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py
index 960342ce..52237aeb 100644
--- a/src/soc/fu/alu/formal/proof_main_stage.py
+++ b/src/soc/fu/alu/formal/proof_main_stage.py
@@ -44,6 +44,8 @@ class Driver(Elaboratable):
         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]
         o = dut.o.o
 
         # setup random inputs
@@ -77,6 +79,15 @@ class Driver(Elaboratable):
                 # 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)
+
+                with m.If(a[-1] == b[-1]):
+                    comb += Assert(ov_out == (o[-1] != a[-1]))
+                with m.Else():
+                    comb += Assert(ov_out == 0)
+                with m.If(a[31] == b[31]):
+                    comb += Assert(ov_out32 == (o[31] != a[31]))
+                with m.Else():
+                    comb += Assert(ov_out32 == 0)
             with m.Case(InternalOp.OP_EXTS):
                 for i in [1, 2, 4]:
                     with m.If(rec.data_len == i):
diff --git a/src/soc/fu/alu/main_stage.py b/src/soc/fu/alu/main_stage.py
index 21738144..88f268ad 100644
--- a/src/soc/fu/alu/main_stage.py
+++ b/src/soc/fu/alu/main_stage.py
@@ -25,6 +25,7 @@ class ALUMainStage(PipeModBase):
         m = Module()
         comb = m.d.comb
         cry_o, o, cr0 = self.o.xer_ca, self.o.o, self.o.cr0
+        ov_o = self.o.xer_ov
         a, b, cry_i, op = self.i.a, self.i.b, self.i.xer_ca, self.i.ctx.op
 
         # check if op is 32-bit, and get sign bit from operand a
@@ -66,6 +67,11 @@ class ALUMainStage(PipeModBase):
                 # https://bugs.libre-soc.org/show_bug.cgi?id=319#c5
                 comb += cry_o.data[1].eq(add_o[33] ^ (a[32] ^ b[32])) # XER.CO32
 
+                comb += ov_o.data[0].eq((add_o[-2] != a[-1]) &
+                                        (a[-1] == b[-1]))
+                comb += ov_o.data[1].eq((add_o[32] != a[31]) &
+                                        (a[31] == b[31]))
+
             #### exts (sign-extend) ####
             with m.Case(InternalOp.OP_EXTS):
                 with m.If(op.data_len == 1):