Commentary: 0-In eases verification tasks

0-In eases verification tasks
By Clive Maxfield, EEdesign
February 17, 2003 (1:34 p.m. EST)
URL: http://www.eetimes.com/story/OEG20030217S0025

Some areas of EDA have largely reached maturity and appear somewhat old and staid, whilst others are still young, rambunctious, and full of fun and vitality. In the case of tools like simulation, synthesis, and place-and-route, for example, the best we can typically hope for these days is to see some small incremental advance every now-and-again. By comparison, formal verification (both static and dynamic) currently seems to be one of the hottest areas for technological advances and is charging forth in leaps and bounds.

0-In announce V2.0 of ABV

Ever since I first plunged into the mire of assertions and formal verification, I've had something of a soft-spot for 0-In and their Assertion-Based Verification (ABV) technology.

First of all I like the fact that they are based on the concept of using pragmas (commented directives) in the RTL, which doe sn't require you to change your core RTL code. Second, I like the way in which their tools infer things like bus widths on-the-fly, which saves you having to specify them explicitly (and then subsequently have to modify these specifications when things change). And third, I like the way in which 0-In are simulator, testbench, results viewer, and GUI-neutral, which means that you can drop their tools into your design environment with the minimum of hassle and disruption.

0-In's original ABV suite comprised a number of elements:

CheckerWare: Assertion IP in the form of a comprehensive library of checkers and monitors.

0-In Check: Assertion simulation that enables the use of complex assertions and protocol monitors in simulation through easy specification, assertion management, and links to debugging tools.

0-In Search: Dynamic formal verification that amplifies hand-written directed tests using exhaustive formal algorithms to find bugs missed in simulation.

Well, in release 2.0 of the ir ABV that was announced late last month, 0-In unveiled two new tools:

0-In Checklist: Automated RTL checker that find common RTL errors, simulation-to-synthesis mismatch errors, and clock-domain crossing errors.

0-In Confirm: A new static formal verification tool that can perform deep searches to find bugs, thereby saving billions of simulation cycles

0-In claim that this new suite allows designers to systematically and efficiently detect a variety of key bug types that are difficult to identify using traditional verification techniques:

Control logic corner-case bugs

Clock domain crossing problems involving data loss across clock domains

Interface bugs (both in compliance and implementation omissions)

Low-probability, data-dependent bugs

Simulation-to-synthesis mismatches

The two points that really grabbed my attention here are the Clock Domain Crossing (CDC) bugs and the low-probability data-dependent bugs. In the case of CDC considerations, the number o f clock domains employed by some designs has ramped up dramatically over the last year or so (I recently heard of a design with 300 clock domains — this may be old news to you, but it certainly made my eyes water, let me tell you).

The answer here is the new 0-In Checklist tool, which analyses the RTL, detects potential problem areas, and automatically generates CDC-based checks that will run in simulation and in formal verification.

One of the things I really hate about a lot of tools is that they overwhelm you with information. I remember using Static Timing Analysis (STA) tools that would bury you under reams of computer printout listing tens of thousands of false-positive errors. The end result was that you often missed real errors that were hiding in the morass of meaningless messages.

Well 0-In seem to have cracked this problem, because at every level their tests result in a Pass, Fail, or Ambiguous condition. In the case of the Ambiguous results (which equate to false positives), thes e are automatically promoted to the next level of verification without you having to worry about them. The ability to limit reports to only real errors is a real "Cool Beans" aspect of the system as far as I'm concerned.

In the case of low-probability, data-dependent bugs, you might potentially have one problem pattern on a 64-bit wide bus, which means that you have to hunt this "needle" down in a "haystack" consisting of 2 to the power of 64 "straws"! Some of these data-dependent bugs require you to try a lot of initial states (this class is addressed by 0-In Search), while others require you to go down-and-deep (this class is addressed by the new 0-In Confirm). The beauty once again is that any ambiguous results from 0-In Search are automatically promoted to 0-In Confirm for further analysis.

I love this automatic promotion concept. In a conversation with some of the guys and gals from 0-In, they told me that their philosophy is to identify and detect bugs with the least amount of human and compute r effort — and that certainly works for me. So it's another "Cool Beans" for 0-In from me. Until next time, have a good one!