IP Verification : Integrating IP with assertion- based verification

As one of the first tasks in the IP creation process, the IP provider creates a functional specification. Unfortunately, this document is not directly integrated into the design process. It usually is updated only infrequently and is not synchronized when design activity is high. Sometimes the specification is actually written after the IP coding is well under way. Insufficient attention to the functional specification can lead to bugs in the IP and in its use.

Because the specification of the interfaces and protocols is disconnected from the actual IP model, the specification document is the main source of information during IP integration. However, the information can be misinterpreted or, worse, it may be ambiguous. Even if this document is well written, designers may still have trouble deriving the information they need. This leads to bugs in the SoC.

Also, when bugs occur, they are usually detected as symptoms, and not at th e location where they occur. For example, if the SoC drives data into an IP block, and it does not fully adhere to the protocol, the problem may not be found until the data comes back from the IP block. At that time, the data is mangled, having undergone various transformations. It is difficult to debug such problems, especially if the IP is provided as a black box.

Assertion-based verification (ABV) can address the problems in IP integration. With ABV, the IP provider can develop the IP with assertions that express the interface specification in a clear, concise manner. Instead of writing lengthy textual descriptions, the specification can be written in an assertion language designed specifically to describe complex and temporal functionality. Expressing the IP specification in an assertion language reduces the risks of misinterpretation and ambiguity. This alone can make the effort of writing assertions worthwhile. However, a greater benefit of ABV is that these assertions become live verification objects that monitor functionality during the verification process. Suddenly, the specification becomes an active document, and the assertions can help flag problems on the use of the IP.

If the SoC drives data into an IP block that does not contain assertions, the misuse of the interfaces is detected as an effect on data coming back from the IP. In terms of logic, the debugging process takes place far from the source.

However, if the IP contains assertions about the interface, problems are exposed at the location where they appear on the interface. This eases the process of debugging by focusing on the source of the problem. The assertion points out which aspects of the interface were violated and presents specific information about the problem.

Interface specifications can be simple, combinational assertions or complex, sequential assertions that describe temporal relationships. The following examples illustrate assertions written in IBM's Sugar 2.0 language, which the Accellera F ormal Verification Technical Committee selected to be the basis for the industry-standard language.

The assertions shown specify the functionality of a memory access arbiter and controller state machine block. It can perform four operations: Receive Write, Receive Read, Transmit Write and Transmit Read.

Assertion 1 is a simple combinational assertion, which specifies that there can never be more than one request made to the block at a time:

never (( RcvDataWrtReq + RcvDataRdReq + XmtDataWrtReq + XmtDataRdReq ) > 1 )

Assertion 2 is a simple sequential example that specifies that a request for a Receive Write operation can only be true for one clock cycle. If it is true for two clock cycles, the assertion is violated. Assertion 2 specifies forbidden behavior of the interface and reports misuse. It limits the length of the Receive Write request:

never {RcvDataWrtReq [*2] }

If any of these assertions are not met during IP integr ation, the designer must change the design. For example, the block itself could take care of Assertion 1 by storing the request in a queue and relying on a set of rules to determine which queued request to process, particularly when multiple requests occur in parallel. The logic to implement this behavior could be shared between the block itself and the connecting logic outside the block. However, since this block represents IP, its interface is fixed. The use of the IP has to adhere to the specification as expressed in the interface assertions. Therefore, all of the adjustments need to be made in the logic driving the IP. Fortunately, in the verification process, the assertion clearly shows whether a problem occurs on the interface.

Assertions about interfaces can even be used before integration, during the development of the IP and its test infrastructure. For example, when the IP is simulated alone, to verify the IP the assertion checks whether the IP's testbench adheres to the interface and stimu lates the IP according to the specification. These assertions can help in the development of the test infrastructure for the IP block.

Other types of assertions can be used during the development of internal behavior of the IP. For example, Assertion 3 ensures that the state machine goes through the right sequence of transitions for the Receive Write operation. After a Receive Write operation has started (RcvWrtcyc) the state needs to go through a transition from 1 to 2 to 3, then back to 0. This assertion represents required behavior of the state machine for this operation:

{[*]; RcvWrtcyc } |=> { state == 1 ; state == 2 ; state == 3 ; state == 0 }

Assertions can be checked dynamically via HDL simulation. During simulation, assertions report the times when assertion failures occur. It is ideal that assertions never report failures during simulation, so the designer needs to fix the design until no more assertion failures are reported. However, the absence of failure s is not enough to assure confidence in the operation of a design. It is possible that missing simulation scenarios cause the lack of assertion failures.

In more advanced simulation approaches, assertions can also be used to measure functional coverage. It is necessary to know whether assertions failed, and whether they have been exercised sufficiently. With functional coverage analysis, this information can be obtained and the tests adjusted if the functional coverage metrics have not been met. Functional coverage can provide information about individual assertions, about interaction between assertions and about interaction between assertions and the testbench.

Assertions can also be checked statistically with a property checker. Static or formal verification methods can find problems faster than simulation, and potentially be used to explore a larger state space than simulation. They do not rely on testbenches so they can be applied when the testbench is unavailable or when the test scenar ios are not complete or refined. Static methods can find cases where assertions are violated, and they can produce counterexamples to show the scenarios that cause assertion failures.

Although verification with assertion-based verification is generally useful, it's particularly useful for SoC and IP designs. ABV is especially helpful during IP creation and integration. It can improve the quality of the IP and ease the pain in some of the most difficult areas in an SoC design with IP. ABV builds the specification of the interface right into the IP model, making SoC design much more practical and reducing the time spent in debugging.

See related chart