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
