Developing Assertion IP for Formal Verification

By Manoj Kumar Thottasseri, Synopsys, Inc.
Gaurav Gupta, Synopsys (India) Pvt. Ltd.
Mandar Munishwar,  Synopsys, Inc.

ABSTRACT

Assertion language provides a way to express the properties and constraints for property based formal verification environment. Current assertion languages such as SVA and PSL offer a great set of constructs that enables one to write assertions in number of ways. Most of these assertions work very well in simulation; however some of these may not be usable effectively in a formal based verification environment. The logic implied by some of these coding styles can be very heavy for a formal tool to handle and can slow down or make the formal verification closure impossible to achieve. An assertion IP for formal verification must be architected such that it can work efficiently with any formal tool. This paper covers certain coding guidelines which should be considered while developing a formal friendly assertion based IP.

INTRODUCTION

Assertions are key ingredient to today’s property based formal verification environment. Industry standard assertion languages such as SVA and PSL have a very strong formal friendly assertion constructs that help the user to express their complex design behavior at a high level of abstraction. Although the language permits user to express the complex temporal assertion behavior in a concise way, it often yields complex logical behavior at lower level depending on the coding style used to write the assertions. Writing efficient assertions, especially formal friendly assertions, usually involve a longer learning curve not only to interpret the assertion constructs correctly but also to use them in a more effective and accurate ways.

In formal verification, assertions are used to define the property to be proven by formal methods as well as to define the constraint environment (valid inputs) for the Design under Test (DUT). The effectiveness and completeness of Formal Verification greatly relies on the accuracy of these assertions. A major part of the formal verification effort is spent on creating a robust set of properties and constraints. This development burden often slows down the easy and useful adoption of formal technology into the design verification process. The wide adoption of industry standard protocols to define the design interface specification has made it possible to create a pre-verified set of assertion IPs that are is re-usable across different development projects.

Given the rich set of language constructs that SVA and PSL offer, it is important to develop an Assertion IP in such a way that it uses constructs and auxiliary variables that are not only supported in formal verification tools but also efficient for the formal verification process. Majority of today’s industry standard protocols involve pipe-lined, multi-threaded control or data transfer that often requires large amount of data storage for successful tracking and evaluations of design properties. Memory logic implemented to account for these storage requirements needs to be architected in a favorable way for the Assertion IP to be usable with formal verification, as more storage elements can consume the capacity of formal tools ending in poor quality of results. For successful deployment of Assertion IP in a formal verification process, it is important that, logic inferred by Assertion IP is efficient and fits within the limitations of existing formal technology

Assertion IP also should consider handling temporal nature of some of the design properties. Large temporal window need to be handled such that there is no state-space explosion and formal algorithms can produce results while the assertions meet functional requirement.

As assertions often involve multi-cycle evaluations, it can lead to conflicting assumptions at any given time from one or more different assertion evaluation threads. In a pure formal world, these conflicting assertions can easily get masked resulting in over-constrained environment, which can miss a design bug or produce false positive results. These conflicting assertions will be exposed while using these constraints in a hybrid verification environment that uses these constraints for stimulus generation during random simulation. A hybrid formal tool that uses the assertion based constraints to generate the constrained random stimulus can therefore be used to debug the assertion conflict; a major and challenging part of verifying the assertion IPs.

This paper describes the practical experience of authors in developing Assertion IPs for popular protocols like AMBA, OCP, PCI and several others. We propose Assertion IP development guidelines in terms of formal friendly coding styles, efficient modeling of storage requirements to minimize memory footprints, avoiding and debugging constraint conflicts such that, it can significantly improve the quality of results from the formal verification tools.

DEVELOPMENT GUIDELINES

Following are the different coding guidelines proposed by the authors.

Avoid large temporal windows

Every assertion expressions must be written such that the amount of sequential elements inferred by the assertion or the logic required to model the assertion is minimal. The complexity of formal proof increases exponentially to the number of sequential elements involved in the property. Larger time bounds on the delay check can infer a large amount of sequential elements and thereby causing overhead for the formal tools. The cycle delay operators and repetition operators in the assertion languages should be used with moderate number of cycles.

For example, OCP Protocol does not specify the latency between a valid response on the OCP Slave interface signal - SResp and the OCP-master response acknowledgement signal – MRespAccept. However, in order to avoid large delay between these two signals, there may be a latency check to make sure that MRespAccept signal is asserted within an expected time period. In the normal case, this property can be written using the assertion in SVA as shown in Figure-1

Figure 1

The above assertion can significantly slow down the performance of a formal tool, if the value specified for the parameter LATENCY is a multi digit value. The delay construct, ##, in the above expression will infer a shift register of depth

“LATENCY” and it will involve that many number of sequential elements. If the property definition demands for a large amount of delay/repetition, an alternative method of coding may be possible.

For example, if the above property specification does not involve overlapping transactions, this delay checks with ## operator can be replaced by a static delay counter as shown in Figure-2.

Figure 2

Avoid large amount of data storage

Some of the industry protocols like OCP and AXI are highly configurable, multi-threaded and pipelined in nature. These protocols require a large amount data buffering for validating the interface behavior. In theory, this would require the buffering all outstanding transactions on the interface using Multi Dimensional Arrays (MDA). For example, in the case of OCP checker, independent buffering would be required for each thread and tag combinations. The MDA structure for this combination would look as shown in Figure-3.

Figure 3

The number of sequential elements in the design increases substantially with the increase in number of threads and tags and the complexity of formal analysis increases exponentially with increase in sequential elements.

The disadvantage of the above methodology is that it does the book keeping of each and every thread

X tag combinations, even though there are no pending transactions on most of them. Additionally, it would also require creating individualized assertions for each and every combination of thread X tags as shown in Figure-4.

Figure 4

The above methodology requires large amount of redundant data to be maintained unnecessarily while the required amount of data to be kept may be marginally low. It is possible to control and minimize the data storage by replacing the individualized memory for each and every threadXtag combinations with a Content Addressable Memory (CAM) that stores the information only for a predefined number of outstanding transactions irrespective of the maximum possible combination of threads and tags. The details of the CAM structure and how it can help reducing the memory are explained below.

Reconfigurable Content Addressable Memory

Content Addressable Memories or CAMs are popular parallel matching circuits. They provide the capability in hardware to search a table of data for a matching entry. Standard computer memory (Random Access Memory or RAM) involves the user supplying a memory address and the RAM returning the data word stored at that address. However, "reading" the CAM involves providing input data to be matched, followed by searching the CAM for a match so that the address (index) of the match can be output.

The maximum buffering for each required data is limited to the amount of pending transfers specified. There is no exclusive buffering for each thread and tag possible. Moreover, for the specified number of outstanding transactions, the amount of sequential logic will be significantly reduced as buffer (CAM) size is independent of number of threads and tags.

In this approach, whenever there is a new request, the IDs and other input information would be stored in a CAM at its available free location. The index of the CAM location where data will be stored will be dynamically incremented/ decremented based on a new request/response (or in case of OCP, request/data based on configuration settings, like response phase disabled and/or data handshake phase disabled). Figure-5, depict a typical CAM structure used to fulfill buffering requirements of OCP checker.

Figure 5

Figure-6 shows some examples of CAMs used in the OCP-Assertion IP.

Figure 6

On a request, data or response, the contents of the ID Cam will be matched for the appropriate ID and the matching index location will be determined. This matched index will be used to access the rest of the arrays for required information. Once the required data is retrieved, which may be from any location, the remaining elements with higher index in the CAM will be shifted up to fill in the empty space. See figure-7

Figure 7

An example code on finding the matching index is shown in figure-8.

Figure 8

Once the CAM structure is ready, assertions can be easily integrated to the existing CAM structure using index (id) corresponding to the phase. Only one instance of the assertion is needed to monitor all possible thread and tag combinations. An example is shown in Figure-9.

Figure 9

Avoid conflicting assertions

As the assertion languages provide a way to represent complex temporal behavior in a single expression, it often causes conflicting scenarios which are hard to determine by the assertion developer. These conflicts can be either between multiple assertions or from the different threads of the same assertion. These conflicting assertions, when used as assumptions or constraints for formal tools, can cause over constrained environment that can miss a possible bug in the design. So it is important that these assertions are corrected such that the conflicting scenarios are removed to use them flawlessly in the formal verification environment.

Conflict from multiple properties

It is common to find conflict between multiple constraints especially when they are temporal constraints. For example, consider the following two SVA PCI constraint properties written to constrain the Target interface of the DUT.

Figure 10

The property e_SnpsPciTP03 says that whenever there is a reserved command issued by the master, then the devsel_n signal should not be asserted or high for the next four consecutive cycles.

The second constraint property, e_SnpsPciTP04 specifies that, once the transaction is started, then Target should assert the devsel_n command within the next four clock cycles.

These two constraints will obviously conflict when the transaction is started with a reserved command, as e_SnpsPciTP04 specifies the devsel_n to be asserted while devsel_n specifies this signal to be deasserted. The above example is very straight forward and simple for easy understanding. In reality, the conflict caused by complex assertions can be very hard to determine as the conflict could happen anytime during the progression of different threads of a single or multiple temporal expression.

In order to resolve the conflict demonstrated in figure-10, it is mandatory that the evaluation of these two assertions is happening in mutually exclusive fashion. To make them mutually exclusive, the condition at which the constraints become in effect must be made mutually exclusive. Therefore the precondition (antecedent) of the implication in the property e_SnpsPciTP04 should be modified such that it is not evaluated when the expression b_reserved_command is true. The modified version of the expression is shown in figure-11.

Figure 11

Conflict between different threads

Often these conflicts can occur from the different temporal threads of the same assertion. In that case the conflicts will be even harder to determine. For example, consider the following constraint rule that the signal done_n should be asserted for one clock cycle after 4 clock cycles from signal last_tfr is asserted, where done_n is a primary input signal while last_tfr is controlled by the output of the design. One may write the assertion for this rule as shown in figure-12.

Figure 12

Figure 13

Now, consider the case when last_tfr is asserted consecutively for two clock cycles as shown in figure-13. There will be two evaluations started at time [1] and time [2]. The evaluation that started at time [1] would require done_n to be LOW at time [5] and to go HIGH again at time[6]. However, the evaluation started at time [2] will require done_n to be LOW at time [6] causing a conflict at [6].

The issue here was that the assertion developer did not realize about the case where last_tfr get asserted consecutively for more than one cycle. To fix the conflict, the assertion in this case may need to be split into two and can be re-written as shown in figure-11.

Figure 14

In figure-14, e_singlePhase_dataXfer_multi will make sure that done_n is asserted for one clock cycle after 4 cycles from the assertion of last_tfr when last_tfr is asserted consecutively for more than one cycle. Property ie_singlePhase_dataXfer_end will make sure that done_n is asserted for one clock cycle and also make sure that it goes LOW on the next clock cycle.

Conflict due to missing constraints

Often there are cases where two constraints can have conflicting implications when the causes of the implications are not mutually exclusive. As an example, consider the following two constraint properties

1. Signal data_ready should be high on the next clock cycle, when the signal xfer_begin is asserted.
2. Signal data_ready should be high on the next clock cycle, when the signal xfer_end is asserted.

Where data_ready, xfer, begin and xfer_end are controlled by primary inputs of the design.

Figure 15

It is obvious that the above two constraints will imply conflicting values on data_ready whenever xfer_begin and xfer_end get asserted at the same time. This implies a new constraint between xfer_begin and xfer_end that they should be mutually exclusive. Although, this kind of conflict will not affect the formal results, it may affect the formal performance. So adding the missing constraint, as shown in figure-16, can be helpful.

Figure 16

The constraints discussed in the above sections will be hard to determine in a pure formal based environment. However, the same can easily catch in “Hybrid Formal” tools as it also employs simulation to replay the constrained random stimulus. These conflicts will appear as unsolvable constraints in hybrid tools, and will provide appropriate error/warning messages to fix them. Magellan, a property based hybrid-formal verification tool from Synopsys, reports these conflicts as dead-ends and provides useful tips to fix them.

Avoid constraining the outputs

Constraints are written to control the input of the design. The constraint properties should be written such that the constraints can be evaluated to be true solely by controlling the input values. This means that, even if output signals appear in the constraint expression, the tool should be able to evaluate the expression true every time independent of the value of the output signal.

For example, consider the following assertion which tries to constrain the value of input signal tready based on the value of the signals mready and mvalid., where in mready and mvalid may be design internal variables or design outputs

Figure 17

The problem here is that, in order to ensure the constraint is always valid, mready must be asserted for every time mvalid is true. As mready is controlled by the design itself and not by the formal tool, it may fail to make the whole expression true, if mready gets a logical value of false. In order to make the constraint expression solely depends on the primary input value, the code may be re-written as follows.

Figure 18

The conjunctive association of input and the design controlled variable (tready and mready), through “&&” has made the constraint to be a dependent of the signal mready. If this was disjunctive association through “||” operator, the constraint shown in figure-18 would have been acceptable.

CONCLUSION

Some of the coding practices for developing formal friendly assertion based IPs have been discussed. The recommendations include remodeling of memory intensive logics, dealing with longer temporal expressions, steps to diagnose and re-code the constraints that cause conflicting results. These coding guidelines have been written based on the experience in developing Assertion IP based constraint environment for formal verification.

REFERENCE

[1] Janick Bergeron, Eduard Cerny, Alan Hunter, and Andy Nightingale, (VMM) Verification Methodology Manual for SystemVerilog Published in 2005.

[2] Jin Hou and Dan Benua, Managing Capacity Limitations During Formal Verification of Assertions, Proceedings of DV Con-2006

[3] Eduard. Cerny, Janick Bergeron, and Manoj Thottasseri. Guidelines for System Verilog Assertion IP Development, Proceedings of DV Con-2006