June 1, 2005 -- The complexity of modern SoC designs has created a verification crisis. Engineers cannot imagine all of the possible corner-case behaviors let alone write tests to exercise them. The only way to address the increased complexity is to supplement traditional functional verification methods by combining assertions, simulation, and formal techniques in a process called assertion-based verification (ABV). Assertions allow engineers to detect bugs sooner while formal verification gives them more control of the overall verification effort.

Assertions increase the observability of the design. When used in a simulation-based verification environment, embedded assertions catch design issues locally, identifying them immediately as they happen. Assertions enable hard-to-verify logic and critical functionality to be identified as coverage goals. In a pseudo random simulation environment, they audit the quality of the stimulus and thereby identify holes in the test environment, in effect, measuring the thoroughness of verification.

Formal verification with model checking technology increases the controllability of the design. Once a design is instrumented with assertions, formal verification can verify areas of concern, known as verification hot spots. Model checking analyzes the RTL structure of the design and characterizes its internal nature. It targets corner-case behaviors directly. Each assertion violation discovered by model checking is reported with the counter-example or examples in which the violation can happen. This uncovers functional errors that would have been missed using traditional verification methodologies.

Standardized assertion languages and assertion libraries have lowered the barrier for adopting an ABV methodology. However, as with any tool, their effectiveness in achieving specific goals depends to a large extent on how well they are deployed.

As an early pioneer of ABV, the 0-In Business Unit of Mentor Graphics has helped many design teams deploy ABV. We noticed that some users paid too much attention to the details of the assertion languages, the richness of the libraries, or the features of the ABV tools themselves. However, these "external" factors are not important until the verification challenges and the hard-to-verify hot spots in the design are clearly identified. In other words, these users failed to identify the "internal" verification deficiencies that drove them to consider ABV in the first place. For this reason, we recommend first applying ABV to the verification hot spots. By focusing ABV on verification hot spots, a design team can adopt ABV incrementally, concurrent with their simulation-based methodology. This has the added benefit of minimizing the risks involved with adopting a new methodology while maximizing the return-on-investment. It is this area of ABV that we will discuss in this article.

Verification hot spots

A verification hot spot is typically difficult to verify because it contains a great number of sequential states; it is deeply buried in the design, making it difficult to control from the inputs; it has many interactions with other state machines and external agents; or it has all of the above characteristics. Therefore, a verification hot spot cannot be completely verified by simulation alone - the amount of simulation and the difficulty of creating a sufficient input vector set are simply prohibitive.

The value of a verification hot spot solution is that it captures and makes explicit the knowledge of how to effectively use formal verification and simulation together to fully verify a section of logic. In this way, the expert knowledge of one user can be transmitted to others. This knowledge includes such items as how to capture the right assertions for a verification hot spot; what mix of formal and simulation analysis is appropriate; what input constraining methodology is effective for the verification hot spot; what metrics need to be measured; and what the metric goals need to be.

To identify the most common verification hot spots that designers experience, we conducted a comprehensive review with each design team. During each review, the following questions were used to lead the bug exploration discussion.

In the previous project:

Where did you find the most bugs? Which verification approach or approaches found the most bugs? What bugs were found after tape-out?

In the current project:

Which modules are difficult to verify? Which modules are you concerned about? Which modules are highly connected with the rest of the design? Where is the new logic in the design?

In the following sections, we describe five selected verification hot spots found in most designs. The overall process to deploy ABV on the verification hot spots is:

Identify the hot spots in the design. Capture the hot spots properties as assertions. Apply the right ABV methodology.

Figure 1. Five common hot spots.

Hot Spot #1: Resource Control Logic

Computation resources, system on-chip buses, inter-connections, buffers, and memories are logic structures usually controlled by arbiters and complex control logic. When creating directed tests for the design, verification teams tend to focus on the high-level specifications. They seldom stress the corner cases of the resource control logic, as a result, some problematic scenarios are not observed.

Properties

Ensure the requests are generated correctly based on the mask, the weight, the credit scheme, and so on. This is done by using procedural descriptions to generate the "glue logic" associated with the corresponding assertions. Ensure the arbitration scheme is correct. For straight-forward arbitration schemes (such as round-robin, priority, least-recently-used, and so on) the arbiter checker from an assertion library can be used directly. Ensure the resource (bus, interconnect, memory) is addressed by only one master at a time. This can be done with an assertion language or with the mutex checker from an assertion library. Ensure the resource is de-allocated before it is allocated again. Semaphores lock and release the common resources that do not allow multiple simultaneous accesses. Such locks should be set before an access.

Methodology

If the design is well modularized (i.e., the targeted control logic is self-contained), formal model checking can be applied early-even before the simulation environment is ready.

In a typical system, resources can be requested at any time and allocated in any sequence. Verifying all possibilities with simulation is tedious (if not impossible). Alternatively, by capturing the environmental assumptions as assertions, formal model checking can analyze exhaustively all possible scenarios and detect any potential resource conflict. Once the system simulation environment is ready, these assumptions can be validated in the system environment.

Hot Spot #2: Design Interfaces

Inter-module communication and interface protocol compliance are infamous for causing a lot of verification failures. When design teams first integrate all the blocks together for chip-level simulation, the blocks usually fail to "talk" with one another. To catch this problem early, assertion-based protocol monitors are added to instrument the on-chip buses and the standard and common interfaces. During simulation, each protocol monitor verifies that the modules communicate correctly with its associated interface. By collecting statistics and coverage information at the same time, these monitors also measure the effectiveness of the regression environment.

Properties

Ensure the correctness of the protocol on all of the bus interfaces, especially when there are different modes of operation. As the popularity of standard assertion languages increases, more assertion monitors for standard bus interfaces will become available. Ensure the transparency of the interfaces. This property ensures that the interface does not lose transactions. For example, in a bus bridge design, transactions on the master interface should be reflected at the target interface. These requirements can be expressed with an assertion language using temporal properties.

Methodology

Unlike testbench-oriented monitors developed using Vera or 'e', monitors written with an assertion language can be used with both simulation and formal verification. In addition, assertion monitors track simulation coverage and statistics information, which provides a means for gauging how thoroughly bus transactions have been stimulated and verified.

Assertion monitors are useful for verifying internal interfaces as well. Such interfaces have ad hoc architectures, so they are particularly prone to mistakes caused by misunderstanding and miscommunication. We recommend minimizing the extent of such internal interfaces and simplifying the handshake protocols. For example, rather than incorporate several different internal interfaces, standardize on a single interface that uses a simple handshake scheme.

Coverage and statistics information is as important for the internal interfaces as it is for the external ones. Such information confirms the flow of data through the design architecture and highlights any potential bottlenecks.

To validate the transparency of an interface, we must ensure that the transactions are interpreted and transferred correctly. For example, assume the design is an AHB-to-PCI bridge, we must ensure that:

Every PCI transaction initiated by a PCI master is converted to the corresponding AHB transactions. Every AHB transaction initiated by an AHB master is converted to the corresponding PCI transaction.

Simulation with assertions can validate the one-to-one mapping of the basic transactions. However, to be thorough, we have to ensure that the illegal, error, and retry transactions are also handled correctly.

Hot Spot #3: Finite State Machines

For verification purposes, we classify finite state machines (FSM) into two categories: interface FSM and computational FSM. Interface FSM use I/O signals with well-defined timing requirements. Examples of interface FSM are bus controllers and handshaking FSM. Computational FSM do not involve signals with explicitly defined timing requirements. Examples of computational FSM are FSM for flow charts and algorithmic computations.

Properties

Typically, specifications for interface FSM are derived from waveform diagrams. It is crucial to ensure that the FSM correctly samples the input signals within the time period and that the response signals are asserted within the output timing specification. It is natural to express these timing requirements with an assertion language using temporal properties. Typically, specifications for computational FSM are derived from control flow graphs, which are common in engineering documents and standard specifications. To improve performance and/or simplify implementation, a flow graph might be partitioned, flattened, re-timed, or pipelined into multiple FSM. But, regardless of the optimization performed, they should still mimic the flow graph correctly. Implementing a control flow graph with assertions captures its specification in an executable form. These assertions then ensure that all of the FSM decisions and transitions are made correctly. Such assertions can be implemented with a mix of procedural description and temporal properties.

Methodology

During simulation, assertions monitor activities inside the design and provide information showing how thoroughly the test environment covers the design's functionality. By capturing the properties of FSM using assertions, we can identify them easily, exercise them completely, and collect cross-product coverage information during the simulation process. In addition, the implementation of the FSM also has a direct affect on the effectiveness of verification.

When several FSM are interacting with each other, it is important to ensure that they do not get "trapped" in a corner-case behavior. Formal verification can be applied to check this situation. However, formal model checking is not efficient with complex properties which are unbounded. Hence, the high-level timing requirements of a FSM may have to be decomposed and captured within several assertions.

Hot Spot #4: Clock-domain Crossings

The challenges of designing clock domain crossing (CDC) logic are well known. The static portion of the problem can be addressed with automatic analysis of the RTL code and netlist. However, the dynamic portion of the problem is not so well formulated. Each CDC signal has a set of properties to be verified. As the implementation requirements for the control and data signals are different, they should also be handled separately.

Figure 2. Clock Domain Crossing signals.

Properties

Ensure that the CDC control and data signals are synchronized correctly in order to avoid the metastability problem. Ensure that the CDC signals are stable long enough to be sampled correctly. Consider the example in Figure 1. Control signal c must be held stable for two or more clock_b cycles (depending on the frequencies of clock_a and clock_b). Data bus d must be held stable from the time sel_a asserts, during the time the control signal propagates across the clock domain boundary to assert sel_b, and until the propagated value of d's output from the multiplexer is latched by the destination register. This example is a common CDC protocol. Other CDC protocols use similar interface handshakes. They can all be captured as temporal properties. Ensure that logic driven by reconvergent CDC signals (i.e., CDC signals that are recombined in the target clock domain) is tolerant of the variable delays caused by the CDC synchronizers. This problem cannot be verified with simulation alone. When simulating the RTL version of a design, synchronizer delay is always two clock cycles. However, in silicon, the synchronizer delay may vary (depending on the data/clock relationship). Reconverging CDC signals with these random delays can cause undesired pulses to be generated, causing logic in the target clock domain to malfunction. Hence, assertions should be placed in the reconverging logic structure to catch any potential problem.

Methodology

Static CDC design rule checks are available from several popular netlist analysis tools. They can be run automatically. We recommend doing this as soon as the RTL is created. These checks are similar to synthesis design rule checks, which should be performed before the RTL code is integrated into simulation regressions.

Once the synchronization structures are in place, the assertions that capture the CDC protocols can be verified in simulation concurrently with the design functionality. The CDC protocol assertions ensure that CDC data are stable across clock domain boundaries and that the receiving logic in the target domain samples the data correctly. Unfortunately, experience has shown us that functional simulation alone does not cover or stress the CDC paths sufficiently. Hence, coverage information from the CDC assertions must be reviewed and holes in the regressions must be filled.

To simulate the effects of CDC metastability and detect any reconvergent problems arising from reconvergent CDC signals, random delays can be introduced into the paths of the CDC signals. This process can be automated using reconvergent path analysis and by inserting metastability effect generators.

Hot Spot #5: Data Integrity

Devices such as bus bridges, DMA controllers, routers, and schedulers transfer data packets from one interface to another. One goal of verification is to ensure the integrity of the data during these transfers. Data packets must transfer correctly-even if they are re-ordered, de-multiplexed and multiplexed, or segmented and re-assembled during the process.

Unfortunately, in a system-level simulation environment, data integrity mistakes are not readily observable. Usually, problems are not evident until the corrupted data is used. With ABV, assertions check the integrity of data along the entire data transfer path. A lost or corrupt data packet is detected immediately.

Properties

Ensure key registers (program counters, address pointers, mode/configuration registers, status registers, and the like) are programmed correctly and their data are never lost. Key registers contain precious data that must be consumed before being over-written. Assertions can ensure these registers are addressed, programmed, and sampled correctly. An assertion language can capture these properties by probing into the registers hierarchically. Ensure data going through a queue is not lost or corrupted. Data transferred through a queue (such as a FIFO structure or a layered bus interface) must follow the first-in first-out scheme without any alteration. The best way to capture this property is to use an approach that mixes both an assertion language and an assertion library. The assertion language readily captures the enqueue and dequeue protocol conditions. Instead of manually creating the data integrity assertion, we use a data integrity checker from the CheckerWare® assertion library. The checker ensures that: No more than n transactions are ever stored in the queue. No outgoing transaction is generated without a corresponding incoming transaction. Data written to the queue is not corrupted. Ensure tagged data in the system is not lost or corrupted. In many designs (for example, data switches and routers), data is stored temporarily before being transferred. A tag is a handle on the data content; it can be an ID, an address, or a header. Structures that store and retrieve data can be verified using checkers (for example, the memory and scoreboard checkers from an assertion library). The type of storage structure is not important. For example, the storage structure might be a simple 2D array or a DDR-SDRAM with a memory controller. The objective is to ensure the data stored in memory is not corrupted, the read/write ordering is correct, and the address has no conflicts.

Methodology

End-to-end, simulation-based verification methodologies transfer many data packages; therefore many of the data integrity assertions are thoroughly exercised. However, simulation typically fails to stress test-storage elements by filling up the FIFOs/memories. Thus, pseudo-random simulation environments should be guided by coverage information from the assertions. This can be done manually (by fine tuning the random parameters) or automatically (using a reactive testbench that monitors the assertions).

To compound the issue, multiple queues and data streams might transfer and retrieve data at unpredictable intervals. Simulation alone cannot verify all of the corner-case scenarios-there are simply too many of them. Instead, formal model checking is used to target the remaining data integrity assertions. It can explore all legal combinations of transfer events to ensure the data is never corrupted. When we examine the bugs found with this methodology, they are all related to complex combinations of events initialized by different data transfers. An example is described in the next section.

Verification results

By identifying and focusing on the verification hot spots in the designs, we have helped many design teams deploy ABV successfully. The designs represent a wide range of applications, including a processor chip-set, an I/O hub, a Gigabit Ethernet controller, a networking switch, a storage network controller, and several SoC platforms for mobile devices and consumer electronics. The challenges of the five verification hot spots were experienced by all the design teams. Table 2 summarizes the verification hot spots from two of the designs.

Verification Hot Spot Bugs Found

ABV is a relatively new verification methodology. So when most of the teams deployed ABV, they had already performed a significant amount of functional simulation. Hence, they did not experience one direct benefit of the ABV method, which is finding bugs early in the design cycle, concurrent with functional simulation. But, by concentrating on the hot spots of the designs, the teams found difficult bugs. These results boosted confidence that tape outs would be successful. Table 3 gives a summary of bugs found at the five verification hot spots.

Customer methodology

It is not surprising that most of the bugs were found at the CDC and design interface hot spots. The methodologies for these two verification hot spots were straightforward to deploy. The static CDC design rule checks were performed automatically (without assertions). As a result, all the design teams used it extensively.

For the bus interfaces, standard bus and memory interface monitors were already available through the CheckerWare library, which includes protocol monitors that check for violations during simulation, collect detailed functional coverage metrics, and provide both checks and constraints for formal verification. The protocol rules had been captured as assertions, so the effort to use the monitors was minimal. All of the teams employed protocol monitors to verify the standard interfaces and incorporated them into their simulation environments.

A few design teams also leveraged the monitors as interface constraints for formal verification. In this configuration, model checking can only analyze legal transactions.

We also analyzed how the teams added other assertions. Typically, verification engineers added assertions capturing the test plan criteria. Design engineers added assertions for verifying the implementation structures.

We have seen "bug triage" time improve significantly with assertions, especially with directed random simulations. In a directed random simulation, once a bug has taken effect, many cycles can pass before the bug propagates and the simulation fails-if indeed the simulation fails at all. Assertions simplify the identification of the root causes of problems when they catch bugs at their sources.

Most of the design teams put significant effort into the resource control logic and data integrity hot spots. Assertions for resource control logic were the easier of the two to capture. Checkers from the CheckerWare assertion library were used extensively. Since most simulation environments did not stress-test the resource control logic sufficiently, formal model checking was used. On the other hand, the assertions required to capture data integrity properties were complex. For example, when data was re-packaged or when packages were dropped intentionally. However, once these complex assertions were in place, they can be verified with various methodologies.

The data integrity and the resource control logic in some of these designs were especially difficult to verify. They represented an essential part of the test plans. So, the effort was well spent. Importantly, the bugs found at these hot spots were both critical and obscure. None would have been found with traditional verification methodologies.

For instance, one of the designs had a high-speed communication link interface. There was a logic bug such that if a re-transmit was requested and queued, and the re-transmit counter was equal to max-1, and a multi-bit error arrived on the receive interface, then the re-transmit data at the head of the retransmit FIFO would be lost. This was caught by the data integrity assertion before massive data corruption had occurred downstream. In this case, the bug was never detected in simulation. Handwritten tests did not target the bug, and extensive pseudo-random simulation never created the right combination of events in the right order. Formal verification triggered this corner-case behavior. Model checking, with a starting state from simulation, found the combination of events that caused the control-logic to dequeue the FIFO prematurely.

Conclusion

Assertion-based and formal verification are important tools in a full verification toolkit. Their benefits have become obvious and essential to the many design teams with whom we have worked. By allowing assertion-based and formal verification tools to solve specific problems in existing verification flows, the verification hot spot methodology helps design and verification teams reap the benefits of these technologies without having to climb a steep learning curve.

As we have experienced, strategic deployment of the ABV methodology on hot spots has proven effective. This approach applies scarce verification resources to areas that need them most. It improves verification efficiency and boosts the overall quality of the design. We have found that verification plans that incorporate these techniques can enjoy a verification productivity improvement of more than 10X.

The five prominent verification hot spots discussed are not the only hot spots for verification. Yet design teams can leverage the knowledge developed through them to identify and address the hot spots specific to their designs. We recommend each design team conduct an internal review to explore the unique hot spots in their designs. Knowing the verification hot spots is half of the battle.

By Ping Yeung and Vijay Gupta

Dr. Ping Yeung is Director of Verification Methodology at 0-In Design Automation, Inc. His primary responsibility is helping companies incorporate assertion-based verification methodologies into their IC development projects. Since 0-In released its assertion-based technology and methodologies several years ago, Dr. Yeung has been working with several companies to adopt assertion-based verification. Some chips designed using the 0-In assertion-based verification technology already have taped out successfully.

Vijay Vardhan Gupta has over 10 years of experience in ASIC design and verification. Prior to 0-In, Vijay worked for a number of component and system design companies, including Intel, Agere, and Adaptec. His major contributions have been in the logic design, verification, and ASIC implementation space. Vijay holds a B.S. in Electronics Engineering from MNR Engineering College, University of Allahabad, India.