Global Sources
EE Times-Asia
Stay in touch with EE Times Asia
EE Times-Asia > EDA/IP

Cadence formal analysis claims ease of use

Posted: 04 May 2005 ?? ?Print Version ?Bookmark and Share

Keywords:cadence design systems? formal verifier? tool? ic design? rtl code?

Cadence Design Systems is introducing this week Incisive Formal Verifier, a tool that aims to make it easy for IC designers verify assertions in RTL code.

Cadence has had formal analysis offerings in the past, but Incisive Formal Verifier is the company's "first integrated solution with a complete methodology and flow," said Michal Siwinski, product marketing director for Cadence's Incisive group.

What's distinctive about Incisive Formal Verifier, according to Siwinski, is its ease of use and rapid adoption by design teams. "Formal analysis used to be for people more specialized in formal," he said. "We took a completely different attitude. This is formal analysis for every design and verification engineerit's intended to be for the masses."

Formal analysis is primarily intended for block-level analysis in the early stages of verification. The input to Incisive Formal Verifier consists of RTL code plus properties. These may be utilized as assertions, which are properties that are verified for correctness, or assumptions, which are properties on block interfaces that serve as constraints.

Incisive Formal Verifier accepts Property Specification Language (PSL) and SystemVerilog assertions, along with Open Verification Library (OVL) assertions. The same assertions can be used across the Incisive platform for simulation, emulation and acceleration. The tool performs some "lint" checking to make sure assertions are valid, and keeps track of which assertions have been proven.

The tool has a number of formal analysis engines, including various types of binary decision diagram (BDD), automatic test pattern generation (ATPG), and SAT solver engines. The selection is automatic and invisible to the user.

A "pass" result means the assertion has exhaustively verified. A "fail" result means the tool found a violation, for which it will generate a waveform for debugging. Finally, the tool may provide a "proof radius" if it can neither find a violation or exhaustively verify a property. In this case, users can increase the effort and try again.

Siwinski said that a dozen or so companies are already using Incisive Formal Verifier in production flows, and Cadence named Siemens and ST Microelectronics as customers. The tool is available now starting at $120,000 for a one-year time based license.

- Richard Goering

EE Times

Article Comments - Cadence formal analysis claims ease ...
*? You can enter [0] more charecters.
*Verify code:


Visit Asia Webinars to learn about the latest in technology and get practical design tips.

Back to Top