0-In revs assertion-based verification
0-In revs assertion-based verification
By Richard Goering, EE Times
April 19, 2002 (6:28 p.m. EST)
URL: http://www.eetimes.com/story/OEG20020419S0102
SAN JOSE, Calif. Claiming breakthrough technology that can accelerate assertion-based verification, 0-In Design Automation is revealing details about its "deep dynamic formal verification" technology, which will be used in a product to be introduced later this year. The company already offers dynamic formal verification with 0-In Search, which uses mathematical techniques to generate alternative sequences to existing simulation tests. Deep dynamic verification can generate much longer sequences; 0-In claims it can exhaustively analyze circuit behavior for 50 to 150 clock cycles from a given simulation state. "This is powerful new technology that we think will change the way people think about assertion-based verification," said Emil Girczyc, president and chief executive officer of 0-In. Girczyc said that dynamic formal verification today can search a lot of seeds or simulation states ; but not go to a lot of depth. 0-In Search, for example, can launch searches from tens of thousands of seeds, but it generally has a proof radius of less than 10 clock cycles. Complex assertions The new technology is much more computationally intensive. While 0-In Search might take "hundredths" of a second to search a simulation state, deep dynamic verification might take thousands of seconds, Girczyc said. It is thus intended for use with only a few seeds, and for the most complex of assertions. But the depth is unprecedented, Girczyc said. If a circuit has 300 inputs, that translates into 1090 patterns each cycle; a proof radius of 100 cycles is equivalent to 109,000 cycles of simulation. That's why 0-In sees deep dynamic verification as "tantamount to a full proof," he said. At present, Girczyc said, the deep dynamic approach works on blocks of up to several hundred thousand gates. It can be used throughout most of the verification cycle, including "posts ilicon triage," he said. What makes the new technology possible is progress with bounded model-checking algorithms, said Curt Widdoes, 0-In chairman and CTO. Widdoes said 0-In leveraged research from Princeton University but refined that work on its own. Girczyc noted that dynamic and deep dynamic verification can start from any simulation state, including reset. For example, a search could be launched after simulation fills a FIFO. With the deep approach, he said, customers will likely fire the search from reset and three to seven other "interesting places" in the circuit thus looking at perhaps 10 simulation seeds, rather than tens of thousands. As with dynamic verification, Girczyc said, designers using deep dynamic verification set forth assertions that are used as both monitors and constraints. With the deep approach, however, more care must be taken to get the constraints accurate. Widdoes said 0-In expects customers to use static formal verification first, to prove some properti es with constraints. But for assertions with "indeterminate" answers, users will then launch dynamic formal verification and "turn up the volume" to the deep dynamic approach for the most complex of assertions. As of today, deep dynamic formal verification and all 0-In technology works only with that company's proprietary assertion format. But 0-In will support whatever standard emerges from the Accellera standards organization, Girczyc said. The company is not currently supporting OpenVera 2.0, the assertion language offering from Synopsys Inc. with cooperation from Intel Corp. An exclusive feature article describing how deep dynamic formal verification fits into the assertion-based verification flow is available at www.EEdesign.com.
Related News
- Cadence and 0-In Collaborate to Deliver Superior Assertion-Based Verification
- 0-In Granted Key Patent in Assertion-Based Verification
- 0-In Demonstrates the Value of Assertion-Based Verification (ABV) throughout the Design Cycle at the Design Automation Conference
- Momentum Builds for Assertion-Based Verification: 0-In Welcomes Averant and Bridges2Silicon as Check-In Partners
- Renesas Technology Integrates Mentor Graphics 0-In Assertion Synthesis for Assertion Based Verification Flow
Breaking News
- Frontgrade Gaisler Unveils GR716B, a New Standard in Space-Grade Microcontrollers
- Blueshift Memory launches BlueFive processor, accelerating computation by up to 50 times and saving up to 65% energy
- Eliyan Ports Industry's Highest Performing PHY to Samsung Foundry SF4X Process Node, Achieving up to 40 Gbps Bandwidth at Unprecedented Power Levels with UCIe-Compliant Chiplet Interconnect Technology
- CXL Fabless Startup Panmnesia Secures Over $60M in Series A Funding, Aiming to Lead the CXL Switch Silicon Chip and CXL IP
- Cadence Unveils Arm-Based System Chiplet
Most Popular
- Cadence Unveils Arm-Based System Chiplet
- CXL Fabless Startup Panmnesia Secures Over $60M in Series A Funding, Aiming to Lead the CXL Switch Silicon Chip and CXL IP
- Esperanto Technologies and NEC Cooperate on Initiative to Advance Next Generation RISC-V Chips and Software Solutions for HPC
- Eliyan Ports Industry's Highest Performing PHY to Samsung Foundry SF4X Process Node, Achieving up to 40 Gbps Bandwidth at Unprecedented Power Levels with UCIe-Compliant Chiplet Interconnect Technology
- Arteris Selected by GigaDevice for Development in Next-Generation Automotive SoC With Enhanced FuSa Standards
E-mail This Article | Printer-Friendly Page |