In the simulation and verification world, particularly with regard to system-on-a-chip (SoC) design closure, certain fault types have made their way to silicon with greater frequency. Many of today's SoCs contain multiple asynchronous clocks, passing signals and data across those clock domains. This can cause bugs that are almost impossible to track down in simulation. Yet new applications of assertion-based verification coupled with simulation and formal verification are confronting these stubborn problems, which before now often didn't turn up until hardware.
We can understand multiple asynchronous clock domains as any part of an SoC that has an asynchronous clock, or a variable phase relationship to another clock in the design. Two parts of a design may implement derivatives of the same clock, with that clock being divided. Both parts would still be of the same clock domain. Multiple domains occur when two (or more) clocks have phase relationships that vary over time.
Consider the example of a 33-MHz PCI bus interfacing with a 50-MHz system clock. The phase relationships of these clocks will shift against each other. Signals that cross from the 33-MHz bus to segments of the system running on the 50-MHz clock, or vice versa, can pose two verification problems if design isn't approached with the proper care.
The first is metastability, which can arise when register setup and hold times are violated. It occurs when signals cross from one clock domain to the other at an inopportune time. Whenever the data input of a register changes within the setup or hold time of that register's clock edge, its output may reach a value between zero and one. Such an output is said to be metastable. Should a metastable signal be used by downstream logic, errors may occur.
Generally, metastability issues are handled by using data synchronization schemes that condition clock domain-crossing (CDC) signals before they're used by downstream logic. A typical two-register data-synchronization circuit makes it much more likely that the register output will be a zero or one because the first register, R1, has a full clock period to settle to a stable value before it's sampled by R2 (Fig. 1).
A second problem is related to protocols. Another way to transmit multiple CDC signals is to use one CDC signal to handshake with the receiving logic. This ensures that the receiving logic samples the other CDC signals only when they are stable. Such an approach eliminates the need for additional synchronization. Richard Ho, chief architect at 0-In Design Automation (www.0-in.com), notes that the protocol issue with CDC signals occurs when you expect that the receiving side can sample a CDC signal, but the holding side doesn't hold the data long enough. "Or," says Ho, "it might be too fast. It took away the data before the receiving side had a chance to look at it, and that would be a protocol problem in a CDC."
HIT OR MISS Both the metastability and protocol problems that can afflict CDC signals in an SoC may potentially be found in simulation, but it's a hit-or-miss proposition. According to Ho, such errors may or may not show up in functional verification. "It's an ad-hoc, random process," he explains. 0-In has developed a potent combination of assertion-based verification and formal verification to flush out bugs that might not cause simulation to fail, but instead only show up in hardware as intermittent failures.As multiple asynchronous clock domains get more play in SoCs, designers view CDC signals as an increasingly vexing issue. Verifying CDC signals comes down to identifying them and verifying the CDC protocols associated with them.
The company has issued Release V2.0 of its Assertion-Based Verification (ABV) suite, which launches a full-scale assault on CDC verification. New to V.2.0 is a tool called Checklist, the suite's secret weapon in the CDC battle.
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.