From 88ac42cce1f43fb8a9e8734c50be3cf2f77632a1 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Fri, 29 May 2020 00:23:05 +0100 Subject: [PATCH] move simple_popcount out of class (does not use any class state) --- src/soc/fu/logical/formal/proof_main_stage.py | 22 +++++++++++-------- 1 file changed, 13 insertions(+), 9 deletions(-) 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): -- 2.30.2