December 9, 2011 -- As complex system-on-chip (SOC) designs grow in size as well as functionality, more and more test vectors must be created and run to get reasonable test coverage. This imposes a cost in the time and effort needed to create these test vectors, and in the increased simulation time required. What's more, there may be cases where it's not very easy to create test vectors, rendering the traditional method of simulation less effective. This is where formal verification can help.

This article describes formal verification concepts and the differences between formal and simulation techniques, especially in the context of assertion-based verification. The assertion- based verification flow and some of the formal verification algorithms are also discussed in detail. Last but not the least, a few applications of formal technology in the context of ASIC designs are also presented.

Conforming to the specification

A lot of functionality is integrated into today's SOCs to achieve a wide variety of features. All these features need to be verified against their specifications. Verification implies ensuring that a particular feature is working in conformance with its specification.

Let us begin with a simple example. In a 3-bit one-hot encoded finite state machine (FSM), only 1 bit out of the 3-bit state vector can be at logic 1. Hence, out of the 8 possible states there are only 3 valid states (001, 010, 100). To verify this function, the verification engineer can apply different techniques. One way could be to apply appropriate test vectors to sensitize the state machine and observe the state vector signals and verify their correctness. But manual verification of signals is both tedious and prone to errors. To overcome this issue, monitors are written, which automatically compare the desired signals against a previously known golden output. An error is flagged by the monitors whenever the comparison fails.

Another method of verification has become popular in the last few years called assertion-based verification (ABV). In this method, an assertion is embedded in the RTL code, which captures the functionality of the feature to be verified. This method is very effective because assertions can be written by design engineers while writing the RTL code itself. These assertions can be tested using the traditional method of applying test vectors.

Whenever a test vector is applied that sensitizes the functionality captured by the assertion, the assertion flags an error if a functional bug is detected. However, this still requires generation of test vectors for verifying assertions. Using formal verification, assertions can be verified without the need of creating test vectors.

Assertion-based verification (ABV)

An assertion-based verification flow verifies the pre-defined or pre-determined properties of the design. Let's examine in detail the concept of properties and assertions, different types of properties, their mathematical representation, the industry standard languages available to describe them, and how simulation and formal techniques can be used to verify the assertions.

What is a property?

A property is nothing but the description of the "expected" design behavior. "Expected" means what is required (or the specification), and not what is implemented. Ideally, the implementation should match the specification, and this is exactly the task of verification.

An assertion is a directive to the verification tool to verify the property. In other words, when it is asserted that the property holds true, the "property" becomes an "assertion." In the verification flow, sometimes these two terms are used interchangeably.

Here are a few examples of properties in the context of ASIC designs:

There can be only one active driver on a tri-state bus (Bus-Contention). There should be no floating buses. There should be no data loss while moving from a fast to slow clock domain. A request should be acknowledged within 5 clock cycles.

It is worthwhile to mention here that properties not only describe the design features to be tested, but can also be used to constrain the design to limit the scope of testing to a reachable state space. In the former case, they are known as assertions, whereas in the latter they are known as "constraints."

It is also important to note that the properties do not modify the design in any way and they only read from the design.

Types of properties

Properties can be of two main types, namely "safety" and "liveness." Safety properties are those design characteristics that are bounded in time. They should always hold true and it is implicit that, "Something bad does not happen." In case of a failure, a counter example would always exist. An example of a safety property is: "A request is followed by acknowledge within 3 clock cycles."

Liveness properties are design characteristics that involve infinite sequences. In this case it is implied that, "Something good eventually happens." In case of a failure, a finite time counter example does not exist. An example of a liveness property is: "A request is followed by an acknowledgement sometime in future."

Mathematical representation of properties

Understanding and defining a "property" is the key to ABV. These properties can be defined using some standard mathematical representations. There are several such representations out of which computation tree logic (or CTL) is described here.

In CTL, a representation of a property is made up of the following three parts:

The design intent to be verified. The logical expression or the atomic formula about the state of the system. The design paths on which the design intent is to be verified.

In the following discussion, "A" means on all paths from the "current" state, read as "inevitably," and "E" means on at least one path from the "current" state, read as "possibly."

Defining the design state or time-stamp on each path on which the property is to be verified:

"X" means the next state(s). "G" means all> future states. "F" means some future state. "U" – means until

Here "AG" would imply the property needs to be verified on all paths in all states and "EF" implies that the property is true in any state on at least one path.

It can be seen that the following equation holds true:

Some properties can also be of the type "AF" which implies that the property holds true on all paths eventually.

Let's look at a couple of examples to understand these further.

For the first example, assume that in a bus protocol, multiple clients can send a request simultaneously to the arbiter and it is required to verify that the arbiter issues a grant to only one client at a time. Assuming two clients C1 and C2, this property can be mathematically represented as follows:

This property is expected to hold always, i.e., at all time-stamps and on all possible design paths. If the property does not hold in any design state even once, then the property fails and a finite length counter example can be generated. Such properties are known as safety properties. These means that something good always happens or anything bad never happens.

For the second example, assuming the same bus protocol as given in the first example, it may also be required to verify that whenever a client sends a request, the arbiter eventually issues a grant to the client. This can be represented mathematically as follows:

In this example, no finite length counter example can be generated. Such properties are known as liveness properties.

Writing assertions

Assertions can be written by RTL designers themselves while writing the RTL code. Three main industry standard languages exist today that can be used to define assertions:

Open Verification Library or OVL Property Specification Language or PSL System Verilog Assertions or SVA

Assertions also can be automatically generated and verified by some tools for some pre-determined set of design features. In this case, they are known as "implicit" assertions.

Verifying assertions

Assertions can be verified by using either simulation or formal techniques.

Simulation involves the creation of test vectors, which are applied to the design under test (DUT), and the output obtained is compared with a known golden output. If the comparison fails, an error is flagged; otherwise the test passes.

A test vector is a set of inputs that can sensitize the design logic to be tested. When assertions are defined in the design, the test vector needs to be created in a way such that it sensitizes the logic affecting the assertions appropriately, i.e., the logic in the fan-in cone of the assertions. If the design intent defined in the assertions is violated by applying the test vector, the assertion fails and an error is flagged by the assertion itself. A simulation trace also can be generated in case of safety properties.

In this method, the detection of a bug is entirely dependent on the test vector applied. A test vector sensitizes one or more paths in the design, and if the bug does not fall on any of those paths, the assertion will not flag an error and the design issue will not be caught. Here the assertion holds true with respect to the test vector applied. However, another test vector that sensitizes another design path may cause the same assertion to fail, if it is able to uncover the bug.

Formal verification does not require any test vectors to verify the assertions. It performs an exhaustive search for the bugs in the entire state space of the design.

For a design with n registers, the total number of design states is 2n. Many states may be unreachable, however, and are not valid. The actual valid states depend on the functionality implemented, input constraints and the initial state of the design. For example, for a 4-bit finite state machine (FSM) with one-hot encoding, the entire state space consists of 16 possible states. Only 4 out of 16 are valid or reachable states, however, and the remaining 12 are unreachable. The formal engine needs to verify the assertion in the reachable state space of the design.

Simulation vs. formal

Figure 1 shows the difference between simulation and formal verification at the conceptual level.

Figure 1. Design state space.

Assume that the design begins from an initial state represented by the center of the circles. Figure 1 represents the entire reachable state space of the design with respect to this initial state. The circles in the figure represent the clock cycles. Six clock cycles are shown here. The dots on each of the circles represent all the possible or reachable states in the corresponding clock cycle. The bigger red dots represent states with a design issue. Starting from the initial state, the design can enter into several other states in the first clock cycle. Similarly, from each state in the first clock cycle, the design can enter into several other states in the second clock cycle and so on.

In case of simulation, a test vector is applied at the input pins of the design. In each clock cycle, the next state of the design will be determined by the current state of the design and the inputs applied. Hence, each test vector will take the design through a specific path as shown by the curved green lines in the figure. Each green line corresponds to one test vector. If the design issue to be caught by the specified assertion gets triggered by any of these paths, it will be flagged; otherwise, it will go undetected. As a result, the scope of simulation is limited to the paths sensitized, or in other words the test vectors applied.

The formal technique works in an entirely different way. It also starts from the initial state of the design. It can be seen from Figure 1 that in the first clock cycle, the design can enter into 5 possible states based on all possible input combinations. These are represented by 5 dots on the innermost circle. The formal engine explores all 5 states and performs an exhaustive search for the design bugs specified by the assertions. It does not follow any specific path. From each of the 5 possible states in the first clock cycle, the formal engine explores all possible states in the second clock cycle for the bugs and continues to do so in subsequent cycles. In this way, it covers the entire state space of the design which is reachable starting from an initial state, taking into account all possible input signal combinations.

The actual algorithms of formal techniques will be described in subsequent articles. It's important to note here that in complex designs the state space is very large and formal techniques run into memory and performance issues, making them unsuitable for large designs.

Use of simulation and formal

Simulation and formal have their own pros and cons. While it is easy to detect deep design bugs by simulation, its coverage of design issues is limited to the number and quality of test vectors. The creation of test vectors is a very challenging and time-consuming task and can also run into controllability issues. It's very difficult to cover the complete design space by simulation alone and would require creation and execution of a huge number of test vectors.

On the other hand, formal techniques have the advantage that they do not need any test vectors. In addition, they cover the entire state space of the design and hence are exhaustive in nature. But they run into memory and performance issues as the design state space grows exponentially with each clock cycle. As a result, they are not able to converge and are suitable only for small to medium size designs.

Traditionally, simulation has been the most effective technique deployed by verification engineers. Formal techniques are not a replacement for simulation. However, they are very effective in finding some types of issues where simulation cannot. Hence, formal techniques can be used to complement simulation and both techniques can be used together to increase design coverage.

In the case of small designs formal techniques are very effective. However, in the case of large designs, they may not be able to converge because of the huge state space, but still there may be some critical functionality where an exhaustive search of bugs is desirable. In such cases, simulation and formal can be used together. Appropriate test vectors can be applied using the simulation method to take the design to a desired state from where the critical functionality can be sensitized easily. Then, using that as the initial state, formal techniques can be used to perform an exhaustive search for bugs in that zone.

By Ashima S. Dabare

and Saurabh Verma

Ashima S. Dabare is a Senior Consulting Applications Engineer at Atrenta India Pvt., Ltd. She has a masters degree from Indian Institute of Technology, Delhi. She has rich experience in several areas of ASIC design flow including clocks, static timing analysis, design-for-test, formal technology and RTL prototyping.

Saurabh Verma is a Senior Manager at Atrenta India Pvt., Ltd. He has a bachelors degree from Indian Institute of Technology, Kanpur. He has rich experience in the area of formal technology, rule-based design verification, clocks, synthesis and optimization.

In this first article in a series of three, we've discussed the basic concept of properties and assertions, different types of properties and the conceptual difference between simulation and formal methods of verifying assertions. The second article will cover some of the formal algorithms used to verify the assertions in case of combinatorial as well as sequential circuits. In the third article, we discuss the applications of formal technology.