From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Thu, 28 May 2020 23:23:05 +0000 (+0100)
Subject: move simple_popcount out of class (does not use any class state)
X-Git-Tag: div_pipeline~759
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=88ac42cce1f43fb8a9e8734c50be3cf2f77632a1;p=soc.git

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 708d732d..6cb31ead 100644
--- 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):