Wednesday Night Hack #9 - Generation of constrained random stimulus using python-constraint with bit-level approach

One of the issues faced my in last experiment with constraint programming for random stimulus generation was that the constraint solver library only accepted input variables of finite domain.  As it turns out, all available constraint solvers share this same constraint.  The state space explodes when specifying 16-bit variables and it became difficult to solve a simple constraint.  For the purpose of stimulus generation, it is absolutely necessary to randomize large payloads;128 or 256 bit wide buses is not uncommon.  One approach is model one 2-bit variable for each bit of the random variable.  As it turns out, it works well.  This is commonly called, if I am not mistaken, a bit level approach.

On some other related notes :

I ordered this book on constraint based verification.  I suspect it will heavy on the computer science, but for $17.99 I couldn't pass it up.  I will give it a quick read.

Also, I stumbled on this web site: http://www.personalkanban.com/ - be forewarned, it's new "agey", similar concepts to "GTD".  Well worth a read through if you are interested in personal growth.  Quoting: "Personal Kanban gives us clarity in our work and our lives by visualizing those tasks, expectations, and commitments we have and helping us prioritize and complete.  With only two simple rules, visualize your work and limit your work in progress."

Without further ado, here is the source code to tonight's experiment.  Enjoy!

#!/usr/bin/env python2.7

from constraint import *
from random import seed


class Solver:
    def __init__(self):
        self.solver = Problem()
        self.solver.setSolver(MinConflictsSolver(100))

    def add_variable(self, name, length):
        # Each bit of input variable is in binary domain, internal format is name[bit position]
        variables = ['{}[{}]'.format(name, i) for i in range(length)]
        for variable in variables:
            self.solver.addVariable(variable, [0, 1])

    def add_constraint(self, *args):
        self.solver.addConstraint(*args)

    def randomize(self):
        self.solution = self.solver.getSolution()

    def get_variable(self, name):
        # generate decimal representation from internal bitwise representation
        remap = 0
        for variable in self.solution:
            if name in variable:
                index = variable.replace('[', '_').replace(']', '').split('_')[1]
                remap += 2**int(index) * int(self.solution[variable])
        return remap

#seed(1)  # fix random seed, if ndeed

solver = Solver()  # init solver object

solver.add_variable('xx', 32)  # rand bit [31:0] xx
solver.add_variable('yy', 15)  # rand bit [15:0] yy

# x is EVEN
solver.add_constraint(lambda x: x == 0, ['xx[0]'])  # x is EVEN
# y is ODD
solver.add_constraint(lambda x: x == 1, ['yy[0]'])  # y is EVEN

# solve the problem
solver.randomize()

# return random solutions for variable xx and yy
print(solver.get_variable('xx'))
print(solver.get_variable('yy'))