As I pen these words, I feel as though my brain has been well and truly "boggled," because I've been trying to wrap the the poor little scamp around the new Archer Assertion-Based Verification (ABV) System that was announced by 0-In Design Automation in late January. The problem is that Archer is so multi-faceted and all-embracing that it's difficult to know which portion one should sink one's teeth into first.
Properties vs. assertions, and procedural vs. declarative
Before we plunge into the fray, it's probably worth spending a few moments setting the scene, as it were. First of all there are a plethora of different terms, such as "properties", "assertions," "events", "constraints", and the list goes on. I took a stab at wading through this morass in my August 15, 2002 column entitled "Walking the assertion maze", so all we need to note here is that the term "property" came from the formal verification model-checking arena, while the term "assertion" made its way to us from the simulation domain. Today — with the use of formal tools and simulation tools in unified environments and methodologies — the terms "property" and "assertion" are used interchangeably (for the purposes of this column we shall stick to "assertion").
A very simple assertion might be something along the lines of "Signals A and B should never be active (low) at the same time." But assertions 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."
In general, we understand an assertion to be a statement about a specific attribute associated with the design that is expected to be true. Thus, assertions can be used as checkers/monitors, or as targets of formal proofs, and they are usually used to identify/trap undesirable behavior.
Two other terms of interest are "procedural" and "declarative," which refer to how the assertions are "seen" and "actioned" by the verification system. A procedural assertion (also known as an "in-context" assertion) is one that is described within the context of an executing process. For example, if we had an "if-then-else" statement, we could associate one assertion with the "then" branch and another with the "else" branch. Assertions of this type are only "on/active" when a particular path is taken through the RTL code. By comparison, a declarative assertion exists within the structural context of the design and is always "on/active."
Different ways of specifying assertions
This is where things start to get interesting, because there are a variety of ways in which assertions can be specified.
Special languages: First of all there are special languages, like OpenVera Assertions (OVA) from Synopsys and Sugar from IBM. These are very powerful for creating complex regular and temporal expressions using very little code.
Some time ago Synopsys donated OVA to the SystemVerilog committee at Accellera. My current understanding is that the SystemVerilog folks are taking what they want from OVA, mangling the syntax and semantics a tad, and incorporating the results into SystemVerilog. The result of this activity may be referred to as SystemVerilog Assertions (SVA).
Around the same time, another Accellera committee in charge of selecting an "official" formal verification language evaluated a lot of different options and then settled on IBM's Sugar language. This has since been transmogrified into something called the Property Specification Language (PSL). (It's important to note that Sugar and PSL should be regarded as two distinct entities.)
One important point is that assertions specified in these languages are typically presented in side files that are associated with specific functional blocks or interfaces within the design, or with the design's primary inputs and outputs. Thus, these assertions function in a declarative manner.
Special statements in the HDL: From its inception, VHDL included a simple "assert" statement. The original Verilog lacked an equivalent, but SystemVerilog has been augmented with this capability. These assertions can operate in a declarative or procedural manner.
Models written in the HDL called from within the HDL: This refers to having a library of RTL models that perform assertion-type functions and that can be instantiated from within the main design just like any other RTL block/module (these instantiations will be flagged by one means or another to ensure that they don't get synthesized and physically implemented as part of the final design). A good example of this approach is the Open Verification Library (OVL) that falls under the auspices of yet another Accellera committee.
Models written in the HDL accessed via pragmas: This is similar in concept to the previous technique in that refers to having a library of RTL models that perform assertion-type functions. However, these models are accessed by means of special comments (called "pragmas" by some and "directed comments" by others) in the main HDL code. A good example of this approach is the CheckerWare library from 0-In, as discussed later in this column. Depending on a pragma's position within the code, these assertions can act in a declarative or procedural manner.
Static formal, dynamic formal, simulation-driven, arrggghhhh!
And this is where the fun really starts (now you can see why my brain aches every time I try to put all of this together). First of all you can use assertions in a simulation environment. In this case, if you have an assertion along the lines of "Signals A and B should never be active (low) at the same time," then if this illegal case occurs during the course of a simulation, a warning flag will be raised and the fact this happened can be logged.
One consideration with regard to a simulation-based approach is that it requires some sort of testbench or a verification environment that is dynamically generating stimulus. Another point to ponder is potential problems with regards to simulation hotspots. These include sections of the design that are difficult to verify either because they are deeply buried in the design making them difficult to control from the primary inputs. They also encompass sections of the design that have large amounts of complex interactions with other state machines or external agents.
At the other end of the spectrum is static formal verification in the form of model checking. This refers to exploring the state-space of a system (or a portion thereof) to test whether or not certain assertions are true. This form of verification doesn't require the use of a testbench, but instead uses mathematical algorithms to exhaustively analyze the design to deterministically determine if there are any cases that will cause the assertion to be violated.
This is currently a very exciting area in which new algorithms that exhibit ever-increasing capacity and performance are appearing on the scene. However, static formal verification can be used to test only relatively small, localized portions of the design before you start to run into state-space explosion problems.
And then we have something called dynamic formal verification. The idea here is that you run the main design code along with its associated assertions in the simulator until you reach a specific corner case condition — for example, loading a FIFO to the stage where it is just full.
At this point something (which we'll discuss in more detail below) causes the simulator to automatically pause and invoke a formal verification tool that performs an exhaustive analysis of this portion of the design in the context of its local assertions to ensure that everything is as it should be. Once this analysis has been completed, the system automatically returns control to the simulator and so on.
And finally we come to 0-In's Archer ABV system
As I said at the beginning of this column, 0-In's Archer ABV system has so many facets that it's difficult to boil it down into a simple overview. However, "there's nothing to fear but fear itself" as my dear old dad used to say, so we'll throw caution to the winds and give it the old school try.
The CheckerWare Library: The first point is that Archer features 0-In's CheckerWare library. This Verilog RTL-based library of models includes over 70 pre-verified assertion checkers and over 25 proven protocol monitors. These models are called by associating a special comment with a particular line of code. For example, let's assume that you have a set of registers acting as state variables for a state machine and you wish to use one-hot encoding. In order to check this encoding is always valid, you can associate a "// 0-in one_hot" comment with the register declaration. At the appropriate time, this will cause 0-In's tools to instantiate a corresponding "one-hot" CheckerWare assertion monitor with these registers.
One key point about the 0-In implementation is they you never need to specify things like the variable(s), clocking, or bit-width(s) of the assertion, because all of this information is picked up automatically. Another key point is that the CheckerWare models include flags that highlight corner case conditions. This means that these models can be used to guide dynamic formal verification (to pause the simulator and to invoke the static formal verification tool as appropriate).
The Assertion Compiler: One consideration with today's designs is that they tend to include large quantities of intellectual property (IP) blocks from multiple sources. This can be particularly taxing when it comes to assertion-based verification, because each block may have its assertions specified using a different language or technique. Thus, Archer includes an Assertion Compiler that can accept 0-In's CheckerWare models, PSL assertions, SystemVerilog Assertions (SVA), and Open Verification Library (OVL) assertions, and then translate all of these formats into synthesizable Verilog equivalents that can be used by multiple tools and environments.
Static and Dynamic Formal: The Archer SF (Static Formal) portion of Archer includes a suite of engines that perform tasks such as automatic RTL checking, clock domain verification, and classical static formal verification. Sitting on top of your existing logic simulation solution, the Archer DF (Dynamic Formal) portion of Archer adds dynamic formal capability into the mix.
Coverage Driven Verification: Verification coverage metrics really fall into two camps: specification-level coverage and implementation-level coverage. In this context, specification-based coverage measures verification activity with respect to items in the high-level functional or macro-architecture definition. This includes the input/output behaviors of the design, the types of transactions that can be processed (including the relationships of different transaction types to each other), and the data transformations that must occur.
By comparison, implementation-based coverage measures verification activity with respect to micro-architecture details of the actual implementation. This refers to design decisions that are embedded in the RTL that result in implementation-specific corner cases; for examples, the depth of a FIFO buffer and the corner cases for its "high-water mark" and "full" conditions. Such implementation details are rarely visible at the specification level.
Total verification coverage is the combination of specification and implementation coverage. Thus, another aspect of 0-In's solution is Archer CDV (Coverage-Driven Verification). This unified coverage management and debugging environment gathers, organizes, and makes available for analysis the results from all of the different simulation-driven, static formal, and dynamic formal assertion-based verification engines.
Engineered Methodologies: There's a lot more to the lives of design and verification engineers than simply having access to a grab-bag of tools. Archer provides an environment that allows you to easily use multiple simulation-driven, static formal, and dynamic formal engines. Archer also encompasses the concept of "engineered methodologies," which refers to the capturing of best practices of experienced users and codifying them for use by all design and verification engineers.
As usual, there's much more to Archer ABV than we have time to go into here. Suffice it to say that 0-In continues to pave the way in the ABV arena, and I for one am very impressed. So it's an official "Cool Beans" from me!
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.
RSS
Digital
RSS| 
Digital| 
Mobile
