Re: [vhdl-200x] Meeting Reminder: August 11, 8 am Pacific

From: David G. Koontz <>
Date: Wed Aug 10 2011 - 23:20:06 PDT

On 11/08/11 4:07 AM, Jim Lewis wrote:

> You made a claim. I just wanted to see if you could back
> it up with any facts and/or examples. I would like to see
> if the issues still apply in the approach I have in mind.

I went and found the text I was counting on as a supposition and I was in
error. After doing some reading on the application of constraint
programming and solvers to EDA it appears there are two advantages in using
a solver.

First, it's use reflects formal verification, the constraints are usually
derived directly from models being verified. Second, the back and step like
mechanisms used to search for answers within constraints reflect the sort of
domain expert equivalent thinking that would go into a procedural
randomization implementation, which would still have to be shown to be
formally correct (that you didn't make mistakes in it).

A couple of other things to note, the solver used in System Verilog was
noted to be somewhat slow, there's a couple of guys who went around
demonstrating you could be smart doing procedural randomization to beat it,
using the same sort of techniques you'd use to speed up a solver, you anchor
a variable in an known solution space, then maybe anchor another one... It
reduces the number of operations for both.

Not requiring a knowledgeable designer be involved in writing a testbench
can be a win from the EDA industries point of view, reducing the overall
requirement for design expertise in doing verification (and those
consultants teaching you how to do anchoring now can switch to teaching how
to use solvers).

Solvers can also find relationships across time which immediately set me to
thinking about the e language and musing about setting a solver to discover
a an opcode set for a small processor.

There are literally dozens of solvers floating around and they don't seem so

This wouldn't be the same approach you hinted about in 2007, would it?

This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Wed Aug 10 23:20:41 2011

This archive was generated by hypermail 2.1.8 : Wed Aug 10 2011 - 23:21:15 PDT