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

[Tom Hawkins <tom@launchbird.com>]

On Sunday 02 May 2004 11:18 am, Samuel A. Falvo II wrote:
> 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.

STA, and path analysis in general, is much easier to solve than 
equivalence checking.  STA is a fairily linear algorithm; it involves 
traversing each path between registers, accumulating delay values for 
each combinatorial element.  Constraints dictate acceptable delays on 
each path (multi-cycle paths, false paths).  The latest trend in EDA 
is automatic timing constraint generation (FishTail), and timing 
constraint checking (RealIntent, Verplex).  These problems are also 
fairily easy.

Equivalence checking is much harder.  The basic technique involves 
matching state registers between two designs, then proving the 
combinatorial logic cones are equivalent by way of BDDs, SAT, and 
other tricks.

The biggest hurdle is we (the open-source EDA community) don't have a 
standard netlist format to represent RTL and gate-level.  When ever 
someone starts to write a new tool, they get lost in building a 
Verilog parser.  Wouldn't it be cool to have an XML standardized 
netlist format?  It would be the perfect starting point for a wide 
range of tools including:

  - STA
  - Equivalence checking
  - FPGA synthesis
  - Code generation
  - Logic optimization
  - Model checking
  - and so on...


>
> 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."

One of my favorites:

"Program testing can be used to show the presence of bugs, but never 
to show their absence."  -- Dijkstra

-- 
Tom Hawkins
Launchbird Design Systems, Inc.
Home of the Confluence Logic Design Language
http://www.launchbird.com/