Re: gEDA-user: Assertion based verification using VCD and VHDL

["Samuel A. Falvo II" <sam.falvo@falvotech.com>]

On Sunday 02 May 2004 07:48 am, Tom Hawkins wrote:
> There are two formal methods to prove correctness of a low-level
> netlist; they are static timing analysis (STA) and equivalence
> checking (EC).  Unfortunately there are no open-source STA or EC
> tools.  :-(  If you can afford STA and EC (I recommend Conformal),
> you'll never have to run a digital gate-level sim again.

What would be involved with the creation of such tools?  Where can one 
learn more about them?  As someone who is working on a digital design 
project using Icarus Verilog, would something like this kind of tool be 
useful to me?  If so, maybe I can offer my time to kill two birds with 
one stone.

The problem is, I only have a very tenuous level of experience with 
*software* formal methods; though, I would like to learn more about 
formal methods in general.  I believe it was Knuth who once said of a 
piece of code, "Beware: I have not tested this code, but merely have 
proven it."

--
Samuel A. Falvo II