Anaheim, Calif. - Functional-verification technology, including both formal and simulation techniques, will appear from several vendors at the 40th Design Automation Conference here next week. Vendors that will come to the conference claiming new approaches or updates include 0-In Design Automation, Aptix, Jasper Design Automation, Novas Software, ProDesign and Synopsys.
This week, 0-In Design will announce a "unified coverage" metric called structural coverage, an implementation-specific approach complementary to functional coverage. The San Jose, Calif., company claims this is the first metric to measure verification in both simulation and formal verification.
Richard Ho, chief architect at 0-In, said that structural coverage seeks to answer three questions: where assertion checkers are needed, whether checkers are exercised in simulation and how good a job formal verification has done.
There are three types of structural coverage, and 0-In introduced one of these-simulation structural coverage-in 2001. This technique reports how well testbenches exercise corner cases, directly linking functional coverage to error checking with assertions.
New this week are two additional types-static structural coverage, which identifies places in register-transfer-level code that don't have good coverage or assertion monitoring, and formal structural coverage, which assesses the amount of formal analysis performed from each functional corner case.
Not just lint tool
Static structural coverage works by calculating the minimum sequential distance between each register and an assertion within a checker. It is more than a lint tool, said Ho. "It does a netlist analysis and actually understands the RTL netlist. It has the concept of what registers, arbiters, FIFOs and data paths are."
Formal structural coverage uses the proof radius from the corner case as its metric. The proof radius identifies the number of cycles of exhaustive analysis. "If it says the proof radius is 37, that's 37 cycles in which no input combination at all will trigger a bug," Ho said.
The structural-coverage metrics work with 0-In tools, including 0-In Check, 0-In Search and 0-In Confirm. The metrics are shipping with current releases.
0-In is not the only company casting its eye on both formal verification and simulation. Earlier this month Synopsys Inc. (Mountain View, Calif.) announced Magellan, a "hybrid" tool that combines a formal property-checking capability with the company's VCS Verilog simulator (see May 12, page 45).
By including a simulation engine, Synopsys claims that Magellan can reach thousands of cycles deep into designs and avoid the false-negative errors that have plagued other formal tools.
However, startup Jasper Design Automation Inc. (Mountain View), formerly called Tempus Fugit, is coming to the conference with a "pure" formal tool that does not rely on simulation (see May 19, page 1).
The company's JasperGold is an interactive tool that works from specifications, which are at a higher level than assertions. It employs "state space tunneling" to guide formal proof engines and to overcome the capacity limitations of other approaches.
Another "new" company exhibiting at DAC has actually operated as a service bureau in Bruckmuehl, Germany, since 1981. ProDesign Electronic & CAD Layout GmbH is entering the U.S. market with ChipIt, a line of rapid-prototyping systems that promise high speeds, a "desktop" profile and low costs.
Marketing manager Gunnar Scholl said that ProDesign realized that many customers cannot afford expensive emulation systems-and that those systems work at relatively low frequencies. "Therefore, ProDesign decided to develop a compact and transportable verification system that allows high frequencies and some visibility of the internal signals for an attractive price," Scholl said.
ChipIt systems provide both rapid prototyping and in-circuit emulation, although they're really high-speed rapid-prototyping tools, Scholl said. He noted that ChipIt provides a system clock up to 200 MHz and offers a scalable solution from a single FPGA PCI board with 2 million FPGA gates to the newest ChipIt Platinum Edition, which goes up to 144 million FPGA gates.
Third-party partitioning
ChipIt platforms come with configuration software, but partitioning into FPGAs is handled by third-party software, such as Synplicity's Certify program. The ChipIT Gold platform, which handles up to 16 million FPGA gates, is priced from $25,000 to $55,000; ChipIt Platinum starts at $85,000.
The ChipIt platforms compete against rapid-prototyping systems from Aptix Corp. (San Jose), which this week will announce release 5.0 of its software for its System Explorer and SiS platforms. The release, available now, supports TCL scripting, improved probing and triggering, and new hardware self-test.
A flexible probe-assignment technique lets users instrument probes during mapping to eliminate lengthy place and route times. An improved logic optimizer claims to provide new partitioning options to reduce the number of FPGAs and to increase system speed. Aptix claims a 70 percent time reduction for internal probing. The Aptix rapid-prototyping systems start at $60,000.
Better debugging
Novas Software Inc. (San Jose) will announce enhancements to its Debussy debugging system and Verdi behavioral-based debugging system this week. These include database upgrades that are said to use less memory and to double the performance of many debugging operations. Novas has also added new clock tree and timing debug features.
An optimized format developed for Novas' proprietary fast-signal database stores results from verification tools in files that are as much as 50 percent smaller and faster for data extraction, reload and annotation tasks, according to the company.
New clock tree debug and analysis features let engineers easily find clock sources, extract and highlight clock domains, and detect and check clock domain crossings. Users can also import PrimeTime timing-analysis reports into Debussy and Verdi.
Novas will also announce that its debug systems will support Accellera's Property Specification Language for assertion-based verification by the end of this year and the SystemVerilog 3.0 specification by the second half of this year.
