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 960342ce4d5ec100c004c658a1d33b995e54c4f0..52237aeb6b3ab722abe8d66b24d7efb81dc11273 100644 (file)
--- 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 2173814465efa1b014248849c4ee1d240e226c30..88f268ada3f2f471dbd115f1974e2127cbf943c1 100644 (file)
--- 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):