From 58c25d7559a0ba7de91a01cfad932d28f9e8275a Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Wed, 20 May 2020 10:49:54 -0400 Subject: [PATCH] Fix bug with popcntd Popcount on -1 (64 ones) would overflow the signal holding the sum, giving 0 instead of 64 --- src/soc/fu/logical/formal/proof_main_stage.py | 13 ++++++++++++- src/soc/fu/logical/main_stage.py | 2 +- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/src/soc/fu/logical/formal/proof_main_stage.py b/src/soc/fu/logical/formal/proof_main_stage.py index 804643df..277575dc 100644 --- a/src/soc/fu/logical/formal/proof_main_stage.py +++ b/src/soc/fu/logical/formal/proof_main_stage.py @@ -21,6 +21,12 @@ class Driver(Elaboratable): # inputs and outputs pass + def popcount(self, sig): + result = 0 + for i in range(sig.width): + result = result + sig[i] + return result + def elaborate(self, platform): m = Module() comb = m.d.comb @@ -41,7 +47,6 @@ class Driver(Elaboratable): b = dut.i.b carry_in = dut.i.carry_in so_in = dut.i.so - carry_out = dut.o.carry_out o = dut.o.o # setup random inputs @@ -73,6 +78,12 @@ class Driver(Elaboratable): with m.Case(InternalOp.OP_XOR): comb += Assert(dut.o.o == a ^ b) + with m.Case(InternalOp.OP_POPCNT): + #comb += Assume(a < ((1<<64)-1)) + with m.If(rec.data_len == 8): + comb += Assert(dut.o.o == self.popcount(a)) + + return m diff --git a/src/soc/fu/logical/main_stage.py b/src/soc/fu/logical/main_stage.py index d8c3b2fb..27167ef0 100644 --- a/src/soc/fu/logical/main_stage.py +++ b/src/soc/fu/logical/main_stage.py @@ -68,7 +68,7 @@ class LogicalMainStage(PipeModBase): # creating arrays big enough to store the sum, each time pc = [a] # QTY32 2-bit (to take 2x 1-bit sums) etc. - work = [(32, 2), (16, 3), (8, 4), (4, 5), (2, 6), (1, 6)] + work = [(32, 2), (16, 3), (8, 4), (4, 5), (2, 6), (1, 7)] for l, b in work: pc.append(array_of(l, b)) pc8 = pc[3] # array of 8 8-bit counts (popcntb) -- 2.30.2