Formally verify OP_POPCNT

diff --git a/src/soc/fu/logical/formal/proof_main_stage.py b/src/soc/fu/logical/formal/proof_main_stage.py
index 277575dcc9fec50d401dc20b4b2acb498837dccf..99c88eebd47b2864206609eb2f3258ded1679b9b 100644 (file)
--- a/src/soc/fu/logical/formal/proof_main_stage.py
+++ b/src/soc/fu/logical/formal/proof_main_stage.py
@@ -21,9 +21,9 @@ class Driver(Elaboratable):
         # inputs and outputs
         pass
 
-    def popcount(self, sig):
+    def popcount(self, sig, width):
         result = 0
-        for i in range(sig.width):
+        for i in range(width):
             result = result + sig[i]
         return result
 
@@ -79,9 +79,17 @@ class Driver(Elaboratable):
                 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))
+                    comb += Assert(dut.o.o == self.popcount(a, 64))
+                with m.If(rec.data_len == 4):
+
+                    for i in range(2):
+                        comb += Assert(dut.o.o[i*32:(i+1)*32] ==
+                                       self.popcount(a[i*32:(i+1)*32], 32))
+                with m.If(rec.data_len == 1):
+                    for i in range(8):
+                        comb += Assert(dut.o.o[i*8:(i+1)*8] ==
+                                       self.popcount(a[i*8:(i+1)*8], 8))
 
 
         return m

diff --git a/src/soc/fu/logical/main_stage.py b/src/soc/fu/logical/main_stage.py
index 27167ef079bf82fb9df202bb68fe121ff7b47e97..9c223ddceaa979363c21341f2d9f721e347da5ea 100644 (file)
--- a/src/soc/fu/logical/main_stage.py
+++ b/src/soc/fu/logical/main_stage.py
@@ -20,7 +20,8 @@ from soc.decoder.power_fieldsn import SignalBitRange
 def array_of(count, bitwidth):
     res = []
     for i in range(count):
-        res.append(Signal(bitwidth, reset_less=True))
+        res.append(Signal(bitwidth, reset_less=True,
+                          name=f"pop_{bitwidth}_{i}"))
     return res
 
 
@@ -82,14 +83,14 @@ class LogicalMainStage(PipeModBase):
                         comb += dst[i].eq(Cat(src[stt], Const(0, 1)) +
                                           Cat(src[end], Const(0, 1)))
                 # decode operation length
-                with m.If(op.data_len[2:4] == 0b00):
+                with m.If(op.data_len == 1):
                     # popcntb - pack 8x 4-bit answers into output
                     for i in range(8):
-                        comb += o[i*8:i*8+4].eq(pc8[i])
-                with m.Elif(op.data_len[3] == 0):
+                        comb += o[i*8:(i+1)*8].eq(pc8[i])
+                with m.Elif(op.data_len == 4):
                     # popcntw - pack 2x 5-bit answers into output
                     for i in range(2):
-                        comb += o[i*32:i*32+5].eq(pc32[i])
+                        comb += o[i*32:(i+1)*32].eq(pc32[i])
                 with m.Else():
                     # popcntd - put 1x 6-bit answer into output
                     comb += o.eq(popcnt[0])