From 48306a1eb31536b154342b34b8db2b82f229a0d9 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Wed, 20 May 2020 09:52:05 -0400 Subject: [PATCH] Add 32 bit carry handling to alu --- src/soc/fu/alu/formal/proof_main_stage.py | 10 +++++++++- src/soc/fu/alu/main_stage.py | 5 +++-- src/soc/fu/alu/test/test_pipe_caller.py | 2 +- 3 files changed, 13 insertions(+), 4 deletions(-) diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py index 601a4875..33c97809 100644 --- a/src/soc/fu/alu/formal/proof_main_stage.py +++ b/src/soc/fu/alu/formal/proof_main_stage.py @@ -41,7 +41,8 @@ class Driver(Elaboratable): b = dut.i.b carry_in = dut.i.carry_in so_in = dut.i.so - carry_out = dut.o.carry_out + carry_out = dut.o.xer_co.data[0] + carry_out32 = dut.o.xer_co.data[1] o = dut.o.o # setup random inputs @@ -64,11 +65,18 @@ class Driver(Elaboratable): comb += a_signed.eq(a) comb += a_signed_32.eq(a[0:32]) + 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)) + # CA32 + comb += Assert((a[0:32] + b[0:32] + carry_in)[32] + == carry_out32) + return m diff --git a/src/soc/fu/alu/main_stage.py b/src/soc/fu/alu/main_stage.py index fb0ed939..b2b2612a 100644 --- a/src/soc/fu/alu/main_stage.py +++ b/src/soc/fu/alu/main_stage.py @@ -62,9 +62,10 @@ class ALUMainStage(PipeModBase): comb += o.eq(add_output[1:-1]) comb += carry_out.data[0].eq(add_output[-1]) # XER.CO - # XXX no! wrongggg, see microwatt OP_ADD code + # see microwatt OP_ADD code # https://bugs.libre-soc.org/show_bug.cgi?id=319#c5 - comb += carry_out.data[1].eq(add_output[-1]) # XER.CO32 + comb += carry_out.data[1].eq(add_output[33] ^ + (a[32] ^ b[32])) # XER.CO32 #### exts (sign-extend) #### with m.Case(InternalOp.OP_EXTS): diff --git a/src/soc/fu/alu/test/test_pipe_caller.py b/src/soc/fu/alu/test/test_pipe_caller.py index 935e272f..4f682f67 100644 --- a/src/soc/fu/alu/test/test_pipe_caller.py +++ b/src/soc/fu/alu/test/test_pipe_caller.py @@ -267,7 +267,7 @@ class TestRunner(FHDLTestCase): self.assertEqual(expected_carry, real_carry, code) expected_carry32 = 1 if sim.spr['XER'][XER_bits['CA32']] else 0 real_carry32 = yield alu.n.data_o.xer_co.data[1] # XXX CO32 - self.assertEqual(expected_carry, real_carry, code) + self.assertEqual(expected_carry32, real_carry32, code) -- 2.30.2