From 3b91483b1d375eacdf44ee9e6e7504c036cb02c4 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Wed, 20 May 2020 13:04:43 -0400 Subject: [PATCH] Use overflow definition from microwatt --- src/soc/fu/alu/formal/proof_main_stage.py | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py index 52237aeb..6e6b1c85 100644 --- a/src/soc/fu/alu/formal/proof_main_stage.py +++ b/src/soc/fu/alu/formal/proof_main_stage.py @@ -80,14 +80,11 @@ class Driver(Elaboratable): 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) + # 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]))) with m.Case(InternalOp.OP_EXTS): for i in [1, 2, 4]: with m.If(rec.data_len == i): -- 2.30.2