Domain Crossing Verification Needs Continue to Grow

Clock domain crossing (CDC) analysis has been around for many years, initially as special checks in verification or static timing analysis, but it fairly quickly diverged into specialized tools focused just on this problem. CDC checks are important because (a) you can lose data or even lock up at, or downstream of a poorly-handled crossing, (b) deciding whether a crossing is well- or poorly-handled is not always easy, (c) this is the kind of problem you really need to check completely, which requires static rather than dynamic analysis and (d) there are a lot more of these things scattered across modern designs.

On that last point, while the number of clock domains in a typical design seems to be growing more or less linearly over time, the number of clock domain crossings is growing exponentially. And these are now quite strongly interrelated with power domain crossings and reset domain crossings. Which means you can’t just look at the clocks anymore. You have to look at the clock intent, the power intent and the reset intent and how those propagate through the design to be sure you are going to catch all potential crossing problems.

So you do static analysis, looking at SDC for clock definitions, UPF for power intent and maybe a side-file for reset definitions. That finds the crossings and, with some additional structural analysis, can check if you are using approved structures to handle crossings. But it doesn’t check functional correctness, say on a fast-to-slow crossing, so you add formal checks, which completely prove the functional correctness or otherwise of the crossing. Except when they don’t. Formal, as we know, doesn’t always quite live up to its “completeness” billing. Sometimes it is only able to partially prove an assertion; sometimes it can prove (or partially prove) an assertion only if you supply a number of constraining assumptions. So you need to be able to fall back easily to simulation to test within expected use-models that the partial assertion and assumptions remain valid. This is generally called a hybrid flow – mixing formal and simulation verification of crossings.

And then there are those pesky resets. Poorly-managed reset domain crossings are becoming a significant problem in their own right. This arises in part through use of asynchronous resets. While many designers suggest async resets should be avoided, sometimes you have no choice, especially if you can’t be guaranteed an active clock when the reset is applied (if the clock is gated, for example). In the example below, if RESET1 is released close to when CLK is turned on and RESET2 is not active, there is potential for metastability in the second flop, for pretty much the same reason you might get metastability between two flops with asynchronous clocks.

This class of problem is amplified by the growing number of reset domains (and even more rapidly growing reset domain crossings) found in modern devices – cold resets, warm resets, resets which skip configuration registers, resets which skip retention registers and more. And then there are the complex sequences through which these domains must be controlled. Reset domain crossing (RDC) checks are starting to appear and I’m sure we’ll see more growth in static /formal techniques for this area.

And then there’s the perennial question of coverage. This is a part of verification, so you really want to know how completely you covered these areas. Definitions and techniques for formal coverage are still emerging, but it appears some initial approaches to coverage are already possible, per class of crossing-problem. This is an important step in quantifying the degree to which domain crossing checks have been proven, which is obviously significant for overall confidence in verification completeness and may become increasingly important in safety-critical applications.

Synopsys dominates (by a wide margin) the domain-crossing checking market with their SpyGlass CDC product, so you probably should stay in touch with what they’re doing and where they’re going. You can learn more from THIS WEBINAR.

More articles by Bernard…