FORMAL VERIFICATION

Although large computer and chip companies like IBM, Intel, and Motorola  have been developing and using formal tools internally for decades (since  around the mid-1980s), the whole field of formal verification (FV) is still  relatively new to a lot of folks. This is particularly true in the FPGA arena,  where the adoption of formal verification is lagging behind its use in ASIC  design flows. Having said this, formal verification can be such an incredibly powerful tool that more and more folks are starting to use it in  earnest.   

One big problem is that formal verification is still so new to mainstream  usage that there are many players, all of whom are happily charging around  in a bewildering variety of different directions. Also, as opposed to a lack of  standards, there are now so many different offerings that the mind boggles. The  confusion is only increased by the fact that almost everyone you talk to puts his  or her unique spin on things (if, for example, you ask 20 EDA vendors to define  and differentiate the terms assertion and property, your brains will leak out of  your ears at the diametrically opposing responses).   

Trying to unravel this morass is a daunting task to say the least. However,  there is nothing to fear but fear itself, as my dear old dad used to say, so let’s  take a stab at rending the veils asunder and describing formal verification in a  way that we can all understand.

Different Flavors of Formal Verififi cation   

As mentioned at the beginning of this chapter, the term formal verification was  considered synonymous with equivalency checking for the majority of design  engineers. In this context, an equivalency checker is a tool that uses formal  (rigorous mathematical) techniques to compare two different representations  of a design—say an RTL description with a gate-level netlist—to determine  whether they have the same input-to-output functionality.   

In fact, equivalency checking may be considered a subclass of formal verification called model checking , which refers to techniques used to explore the  state-space of a system to test whether certain properties, typically s pecified in the form of assertions, are true. (Definitions of terms like property and assertion are presented a little later in this section.)   For the purposes of the remainder of our discussions here, we shall understand formal verification to refer to model checking. It should be noted, however, that there is another category of formal verification known as automated  reasoning , which uses logic to prove, much like a formal mathematical proof,  that an implementation meets an associated specification.

FAQs  

What is formal verififi cation, and why is it so cool?  

To provide a starting point for our discussions, let’s assume we have a design  comprising a number of subblocks and that we are currently working with one of  these blocks, whose role in life is to perform some specific function. In addition  to the HDL representation that defines the functionality of this block, we can also  associate one or more assertions/properties with that block (these assertions/properties may be associated with signals at the interface to the block or with signals  and registers internal to the block).  

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 these statements 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. ”

Thus, assertions/properties allow you to describe the behavior of a time-based  system in a formal and rigorous manner that provides an unambiguous and universal representation of the design’s intent. Furthermore, assertions/properties can  be used to describe both expected and prohibited behavior.  

The fact that assertions/properties are both human and machine-readable  makes them ideal for the purposes of capturing an executable specification,  but they go far beyond this. Let’s return to considering a very simple assertion/ property such as “ Signals A and B should never be active (low) at the same time. ”  One term you will hear a lot is assertion-based verification (ABV), which comes  in several flavors: simulation, static formal verification, and dynamic formal  verification. 

In the case of static formal verification, an appropriate tool reads in the functional description of the design (typically at the RTL level of abstraction) and then  exhaustively analyzes the logic to ensure that this particular condition can never  occur.  

By comparison, in the case of dynamic formal verification, an appropriately  augmented logic simulator will sum up to a certain point, then pause and automatically invoke an associated formal verification tool (this is discussed in more  detail below).  

Of course, assertions/properties can be associated with the design at any level,  from individual blocks, to the interfaces linking blocks, to the entire system. This  leads to a very important point, that of verification reuse.

With regard to assertions/properties associated with the system’s primary  inputs and outputs, the verification environment may use these to automatically  create stimuli to drive the design. Furthermore, you can use assertions/properties throughout the design to augment code and functional coverage analysis  (see also the “ Miscellaneous ” section below) to ensure that specific sequences  of actions or conditions have been performed.

Terminology and Defifi nitions  

Now that we’ve discussed the overall concept of the model checking aspects  of formal verification, we are better equipped to wade through some further  terminology and definitions. To be fair, this is relatively uncharted water; the  following was gleaned from talking with lots of folks and then desperately trying to rationalize the discrepancies between the tales they told.  

●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 (e.g., “ 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 a violation if that assertion   “ fires ” ).   

Today, with the use of formal tools and simulation tools in unified environments and methodologies, the terms property and assertion tend to be  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 model checking  space. Formal model checkers consider all possible allowed input combinations when performing their magic and working on a proof. Thus, 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 out put 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 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 consist of a sequence of events.  Also, events can be used to specify the window within which an assertion/ property is to be tested (e.g., “ After a , b , c , we expect d to be true, until e occurs, ” where a , b , c , and e are all events, and d is the behavior being verified). Measuring the occurrence of events and assertions/properties yields  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: The term procedural refers to 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 “ incontext ” 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: The term declarative refers to 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, ” unlike  its procedural counterpart that is only “ on/active ” when a specific path is  taken/executed through the HDL code.  

● Pragma: The term pragma is an abbreviation for “ pragmatic information, ”  which refers to special pseudocomment directives that can be interpreted  and used by parsers/compilers and other tools. (Note that this is a general purpose term, and pragma-based techniques are used in a variety of tools in  addition to formal verification technology.)

Alternative Assertion/Property Specififi cation Techniques   

This is where the fun really starts, because there are various ways in which  assertions/properties and so forth can be implemented, as summarized below:  

● Special languages : This refers to using 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 Sugar, PSL, and OVA are good examples, are very powerful in creating sophisticated, regular, and temporal expressions, and they allow complex behavior to be specified with very little code (Sugar, PSL, and OVA  are introduced in more detail later in this chapter).   Such languages are often used to define assertions/properties in “ sidefiles ” that are maintained outside the main HDL design representation. These  side-files may be accessed during parser/compile time and implemented in  a declarative fashion. Alternatively, a parser/compiler/simulator may be  augmented to allow statements in the special language to be embedded  directly in the HDL as in-line code or as pragmas; in both of these cases,  the statements may be implemented in a declarative and/or procedural  manner.  

● Special statements in the HDL itself : Right from the get-go, VHDL came  equipped with a simple assert statement that checks the value of a Boolean  expression and displays a user-specified text string if the expression evaluates False. The original Verilog did not include such a statement, but  SystemVerilog has been augmented to include this capability.   The advantage of this technique is that these statements are ignored by  synthesis engines, so you don’t have to do anything special to prevent them  from being physically implemented as logic gates in the final design. The  disadvantage is that they are relatively simplistic compared to special assertion/property languages and are not well equipped to specify complex temporal sequences (although SystemVerilog is somewhat better than VHDL  in this respect).  

● Models written in the HDL and called from within the HDL : This concept refers to having access to a library of internally or externally developed models. These models represent assertions/properties using standard  HDL statements, and they may be instantiated in the design like any other  blocks. However, these instantiations will be wrapped by synthesis OFF/ ON pragmas to ensure that they aren’t physically implemented. A good  example of this approach is the open verification library (OVL) from the  Accellera standards committee ( www.accellera.org ), as discussed in the  next section.  

● Models written in the HDL and accessed via pragmas : This is similar in  concept to the previous approach in that it involves a library of models that  represent assertions/properties using standard HDL statements. However, as  opposed to instantiating these models directly from the main design code, they are pointed to by pragmas. A good example of this technique is the  CheckerWare® library from 0-In Design Automation ( www.0-In.com ). For  example, consider a design containing the following line of Verilog code:

reg [5:0] STATE_VAR; / 0in one_hot

The left-hand side of this statement declares a 6-bit register called STATE_ VAR, which we can assume is going to be used to hold the state variables  associated with an FSM. Meanwhile, the right-hand side ( “ 0in one_hot ” ) is  a pragma. Most tools will simply treat this pragma as a comment and ignore  it, but 0-In’s tools will use it to call a corresponding “ one-hot ” assertion/  property model from their CheckerWare library. Note that the 0-In implementation means that you don’t need to specify the variable, the clocking, or the  bit-width of the assertion; this type of information is all picked up a utomatically.  Also, depending on a pragma’s position in the code, it may be implemented in a  declarative or procedural manner.

Static Formal versus Dynamic Formal   

This is a little tricky to wrap one’s brain around, so let’s take things step by  step. First, you can use assertions/properties in a simulation environment. In  this case, if you have an assertion/property 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.   

Simulators can cover a lot of ground, but they require some sort of testbench or a verification environment that is dynamically generating stimulus.  Another consideration is that some portions of a design are going to be difficult to verify via simulation because they are deeply buried in the design, making them difficult to control from the primary inputs. Alternatively, some areas  of a design that have large amounts of complex interactions with other state  machines or external agents will be difficult to control.   

At the other end of the spectrum is static formal verification . These tools  are incredibly rigorous and they examine 100 percent of the state space without having to simulate anything. Their disadvantage is that they can typically  be used for small portions of the design only, because the state space increases  exponentially with complex properties, and one can quickly run into a “ state  space explosion. ” By comparison, logic simulators, which can also be used to  test for assertions, can cover a lot of ground, but they do require stimuli, and  they don’t cover every possible case.   

To address these issues, some solutions combine both techniques. For  example, they may use simulation to reach a corner condition and then automatically pause the simulator and invoke a static formal verification engine to exhaustively evaluate that corner condition. (In this context, a general definition  of a “ corner condition ” or “ corner case ” is a hard-to-exercise or hard-to-reach  functional condition associated with the design.) Once the corner condition has  been evaluated, control will automatically be returned to the simulator, which  will then proceed on its merry way. This combination of simulation and traditional static formal verification is referred to as dynamic formal verification.   

As one simple example of where this might be applicable, consider a  FIFO memory, whose “ Full ” and “ Empty ” states may be regarded as corner  cases. Reaching the “ Full ” state will require many clock cycles, which is best  achieved using simulation. But exhaustively evaluating attributes/properties  associated with this corner case, such as the fact that it should not be possible to write any more data while the FIFO is full, is best achieved using static  techniques.   

Once again, a good example of this dynamic formal verification approach  is provided by 0-In. Corner cases are explicitly defined as such in their  CheckerWare library models. When a corner case is reached during simulation,  the simulator is paused, and a static tool is used to analyze that corner case in  more detail.

FAQ  

Is there a standard formal verififi cation language?  

Let’s begin with something called Vera®, which began life with work done at Sun  Microsystems in the early 1990s. It was provided to Systems Science Corporation  somewhere around the mid-1990s, which was in turn acquired by Synopsys in  1998. Vera is essentially an entire verification environment, similar to, but perhaps  not as sophisticated as, the e verification language/environment introduced earlier  in this chapter. Vera encapsulates testbench features and assertion-based capabilities, and Synopsys promoted it as a stand-alone product (with integration into  the Synopsys logic simulator). Sometime later, due to popular demand, Synopsys  opened things up to for third-party use by making OpenVera™ and OpenVera  Assertions (OVA) available.  

Somewhere around this time, SystemVerilog was equipped with its first pass  at an assert statement. Meanwhile, due to the increasing interest in formal verification technology, one of the Accellera standards committees started to look  around for a formal verification language it could adopt as an industry standard.  A number of languages were evaluated, including OVA, but in 2002, the committee eventually opted for the Sugar language from IBM. Just to add to the fun,  Synopsys then donated OVA to the Accellera committee in charge of SystemVerilog  (this was a different committee from the one evaluating formal property languages).  

Yet another Accellera committee ended up in charge of something called the  open verification library, or OVL, which refers to a library of assertion/property  models available in both VHDL and Verilog 2K1.  

So now we have the assert statements in VHDL and SystemVerilog, OVL (the  library of models), OVA (the assertion language), and the property specification language (PSL), which is the Accellera version of IBM’s Sugar language ( Figure 7-14 ).  The advantage of PSL is that it has a life of its own in that it can be used independently of the languages used to represent the functionality of the design itself. The  disadvantage is that it doesn’t look like anything the hardware description languages design engineers are familiar with, such as VHDL, Verilog, C/C ++, and  the like. There is some talk of spawning various flavors of PSL, such as a VHDL  PSL, a Verilog PSL, a SystemC PSL, and so forth; the syntax would differ among  these flavors so as to match the target language, but their semantics would be  identical.

Figure 7-14 attempts to show the state of things regarding the various verification styles and languages. It’s important to note that this figure just reflects  one view of the world, and not everyone will agree with it (some folks will  consider this to be a brilliant summation of an incredibly confusing situation,  while others will regard it as being a gross simplification at best and utter  twaddle at worst).

Insider Info  

Don’t make the mistake of referring to “ PSL/Sugar ” as a single/combined language. There’s PSL and there’s Sugar and they’re not the same thing. PSL is the  Accellera standard, while Sugar is the language used inside IBM.