From 4f001ab2ae1133e275d782676248a7a9e14f801b Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Wed, 20 May 2020 12:44:46 -0400 Subject: [PATCH] Add overflow handling and proof --- src/soc/fu/alu/formal/proof_main_stage.py | 11 +++++++++++ src/soc/fu/alu/main_stage.py | 6 ++++++ 2 files changed, 17 insertions(+) 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): -- 2.30.2