move simple_popcount out of class (does not use any class state)

diff --git a/src/soc/fu/logical/formal/proof_main_stage.py b/src/soc/fu/logical/formal/proof_main_stage.py
index 708d732d5a8a4369b3e353f1d92ae081d3f3fb40..6cb31ead0a045a8f059a712fb969e72dcee5503d 100644 (file)
--- a/src/soc/fu/logical/formal/proof_main_stage.py
+++ b/src/soc/fu/logical/formal/proof_main_stage.py
@@ -20,6 +20,16 @@ from soc.decoder.power_enums import InternalOp
 import unittest
 
 
+def simple_popcount(sig, width):
+    """simple, naive (and obvious) popcount.
+    formal verification does not to be fast: it does have to be correct
+    """
+    result = 0
+    for i in range(width):
+        result = result + sig[i]
+    return result
+
+
 # This defines a module to drive the device under test and assert
 # properties about its outputs
 class Driver(Elaboratable):
@@ -27,12 +37,6 @@ class Driver(Elaboratable):
         # inputs and outputs
         pass
 
-    def popcount(self, sig, width):
-        result = 0
-        for i in range(width):
-            result = result + sig[i]
-        return result
-
     def elaborate(self, platform):
         m = Module()
         comb = m.d.comb
@@ -87,15 +91,15 @@ class Driver(Elaboratable):
 
             with m.Case(InternalOp.OP_POPCNT):
                 with m.If(rec.data_len == 8):
-                    comb += Assert(o == self.popcount(a, 64))
+                    comb += Assert(o == simple_popcount(a, 64))
                 with m.If(rec.data_len == 4):
                     for i in range(2):
                         slc = slice(i*32, (i+1)*32)
-                        comb += Assert(o[slc] == self.popcount(a[slc], 32))
+                        comb += Assert(o[slc] == simple_popcount(a[slc], 32))
                 with m.If(rec.data_len == 1):
                     for i in range(8):
                         slc = slice(i*8, (i+1)*8)
-                        comb += Assert(o[slc] == self.popcount(a[slc], 8))
+                        comb += Assert(o[slc] == simple_popcount(a[slc], 8))
 
             with m.Case(InternalOp.OP_PRTY):
                 with m.If(rec.data_len == 8):