Why Can’t You Write My Assertions for Me? - Part 1

As regular readers know from previous posts, I have a lot of background in assertion-based verification (ABV) and how assertions are used in simulation and formal analysis. There has been a lot of growth in the use of both assertions and formal since I was first involved in these technologies in 1999, but it would be disingenuous of me to suggest that ABV is as mainstream as I hoped it would be by now. Assertion-based tools are much easier to use, and are no longer appropriate only for those with a PhD in formal methods. Every major simulator supports assertions well, as do most of the hardware acceleration and emulation platforms.

So what's the problem? Why isn't everyone using assertions everywhere? The answer is simply that writing assertions, as valuable as they are in many ways, takes time and effort. The best assertions usually come from designers documenting their assumptions about their designs. In some cases, especially for well-defined buses and interfaces, verification engineers typically write the assertions. I've heard the same question hundreds of times over the years, sometimes from verification engineers but especially from designers: "Why can't you write my assertions for me?"

The simple answer, of course, is that assertions are supposed to capture the assumptions in the designers' heads and no EDA tool (at least so far) can read their minds. High-quality assertions are expressions of design intent that are orthogonal to the specific implementation. Thus, any tool that generates assertions from the design itself is suspect. I maintain that no automatic method for generating assertions will ever completely replace the need for engineer-written assertions. There is always information in the heads of the design and verification engineers that cannot possibly be gleaned from the design.

Having said this, various forms of automatic assertions are in common use and do have considerable value. These generally fall into three categories. The first is assertions derived directly from the design itself, including overflow and underflow checks for arithmetic expressions, bounds checks for arrays, and checks for proper synchronization of asynchronous clocks. Examples in the Cadence product line include the Automatic Formal Analysis (AFA) features of Incisive Formal Verifier (IFV) and Incisive Enterprise Verifier (IEV) as well as the clock-domain checks performed by Conformal Constraint Designer. These tend to be very accurate, requiring little review by the engineers before being used.

Additional assertions can be generated by making some reasonable assumptions about the design, perhaps based on naming rules as well as the design structure. These assertions tend to be suggestions, often requiring a bit of analysis by the designer to ensure accuracy. For example, IFV can identify most forms of FSMs and generate checks for dead-end or unreachable states; the designer need only check that the identified structures were intended as FSMs. Another example is overflow and underflow checks on stacks and FIFOs. There is no sure way to identify these structures in a design, but signals containing the string "stack" or "fifo" might be a good start.

The final category is assertions derived from the design and from supplemental files that express some aspect of design intent. For example, Conformal Constraint Designer can cross-check the design constraints specified in a constraint file against the design itself. IFV can formally verify pin connectivity by generating assertions based on the design and connectivity intent as captured by the designer in a spreadsheet. For low-power designs, Incisive Enterprise Simulator (IES) can generate assertions related to power domain transitions based on the power intent expressed in a Common Power Format (CPF) file. The resulting assertions can be run in IES, IFV, IEV, or the Palladium XP verification computing platform.

Perhaps the most exciting example of assertion generation using supplemental files is the approach taken by NextOp, which analyzes simulation traces to "learn" about a design's behavior and generates appropriate assertions (and coverage). We've discussed NextOp's "assertion synthesis" in the Cadence Community before; Joe Hupcey recently published an update to his video with NextOp CEO Yunshan Zhu; Richard Goering published an interview as well. I also mentioned them briefly in my last blog post about a DVCon panel. For my next post, I'm going to discuss my thoughts on NextOp and assertion synthesis. See you there!

Tom A.

The truth is out there...sometimes it's in a blog.