On Thursday 29 April 2004 12:09 pm, Darryl Dieckman wrote:
[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/