From: Michael Nolan <mtnolan2640@gmail.com>
Date: Wed, 20 May 2020 15:04:57 +0000 (-0400)
Subject: Formally verify OP_POPCNT
X-Git-Tag: div_pipeline~1034
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0bf0e9b743aac05f25669a0891c638958f01360c;p=soc.git

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 277575dc..99c88eeb 100644
--- 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 27167ef0..9c223ddc 100644
--- 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])