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!