Overview of OneSpin's Verification Tutorials @ DAC 2010
At DAC 2010 in Anaheim, June 14-16, OneSpin presents recent advances in its 360 MV family of formal assertion-based verification (ABV) solutions. 360 MV covers formal ABV applications from early automatic RTL analysis and block-level verification all the way to gap-free verification for SystemVerilog assertions (SVA).It covers applications for formal ABV newcomers to get started quickly and provides a wide range of unique features including Operational ABV, exhaustive coverage analysis, and 4-state-logic exhaustive X-analysis and X-verification that are not available in other formal tools.
Tutorials: OneSpin offers four formal assertion-based verification (ABV) tutorials at DAC 2010
Where: Anaheim Convention Center, Booth 1311
When: Monday June 14 – Wednesday June 16, 9:00 am – 6:00 pm
Duration: Tutorials are run every hour and are 45 minutes including demos of the presented concepts on real life designs
Raffle: Every tutorial attendee enters the raffle for an Apple iPad
1. 'Preventing X-related Bugs through Exhaustive 4-state Formal Analysis'
The use of unknown values (X's) can improve RTL verification and synthesis. But unexpected X propagation in simulation can mask bugs causing functional errors in silicon. This tutorial presents OneSpin's most recent enhancement of 360 MV for 4-state-logic formal analysis, where signals can explicitly become X and Z – extending the 0/1-models commonly used in formal verification tools. This X-aware formal analysis enables an exhaustive pre-synthesis X-analysis and X-verification, detecting, e.g., unintended X-propagation caused by uninitialized registers and ensuring safe use of X's for verification and synthesis optimization in general.2. 'Operational ABV + Formal Coverage Analysis = 100% functional coverage'
In this tutorial we present a verification methodology called Operational ABV. Operational ABV simplifies verification planning, eases assertion writing working from timing diagrams and is the key for an exhaustive coverage analysis ensuring that no design behavior is missed during verification. The exhaustive coverage analysis automatically uncovers holes in the verification plan, detects unverified design functionality, and finds errors and omissions in design specifications. It generates diagnosis information guiding the user in writing additional assertions to close verification holes. An AHB2Wishbone bus bridge is used to demonstrate how Operational ABV and exhaustive coverage analysis enable engineers to efficiently achieve 100% functional coverage for their critical modules and IP.3. 'Verifying Processors Beyond Doubt'
In this tutorial we show how to apply Operational ABV and exhaustive coverage analysis to verify processors – ensuring that no processor behavior is missed during verification. The approach allows to formally verify processors at the level of their instruction set architecture, using Operational SVA to capture the expected behavior of complete processor instructions by means of SystemVerilog assertion (SVA). It is demonstrated how exhaustive coverage analysis automatically detects any remaining verification holes.4. 'Exhaustive Verification of Complex Arithmetic'
Verification of complex arithmetic is typically considered tedious and hard for formal ABV. We present recent improvements for exhaustive verification of arithmetic and demonstrate these improvements using 'Ultimate CRC', an FPU example as well as a 'Maximum a Posteriori' channel encoder/decoder.If you would like to attend one of those tutorials just visit OneSpin at booth 1311. If you would like to register up-front just send an e-mail to info@onespin-solutions.com