Fix bug with popcntd

Popcount on -1 (64 ones) would overflow the signal holding the sum,
giving 0 instead of 64

diff --git a/src/soc/fu/logical/formal/proof_main_stage.py b/src/soc/fu/logical/formal/proof_main_stage.py
index 804643df5a01160c6996bae3fe7d8c89133ecf16..277575dcc9fec50d401dc20b4b2acb498837dccf 100644 (file)
--- 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 d8c3b2fb56cc2a3ba25e0882e434974811317244..27167ef079bf82fb9df202bb68fe121ff7b47e97 100644 (file)
--- 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)