February 2, 2007 -- SystemVerilog Assertions (SVA) constitute a major language feature of the IEEE Std. 1800-2005 SystemVerilog standard. Local variables are a powerful component of SVA that allow the sampling and manipulation of data in a property or sequence without requiring the property writer to define auxiliary state machines to model additional behavior when composing the property or sequence.

During assertion evaluation, local variables dynamically allocate storage to hold the sampled data for later reference. Theoretically, this unique capability enhances the expressiveness of the language allowing SVA to model extra temporal behavior concisely, which otherwise requires auxiliary modeling or obscure rewriting to specify the desired behavior. For example, local variables are often used to express a class of properties associated with data integrity—such as a data packet properly traversing through a design block. However, the enhanced expressiveness of SVA also adds considerable complexity to the assertion and its evaluation.

In simulation for certain local variable use patterns, the amount of dynamic storage required to remember the sampled data can be huge and essentially has no upper limit, resulting in increased memory use and potential performance degradation. With formal verification, local variable constructs are compiled into extra sequential elements in the checker; the increased checker complexity thus reduces the effectiveness of the underlying formal algorithms considerably. Unfortunately, these added complexities may prevent users from applying local variables effectively.

A set of coding guidelines and a methodology for efficient SVA local variable will help you take advantage of the expressiveness of SVA local variables while avoiding the potential pitfalls that would result in reduced performance and capacity.

Concurrency issues with local variables

The complexity of local variables might contribute to tool execution performance problems due to potentially huge memory requirements and increased concurrency. In particular, you should avoid using local variables that trigger exponential growth in required memory, which are beyond the capacity of simulation and formal verification tools.

In SVA, sequence operators that allow the choice between several possible sequences add concurrency to the property description. When properties are simulated, concurrency due to the choice operators is typically modeled as multiple threads of execution. However, in formal verification, concurrency due to the choice operators appears as an increase in the state space of the model.

Typically, the amount of resources required in simulation or formal verification to model the property is fairly modest. Often, some form of optimization is possible to reduce the synthesized model for assertions containing concurrency. However, sometimes concurrency can pose real difficulties in modeling the assertion or requiring considerable resources.

When properties are described using both local variables and the choice operators, the concurrency introduced can be much more complex and difficult to optimize. This is primarily due to the semantics of SVA with local variables—the state of local variables bifurcates in different parallel branches of choice operators and it might not be possible to merge them at a later point.

For example, in simulation the local variable valuations split at choice operators. Therefore, if an assignment to a local variable occurs on one side of the two threads, it will typically exist from that point forward—each of the two threads containing a different valuation of its copy of the local variable.

In fact, it is possible to construct some properties using local variables that can cause an exponential growth of the number of threads and local variable storage. For these properties, certain input sequence can trigger the exponential growth and lead to an out-of-memory condition in a simulator within a few cycles.

Simulation local variable coding guidelines

In general, you should avoid using choice operators where there is the possibility of branching. Performance issues can be avoided by insuring that the conditions of the different branches of choice operators are mutually exclusive.

For example, Figure 1 illustrates the execution of sequence (S1 or S2). Let c=c1 represents a condition in S1 under which S1 executes. Similarly, let c=c2 represents a condition in S2 under which S2 executes. If c1 and c2 can both be true, then both threads will exit the or operator with possibly different local variable valuations L1 and L2. You can avoid this scenario if the conditions of S1 and S2 are mutually exclusive.

Figure 1. Choice conditions and the or operator.

Figure 2 illustrates a problematic situation involving a choice repetition operator used as part of a sequence composition. For example: S1[*0:$] ##1 S2.

Figure 2. Repetition operator leading to many threads.

S1 may repeat zero or more times followed by S2. If the conditions of S1 and S2 are such that S2 can execute in parallel with a repetition of S1, this scenario can lead to increasing numbers of threads, each with different valuations. For example, Figure 3 demonstrates coding styles for bad and good mutually exclusive conditions.

Figure 3. Mutually exclusive conditions.

In Figure 4, we illustrate both bad and good coding practices specifically related to local variables and sequence composition with a repetition operator. Our good coding example adheres to guideline 2, which states when using a sequence repetition operator, the condition for repeating the sequence and the condition for executing the next sequence should be exclusive. This concept is illustrated in Figure 2, where condition c2 and condition c1 are not exclusive, excessive threads can be generated.

Figure 4. Sequence composition with repetition operator.

GUIDELINE 1: Avoid non-exclusive choice with the sequence or operator and local variable assignments.

GUIDELINE 2: Make sure when using the sequence repetition operators that the conditions for repeating the sequence and executing the next sequence are exclusive, especially when manipulating local variables.

GUIDELINE 3: Check for thread blow-ups and excessive concurrency by tracking max thread counts per assertion during simulation, or use a profiling tool.

GUIDELINE 4: Use a thread debugger to understand concurrency issues.

Formal verification local variable guidelines

Guidelines 1 through 4 reduce overhead due to unnecessary concurrency—thus avoiding blowups in simulation. Formal verification also benefits from these coding guidelines. However, formal verification requires additional coding guidelines. In formal verification, performance problems occur if the logic required to model the local variables becomes excessive. In simulation, dynamically creating and terminating threads is easy, but for a hardware model (such as a checker) we need to statically determine the resources when the assertion is compiled.

There are a number of techniques we can use to help in the modeling concurrency in a formal verification models (which are beyond the scope of this article). However, keeping the synthesized model small is paramount to achieving good performance during formal verification. We propose several patterns for efficient use of local variables with formal verification. By using these patterns, you will ensure that the overhead required to model the local variables for formal verification is bounded and manageable.

Fixed delay pattern

Reads of a local variable always follow a write after a bounded or fixed number of cycle delays.

Figure 5. Fixed delay pattern.

Fixed delays from write to read can be on the LHS or RHS or across an implication. This style allows for synthesis of a pipelined implementation that supports overlapped execution of successive LHS matches

Figure 6. Pipeline implementation for fixed delay.

Guideline 5: For formal verification, use a fixed delay write/read pattern with local variables.

Single thread/single register per variable pattern

The property in Figure 7 shows pattern for an assertion evaluation that produces exactly one thread because the starting condition for the LHS and RHS are mutually exclusive. In this situation, the model generated for formal verification needs only one register for each local variable, minimizing the amount of complexity.

Figure 7. Single thread pattern.

GUIDELINE 6: For formal verification, use a single thread per assertion pattern with local variables.

Single thread per transaction pattern

Relaxing the single thread per assertion evaluation, the property in Figure 8 shows an example where the local variable does not fork multiple threads per transaction. Although the LHS can match multiple times, each match carries its own local variable valuation to the RHS. Overlapping RHS is manageable in certain situations. Variable delay can be handled, but the time bounds should be as small as possible for effective formal verification.

Figure 8. Single thread per transaction pattern.

GUIDELINE 7: For formal verification, use a single thread per transaction pattern.

Local variable write restriction pattern

Local variable assignments on the LHS of a sequence implication operator can be synthesized for formal verification—with restriction that the RHS side does not contain any local variable assignments. In general, for local variable assignments, we recommend the following restrictions presented in Guideline 8.

GUIDELINE 8: For formal verification, code your properties involving implication and local variables with the following restrictions:

• No local variable assignments within a RHS sequence.
• Overlapping RHS sequences should be bounded.
• Use care with variable delays—keep time bounds as small as practical.
• Use fixed delays from LHS local variable assignment to start of RHS.
• When in doubt, use modeling code (see Guideline 9).

Modeling versus local variables

Although local variables allow concise modeling of certain properties, there are times when auxiliary modeling (outside the property declaration) is best suited for specifying complex behaviors. For example, if we wish to collect statistical information about the various transactions (such as maximum number of unique IDs, maximal count per any ID, or maximum cycles outstanding) we would need a global data structure to capture and track this statistical information. You might be tempted to gather statistic using local variables. However, this approach adds unnecessary complexity to a synthesized model. Intuitively, the rule of thumb is to apply local variables locally with regard to one thread, and use auxiliary modeling when global information (across threads) needs be collected. Moreover, local variables may not be efficient when we cannot statically determine that the storage required to model the behavior is bounded. In these cases, the memory requirement might render the simulation or formal verification ineffective.

GUIDELINE 9: When in doubt, use auxiliary Verilog code to model data manipulation.

SystemVerilog assertions (SVA) with local variables enable you to specify complex properties in a concise form. However, using local variables can result in unacceptable performance during simulation or formal verification if you do not take precautions when coding your assertions. Due to the concurrency expressible in SVA, you may code an assertion with SVA local variables and then be surprised (or may not realize) that the local variables are duplicated in many concurrent threads. The nine Guidelines will help avoid some of the pitfalls you might encounter if your design requires unique storage elements in each thread.

The practical coding style, set of assertion checker coding patterns, and methodology described in this article can be effectively applied to many of today’s common designs and popular IPs. Where the limitations of local variables on properties make them insufficient for modeling certain complex behaviors (such as gather statistics across properties), auxiliary state machines are still required for proper assertion specification. By following these Guidelines, you can take advantage of the expressiveness of SVA local variables while avoiding potential pitfalls resulting in reduced performance and capacity.

By Jiang Long, Dr. Andrew Seawright, and Harry Foster

Jiang is a senior software engineer in the Mentor Graphics Design Verification and Test division, working on assertion synthesis and 0-In front-end compilation. He has over seven years of experience in EDA for high-level functional formal verification of digital designs. He holds a B.S. in Computer Science from Jilin University, China and an M.S. in Computer Science from the University of Texas at Austin.

Andrew is a principal engineer in the Mentor Graphics Design Verification and Test division and leads the 0-In front-end compilation team. He has over 10 years of experience in EDA for advanced design verification and advanced design synthesis. He holds a B.S. in Electrical Engineering from Rutgers University and a Ph.D. degrees in Electrical and Computer Engineering from the University of California at Santa Barbara.

Harry is a principal engineer for the Mentor Graphics Design Verification and Test division. He currently serves as chair of the IEEE 1850 Property Specification Language (PSL) working group. He is the inventor of OVL, the co-author of multiple books and award winning papers on functional verification, and the holder of multiple verification patents.

Go to the Mentor Graphics Corp. website to learn more.