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

[Tom Hawkins <tom@launchbird.com>]

On Thursday 29 April 2004 12:09 pm, Darryl Dieckman wrote:
> Hi,
>
> I am trying to locate an open-source tool chain that I can
> use for assertion based verification of a design.  I have
> read about PSL/Sugar and the Open Verification Library (OVL).
> It looks like OVL would allow me to add verification to
> a VHDL design which would work great while my design is
> in VHDL.
>
> However, my digital design is eventually fabricated as a full
> custom VLSI layout.  I extract SPICE for the design and run
> simulations of the design in SPICE.  I then take the raw output
> from
> the SPICE run and generate a VCD (value change dump) file.
> Currently I use something like GTKWave to visually inspect the
> digital response of the circuit.

[snip]

It sounds like you're tackling two independent issues: functional 
verification and implementation verification.

Functional verification answers the question, "Does my RTL implement 
the intended function?"  Implementation verification answers the 
question, "Now that I've converted my RTL to a lower level (gates, 
transistors, post-layout), was the translation performed correctly, 
i.e. does it meets timing and is it functionally equivalent?"

Assertions (PSL, OVL) help answer the first question by allowing the 
designer to specify system properties such as "If 'req' is high, then 
'ack' should be true on the next clock cycle":

  always (req -> next ack)    // PSL

The properties are verified using simulation or formal methods.  For 
simulation, a tool converts a property into a state-machine to act as 
a monitor.  During simulation, if the property is violated, the 
state-machine posts a failure message.

Model checking is a formal method to mathematically prove a property 
will never be violated.  Unlike simulation, model checking covers 
every possible corner.

For simulations based property assertions, I only know of one 
open-source tool chain.  Confluence (http://www.launchbird.com) has a 
tool called ba2cf, when coupled with another open-source tool, 
ltl2ba, completes the path from temporal properties similar to PSL, 
to assertion monitor state-machines.  Ba2cf is in rough shape, but I 
have a cleaner version that generates Verilog and SystemC monitors. 

For formal verification, there is an open-source model checker called 
NuSMV (http://nusmv.irst.itc.it/).  NuSMV is considered a close 
cousin of Cadence's FormalCheck.  The drawback of NuSMV is it doesn't 
accept HDL as input; you'd have to convert your design by hand.  If 
Confluence is your source code, it can auto-generate VHDL, Verilog, 
and NuSMV, not to mention C.


Implementation verification is a separate topic.  Traditionally this 
has been handled by running RTL test vectors through gate-level 
simulation to check for functional errors or timing violations.  But 
like with any simulation-based approach, you'll always be left 
wondering, "Did my test vectors cover everything?".  Almost always 
the answer is no.

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.

    
-Tom

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