Assertions can be thought of as rules that embody the designer's intent, or at least assumptions regarding intent, against which the design can be checked for violations using either simulation, formal verification, or both. Checklist brings assertions to bear in the search for CDC problems.
To begin, it performs netlist analysis to locate asynchronous clock domains and identifies signals that cross back and forth between them. It then performs analyses to determine what kinds of synchronization schemes, if any, are in place to address metastability issues. "There are many standard schemes for synchronization," says Ho, "as well as many homebrewed schemes. What is required is a library of monitors that are customized to each of these particular schemes." The monitors are actually high-level verification intellectual property (IP) used to determine whether or not the synchronization scheme detected by Checklist is implemented properly.
VERIFICATION GOES FORMAL
Assertions can be simulated together with the design to check for complete CDC protocols. "We can provide monitors for those protocols that cannot be deterministically proven in a simple way," says Ho.
These protocol monitors, part of the company's CheckerWare library, can be promoted to more powerful engines within the ABV suite, including 0-In's formal verification algorithms (Fig. 2). In this way, simulation and formal verification team to flush out corner cases of metastability and protocol violations that simulation alone could miss.
0-In's combination of assertion-based verification and formal techniques sets a precedent that, for now, gives it an edge. According to Gary Smith, Gartner Dataquest's chief EDA analyst, V.2.0 of the Assertion-Based Verification Suite is a step in the right direction. "What I really liked is they came out with a suite, which is what's needed in that technology. They've added model checking, which is, in my mind, a sign of maturing," says Smith.
To be sure, V2.0 of the ABV suite adds other capabilities that make it very strong. Its Deep Counter Example (DCE) technology exhaustively verifies assertions using the tool's formal engine to find slippery register-transfer-level (RTL) bugs late in the design cycle. But the CDC error checking, made more thorough than ever before, sets the suite apart and raises the bar. By this June's Design Automation Conference, we'll learn what other verification vendors have up their sleeves to counter this move by 0-In.