Walking the assertion maze

Walking the assertion maze
Okay, this is where the pain starts, because we're going to try to wend our weary way through the assertion language (a.k.a. "property language") maze. We'll formally define some terms in a little while, but as a starting point let's simply assume that an assertion/property is an alternative way to specify some attribute associated with a digital design, or a portion thereof.

For example, let's assume that one of the modules in your design acts as a simple arbiter such that only one of its outputs is active at any particular time. In addition to the hardware description language (HDL) representation of the functional contents of this module, you could also define an assertion/property that essentially states "Only one output can be in its active (low) state at any particular time." This assertion/property will be specified using some technique (as discussed below) that is both human and machine-readable.

A very simple assertion/property might be along the lines of "Signals A and B should never be active (low) at the same time." But assertions/properties can also extend to extremely complex transaction level constructs, such as "When a PCI write command is received, then a memory write command of type xxxx must be issued within 5 to 36 clock cycles."

These assertions/properties can subsequently be used by a variety of tools, such as a model checker (also known as a formal property checker), which will exhaustively analyze the HDL to check if they remain true in every possible case. Using this technique, there are no problems with weird and wonderful corner cases, because the model checker examines 100% of the state space without having to simulate anything. Alternatively, in the case of a logic simulation, the assertions/properties can be used to monitor how the HDL behaves and report any violations, and they can also be used to track and report functional code coverage - that is, to document which specific sequences of actions have actually been tested. Furthermore, test automation applications can be enhanced to read assertions/properties and use them to automatically create testbenches (or portions thereof) ... and the list goes on.

One really cool thing is that, unlike a testbench associated with an individual module (or IP block) that has to be discarded when that module is integrated into a larger design, any assertions/properties associated with a module remain valid and usable, irrespective of whether the module is being used in isolation or as part of a larger system. So, all things considered, assertions/properties would seem to be a jolly good idea, but of course most things do if you talk about them quickly and gesticulate wildly.

A plethora of definitions
When I was at DAC earlier this year, one of the questions I asked (of anyone who wasn't paying attention and didn't manage to get out of my way fast enough) was "What's the difference between an assertion, a property, and a constraint?" You wouldn't believe the variety of different answers I received ... all of them seeming to make sense at the time, but each of them typically contradicting my previous victim.

Eventually I returned to my home base (welcome to the pleasure dome) and tried to wade through my notes, at which time my mind "threw a wobbly" and flipped into "boggle overload" mode. Fortunately for my sanity, I ran across John Emmitt from @HDL. Thanks to his tremendous history and experience in this arena, John managed to help me to cut through some of the confusion.

I'm also indebted to the folks at Axis Systems, who have been putting a lot of thought into assertions/properties, and who provided me with a fantastic amount of very useful input. Of course, you may be wondering why the guys and gals at Axis - who specialize in hardware acceleration/emulation - are so interested in this topic. In fact, it turns out that they've been looking into the hardware acceleration of assertions/properties, and they will be making some mega-cool-beans announcements in this area on August 19th ... so keep your eyes and ears open, because what they have to say will blow your socks off (perhaps you should wear the elastic variety to work that day).

But we digress ... In order to wrap our brains around all of this stuff, we need a set of definitions that we can all agree to, and a starting point, even if only as a basis for argument and discussion, would be as follows:

Assertions/Properties: The term "property" comes from the model checking domain, and refers to a specific functional behavior of the design that you want to (formally) verify (such as, "after a request, we expect a grant within 10 clock cycles"). By comparison, the term "assertion" stems from the simulation domain, and refers to a specific functional behavior of the design that you want to monitor during simulation (and flag violations if that assertion "fires"). Today, with the use of formal tools and simulation tools in unified environments and methodologies, the terms "property" and "assertion" are used interchangeably - that is, a property is an assertion and vice versa. In general, we understand an assertion/property to be a statement about a specific attribute associated with the design that is expected to be true. Thus, assertions/properties can be used as checkers/monitors, or as targets of formal proofs, and they are usually used to identify/trap undesirable behavior.

Constraints: The term "constraint" also derives from the formal/model checking space. Due to the fact that formal model checkers consider all possible allowed input combinations when performing their magic and working on a "proof," there is often a need to constrain the inputs to their "legal" behavior. Otherwise, the tool would report "false negatives," which are property violations that would not normally occur in the actual design. As with properties, constraints can be simple or complex. In some cases, constraints can be interpreted as properties to be proven. For example an input constraint associated with one module could also be an output property of the module driving this input. So, properties and constraints may be "dual" in nature. (The term constraint is also used in the "constrained random simulation" domain, in which case the constraint is typically used to specify a range of values that can be used to drive a bus.)

Event: An event is similar to an assertion/property, and in general events may be considered to be a subset of assertions/properties. However, while assertions/properties are typically used to trap *undesirable* behavior, events may be used to specify *desirable* behavior for the purposes of functional coverage analysis. In some cases, assertions/properties may be comprised of a sequence of events. Also, events can be used to specify the "window" within which an assertion/property is to be tested (such as, "After A, B, C, we expect D to be true until E occurs," where A, B, C, and E are all (static) events, and D is the behavior being verified). Measuring the occurrence of events and assertions/properties leads to quantitative data as to which corner cases and other attributes of the design have been verified. Statistics about events and assertions/properties can also be used to generate functional coverage metrics for a design.

Procedural: An assertion/property/event/constraint that is described within the context of an executing process or set of sequential statements such as a VHDL process or a Verilog "always" block (thus, these are sometimes called "in-context" assertions/properties). In this case the assertion/property is built into the logic of the design and will be evaluated based on the path taken through a set of sequential statements.

Declarative: An assertion/property/event/constraint that exists within the structural context of the design and is evaluated along with all of the other structural elements in the design (for example, a module that takes the form of a structural instantiation). Another way to view this is that a declarative assertion/property is "always on/active" - that is, it is always being tested - unlike its procedural counterpart that is only on/active when a specific path is taken/executed through the HDL code.

Property Language, Assertion Language, Assertion Library, Formal Property Language: All used interchangeably to describe a language that can be used to represent high-level assertions/properties/events/constraints. These languages are designed to provide a concise format for specifying complex temporal sequences and regular expressions.

A quagmire of approaches
This is where the fun really starts, because there are a variety of ways in which assertions/properties et al can be implemented as summarized below.

Declarative: First we have declarative assertions/properties in the form of a library of Verilog monitor modules, which are typically instantiated in the design like any other modules. These modules are seen as monitors by simulators (the fact that they are specifically handled as assertions/properties is determined by the module names, which are recognized by the environment/tools/etc.). These special modules are "wrapped" by synthesis OFF/ON pragmas to ensure that they aren't physically implemented (where a pragma is a special pseudo-comment directive that can be interpreted and used by parsers/compilers and other tools). A good example of this approach is the Open Verification Library (OVL) from Accellera.

Procedural: As opposed to instantiating a module from a library, it may be more convenient to specify assertions/properties using procedural statements inside the HDL code itself. This is the case with the new "assert" construct that is part of the SystemVerilog 3.0 specification, which was recently approved by Accellera. Procedural assertions/properties are useful in the context of a Verilog "always" block with code such as a CASE statement or an IF-THEN-ELSE statement, which allows the assertions/properties to be active only during the context in which they are important.

Special Language: Another approach is to use a formal property/assertion language that has been specially constructed for the purpose of specifying assertions/properties with maximum efficiency. Languages of this type - of which IBM's Sugar and the Open Vera Assertions (OVA) language used by Synopsys are good examples - are very powerful in creating complex temporal expressions, and they also make use of regular expressions to allow complex behavior to be specified with very little code. These languages are often used to define assertions/properties in side files, which are accessed during parser/compile time, and which are implemented in a declarative fashion. Alternatively, a parser/compiler/simulator/ may be augmented so as to allow assertions/properties specified in the special language to be embedded in the HDL as in-line code (or as pragmas as discussed below), in which case they may be implemented in a declarative and/or procedural manner.

Pseudo-Comment Directives: Yet another technique is to use pseudo-comment directives, which are commonly referred to as "pragmas" (an abbreviation for "pragmatic information"). This allows assertions/properties to be embedded directly in the HDL code in the form of comments that do not interfere with the Verilog syntax. Formal verification tools can read the comments using a special parser. When it comes to simulation, the parser/compiler can be used to insert/output Verilog code/modules corresponding to the assertions/properties.

A good example of this approach is that used by 0-In Design Automation. In their case, when you add a simple comment corresponding to an assertion/property, their parser/compiler automatically extracts related information (such as bus widths) from the context of the code. Each type of assertion/property pragma maps onto a corresponding library module written in Verilog. Of particular interest is that, unlike OVL modules that are used only in a declarative fashion, the 0-In technique (in which the assertion/property is associated with a particular line of code) means that their assertions/properties can be used in a declarative and/or procedural manner. Also, 0-In has a "-constraint" directive that can change an attribute/property into a constraint (phew!).

Post-Processing Simulation History: Last but not least, some amongst us may favor the approach of checking for assertions/properties following a simulation run (similar to the way in which engineers have traditionally used waveform dumps to analyze the results from the simulation). An example of this approach is provided by the lads and lasses at TransEDA, who have developed a tool that can read a waveform dump file in VCD or FSDB format, read a set of assertions/properties specified in Perl or Sugar, and then analyze the dump file and extract and display information as to how the assertions/properties behaved. One big advantage of this methodology is that it doesn't require any changes to the simulator, any language extensions, or any changes to the design files.

A morass of languages
Oh my aching head! Way back in the mists of time (circa 22 April 2002), there was a news release from the Accellera Formal Verification Technical Committee saying that, after months of careful deliberation and debate, they had selected the Sugar formal property language from IBM.

At that time I was tap-dancing in the streets, because the concept of having a single language that everyone could agree to support seemed like an obviously good idea. What I wasn't aware of at that time was that Accellera actually have three different committees working on this sort of thing. In addition to the committee that selected Sugar (both the committee and the language have their roots in the Formal Property Checking camp), there is also a committee working on the Open Verification Library (OVL), and there is another committee working on the syntax and semantics of the Design Assertion Subset (DAS), which refers to the "assert" command in SystemVerilog 3.0 (see also my previous August column for more details on this).

So we can already see that we're in for fun times ahead. But wait - it gets better! During DAC 2002, Synopsys leapt into the fray with gusto and abandon and proclaimed that they were throwing their Open Vera Assertions (OVA) 2.0 language into the pot (they actually used the word "donating," but I'm not exactly sure what this implies in this context). "Good Grief, what's OVA," I asked myself at the time (but now I wish I hadn't).

In fact, OVA 2.0, is based on Intel's temporal logic language ForSpec. This is one of the languages that were evaluated (and ultimately passed over) by the Accellera Formal Verification Technical Committee, who eventually opted for Sugar. As an additional little nugget of information, the development of ForSpec was aided by the folks at Co-Design Automation. As you may recall, these are the designers of the SuperLog language, and are also instrumental in the definition of the "assert "statement in SystemVerilog 3.0. Thus, it's no great surprise that the syntax and semantics of ForSpec/OVA 2.0 aren't a million miles away from those of the "assert "statement in SystemVerilog 3.0 (unlike the syntax and semantics of Sugar).

So what does all this mean? To be honest I don't have a clue anymore and, as Rhett Butler proclaimed in Gone With The Wind, "Frankly my dear, I don't give a damn" (perhaps he had a momentary vision of things to come on the assertion/property language front?). But it means that "EDA Space" will remain nothing if not interesting. In the short term, it also means that formal verification tools - such as @Verifier from @HDL - will need to support multiple formats (indeed, @Verifier already supports a Verilog pragma-based approach, the OVA 2.0 assertion format, and the Accellera Sugar language). In the longer term, one can but hope that the various language flavors will eventually evolve into a single standard format (although I'm no longer holding my breath on this point)! Until next time, have a good one.

Clive (Max) Maxfield is president of Techbites Interactive, a marketing consultancy firm specializing in high-tech. Author of Bebop to the Boolean Boogie (An Unconventional Guide to Electronics) and co-author of EDA: Where Electronics Begins, Max was once referred to as a "semiconductor design expert" by someone famous who wasn't prompted, coerced, or remunerated in any way.