Seven Steps to Create a Formal IP Specification

by Harry D. Foster
Jasper Design Automation, Inc.
100 View Street, #101
Mountain View, CA 94041
harry AT jasper-da DOT com

ABSTRACT

Standardization work is underway to develop assertion languages (for example, PSL and SystemVerilog Assertions) to address the shortcomings of natural language specification. The goal in creating these languages is to give engineers a way to unambiguously specify IP for design reuse—thus providing an automatic path for compliance and interoperability checking in both dynamic (simulation) and static (formal) verification. Yet the approach many engineers are taking in using these languages for IP specification is flawed.

This paper reviews the fundamental elements of today’s emerging assertion language standards, and then discusses missing key elements that are necessary for IP specification. Using this foundation, this paper then presents a technique of combining assertions with a modeling language to specify complex behavior in a “high-level requirement.” This technique overcomes today’s flawed approach that attempts to specify IP using temporal constructs from an assertion language. This paper then presents a set of guidelines and steps for creating efficient and effective verification IP for various verification approaches.

1. INTRODUCTION

With the advent of design reuse and IP-based SoC design, two verification challenges have emerged: verifying that the IP complies with its specification and verifying that the IP is interoperable with other compliant devices (that is, adheres to various interface standards). Fundamental to the process of functional verification is the act of specification. And historically, the process of specification has consisted of creating a natural language description for a set of design requirements. This form of specification is both ambiguous and, in many cases, unverifiable due to the lack of a standard machine-executable representation.

With the emergence of assertion and property language standards, such as the Accellera Property Specification Language (PSL) [1] and SystemVerilog Assertions (SVA) [2], many IP providers are adopting an assertion-based verification (ABV) methodology to provide verifiable forms of IP specification. Adopting an assertion-based specification clarifies ambiguities from the natural language specification and reduces the time spent in verification. And for the IP producer, developing an assertion-based specification for the IP has a collateral benefit—the formal specification process often uncovers misconceptions about the implementer’s original intent. Thus, the time invested in developing the specification is time well spent. And generally, the benefits are realized early in the design and verification cycle, before the IP producer applies any form of verification to the IP [3]. After completing the assertion-based specification, the IP producer can use the formal specification to verify IP compliance and interoperability. For the IP consumer, an assertion-based specification reduces integration time by unambiguously clarifying proper IP behavior under various configurations, while providing a way to verify the SoC’s interoperability with the IP. Finally, for both the IP producer and consumer, assertion-based specification unifies the verification process by creating a single form of specification that can be automatically leveraged across a diverse set of verification tools, such as formal verification, simulation, emulation, and even synthesis [4].

Although data that confirms the benefits of adopting an ABV methodology have been published (for example, HP[3], Cisco[5], IBM[6]), few guidelines exist. Thus, effectively coding an assertion-based specification for IP compliance and interoperability is relatively uncharted waters. And unfortunately, many myths have accompanied the growing interest in using assertion and property languages to specify and verify IP.

This paper examines the myths behind assertion languages in the context of solving the IP specification challenge. It begins by laying a foundation with the fundamental elements of today’s emerging temporal property languages. The foundation prepares you for a discussion of their limitations. This paper then offers an alternative approach to IP specification and a set of guidelines for effective assertionbased specification techniques. Following a good set of guidelines is crucial, for when engineers attempt to formally specify IP without proper guidance, it is not uncommon to generate a specification that is:

• complicated,
• difficult to comprehend through visual inspection,
• difficult to debug, and not always as compact as expected.
  

Finally, this paper presents an alternative form of specification that visually maps well with a traditional approach that typically describes behavior (for example, illustrating behavior in terms of abstract or conceptual statemachines). When combined with conceptual state-machine modeling, we are in a position to express a simpler set of temporal properties to produce a clearer and often more concise assertion-based specification. Furthermore, this approach lets us express a class of data integrity properties that would not be possible by using the temporal constructs of either PSL or SystemVerilog Assertions alone.

2. FORMAL SPECIFICATION MYTHS

Because of the excitement and misunderstanding that surrounds emerging assertion and property language standards, the following myths have materialized. They specifically relate to pure temporal language forms of specifying and verifying IP:

MYTH 1: Temporal Properties are easy to write, read, and understand.

For simple assertions, this is certainly true. However, for creating an assertion-based specification used to verify IP compliance and interoperability, this is not true. Nonetheless, by combining extra modeling with simpler assertions, you will be able to achieve clarity in your assertion-based specification.

MYTH 2: Temporal property languages simplify debugging.

Embedded assertions improve observability, which reduces debugging. However, for simple, embedded properties, an assertion language is not required to improve observability (see OVL [4]). Complex assertions can actually increase the debugging challenge since complex assertions themselves often contain errors. Follow the rules this paper presents and strive for simplicity and clarity in your assertion-based specification.

MYTH 3: Temporal properties are always more compact than automata.

This statement is true for each individual temporal expression. However, often specifying a complex IP block requires creating a set of complex properties. The problem with this approach is that it is not always easy to understand exactly what the block is doing with a large set of properties. For some interfaces, you can reduce a large set of complex properties (involving regular expressions) to a smaller set of simpler properties by combing additional modeling with assertion language constructs.

MYTH 4: All functional properties (required for IP specification) can be expressed using only temporal constructs from a property language.

This is not true. In fact, this paper shows (during the discussion of temporal property languages) that not all properties are expressible purely within the construct of linear-time temporal logic and regular expressions. Furthermore, properties involving transaction ordering or queuing semantics require information storage from various paths of data, which are then used during future data integrity checks. Hence, this type of specification often requires additional modeling to store the transaction information.

MYTH 5: A single form of specification is ideal for all tools (that is, formal verification, simulation, emulation).

This is not always true. As demonstrated during the discussion of Step 1, for efficiency in formal verification, it is often desirable to slice the specification in terms of input paths. Furthermore, there are often many properties we might chose to express that involve timeout counters where abstractions are specified on the counter. The key to the form of specification is to identify the target verification process prior to writing the assertion, as described in the first step in formalizing the VIP process.

During the discussion in the following sections, this paper dispels each of the myths.

3. SPECIFYING CORRECTNESS

This section presents a general overview of today’s emerging assertion language standards.1 It identifies their strengths and limitations and explores ways that they complement each other. It goes on to present a technique of combining assertions with a modeling language to specify complex behavior in a “high-level requirement model.”

3.1. Elements of Assertion Languages

Today’s emerging assertion standards are based on a branch of logic known as temporal logic. The advantage of using temporal logic to specify properties of reactive systems is that it enables us to reason about these systems in a simple way. That is, temporal logic eliminates the need to explicitly describe time when specifying relationships between system events. For example, instead of writing the property expression as follows:

∀t.!(grant1(t) & grant2(t))

(which states that for all values of time t, grant1 and grant2 are mutually exclusive), we write the property in a temporal language such as PSL (which implicitly describes time) as follows:

always !(grant1 & grant2)

(which states that grant1 and grant2 never hold or evaluate to true at the same time).

Linear-Time Temporal Logic: Propositional temporal logic is currently the most widely used specification formalism for reactive and concurrent systems. More specifically, lineartime temporal logic (for example, LTL [7]), has emerged as the preferred foundational semantics for many of today’s fledgling assertion-property language standards (including PSL). A linear-time temporal logic strength is that it lets us reason about expected behavior over a linear sequence of states. This form of specification is intuitive to design engineers, since the specification thought process can view the progression of time similar to a simulation trace. For example, using the PSL linear-time temporal operators, we can express the AMBA™ AHB [8] property a transfer of type IDLE cannot be followed by types SEQ or BUSY as follows:

assert always (HTRANS==`IDLE) -> next ((HTRANS!=`SEQ) && (HTRANS!=`BUSY));

Given the temporal formulas f, f1, and f2; a few common linear-time temporal operator examples include:

• !f                         — f does not hold
• f1 & f2                — f1 and f2 both hold
• f1 | f2                  — f1 or f2 or both hold
• f1 -> f2               — f1 implies f2
• f1 <-> f2             — f1 -> f2 and f2 -> f1
• always f               — f holds in every cycle
• never f                 — f does not hold in any cycle
• next f                   — f holds in the next cycle
• f1 until f2             — f1 holds until f2 holds
• f1 before f2         — f1 holds before f2 holds
• eventually! f         — f1 holds in some future cycle
  

Not all properties we are interested in can be expressed directly using linear-time temporal logic operators. For example, it is not possible to directly express a property that involves modulo n counting, such as: p is asserted in every even cycle.

Extended Regular Expressions: Extended regular expressions overcome some of the limitations in linear-time temporal logic’s expressibility. They are a convenient way to define a temporal pattern that can match (or more aptly put, specify) sequences of states. Regular expressions let us describe design behavior that involves counting, such as modulo n type behavior, with the * operator. Hence, regular expressions let us specify properties that cannot be described directly using linear-time temporal operators, such as p is asserted in every even cycle.

Sequences of Boolean conditions that occur at successive clock cycles can be described succinctly using extended regular expressions. The advancement of time in a sequence is described by the ## operator in SVA (or “;” in PSL). For example, the SVA extended regular expression:

a ##1 b ##4 c ##[2:3] d

describes a set of sequences in which a occurs, followed one cycle later by b, followed four cycles later by c, followed between two or three cycles later by d. Obviously, this regular expression would match two unique sequences:

a→b→true→true→true→c→true→d

or

a→b→true→true→true→c→true→true→d

where the arrow in this example illustrates a clock tick (that is, an advancement in time).

Both PSL and SVA support a form of extended regular expressions. Both support various repetition operators ( [ ] ) that concisely describe repeated concatenation of either a Boolean expression or other sequences. For example, given the Boolean expression b and sequence s, we can write:

• s[* n] —a sequence of n contiguous occurrences of s
• b[= n] —any sequence containing n occurrences of b
• b[-> n] —any sequence ending in the nth occurrence of b

The single constant n can be replaced by the repeat range m:n (for example, [*2:3]). PSL and SVA also support the following repetition operators:

• s[*] —a sequence of zero to infinity contiguous occurrences of s
• s[+] —a sequence of one to infinity contiguous occurrences of s

Sequences can be composed with conjunctive operators, as well as the time advancement operators. For example, given the sequences s1 and s2, in SVA we can create a new sequence by combining them as s1 ## s2, where the sequence s2 would start the clock immediately after s1.

To provide a real example, we could specify the following AMBA AHB forbidden sequence: when the master is not performing a burst type of INCR, then a transfer of type BUSY cannot be followed by NSEQ, which can be coded in SVA as follows:

Even though regular expressions are a powerful way of describing sequences, they have their limitations; that is, not all properties can be expressed directly using extended regular expressions. For example, the property eventually p holds forever, cannot be directly expressed using extended regular expressions. However, it can be expressed using linear-time temporal logic constructs, for example, eventually always p. Thus, linear-time temporal logic constructs address some of the limitations of extended regular expressions. Likewise, extended regular expressions complement linear-time temporal logic constructs.

1.2. Elements of High-Level Requirements Models

Although today’s assertion languages, which combine lineartemporal logic with extended regular expressions, are expressive, there are still many IP-related properties that cannot be directly expressed using this combination. For these properties, we can use a technique that combines lineartime temporal logic constructs, extended regular expressions, and modeling. For example, creating a complete specification for a PCI Express IP bridge requires specifying data integrity properties such as a packet entering from the data link layer could never be dropped, duplicated or corrupted as i t progresses out to the physical layer [9]. Any property involving transaction ordering or queuing semantics requires storing information from various paths of data, which are then used during future data integrity checks. Hence, this type of specification often requires additional modeling to store the transaction information. Note that this process is similar to creating a scoreboard in a simulation testbench. By combining additional modeling with an assertion language, we can specify complex higher-level requirements that would not be possible by using only an assertion language’s temporal constructs combined with extended regular expressions.

There are other instances when additional modeling combined with an assertion language simplifies the process of creating verification IP. For example, for some interfaces, such as the Intel PC SDRAM, the textual specification provides a command truth table that defines interface behavior. This form of defining behavior generally lists conceptual states of the interface, followed by valid commands (allowed with the current conceptual state) and the resulting new conceptual states due to the valid commands (that is, the conceptual state transitions). Although extended regular expressions allow us to describe behavior in terms of sequences, attempting to describe behaviors that involve deep sequences that can further split into multiple sequences (describing alternate paths) can become unmanageable and result in less-thanobvious specifications. Since one of the goals of specification is to define behavior to eliminate ambiguities, specifications that are not clear are not desirable—nor easily maintainable. Hence, there are many instances where modeling aspects of the requirement both clarify and simplify the specification process.

4. RULES FOR ASSERTION-BASED SPECIFICATION

Although research shows there is little doubt that an ABV methodology is beneficial, early adopters have been forced to take a learn-as-you-go approach to implementation. To address the need for guidelines in this emerging field, this section, based on the experiences of early adopters and power users, lists a set of rules for effectively coding assertion-based specifications.

Rule 1: Create a checklist of requirements prior to coding an assertion-based specification.

An ad-hoc approach to assertion-based IP specification is likely to yield an incomplete, contradictory, and generally poor-quality specification. Follow the process outlined in the Section 5 to ensure a high-quality complete specification.

Rule 2: Express all properties in an IP assertion-based specification in a manner that is clear, concise, and obvious.

When reading the formal assertion-based specification, if the design intent is not obvious, then it is highly likely that formal specification is wrong (or incomplete). Even if the specification is correct and complete, a complex assertionbased specification is not maintainable.

Do not be adamant about the specification style. For example, attempting to specify properties solely with temporal logic or regular expressions is not possible. Use all means available. Strive for simplicity.

Guideline: Partition large, complex properties into a set of simpler properties.

Guideline: Partition large, complex sequences (specified using regular expressions) into a simpler set of sequence declarations.

Rule 3: Use an FSM model to describe conceptual states defined in the architecture.

NOTE: The behavior described in conceptual state-machines should be intuitive. Once described, a simple assertion can then be specified over states contained in the conceptual state-machine with respect to the IP design.

Guideline: When the conceptual state-machine becomes too large, try partitioning the FSM into a smaller set of FSMs. The partition should be driven by the properties we want to express. It is acceptable to describe overlapping behavior in the partitioned set of conceptual state-machines since our goal is to provide just enough modeling to simplify assertion specification.

Rule 4: For converging datapaths, specify the output behavior of a port with respect to a unique input path

For example, in Figure 1, to specify the correct behavior of port C with respect to its inputs, it is better to create a set of assertions. Create one assertion to describe the expected behavior of port C with respect to a specific data item on port A (allowing port B to assume any valid value that is not checked by the assertion). Then, create another assertion to describe the expected behavior of port C with respect to a specific data item on port B (again allowing port A to assume any valid value that is not checked by the assertion).

5. FORMALIZING THE VIP PROCESS

One of the most challenging problems when creating assertion-based verification IP is answering the questions: Have I written enough properties? Is my property set complete? This problem is not limited to an assertion-based specification. In fact, this is an inherent verification problem. For example, a similar question is often asked concerning the comprehensiveness of the simulation testbench; that is: Have I written enough checks in the testbench? Is my simulation environment complete? Coverage metrics do not help us solve this problem since coverage measures the quality of the input stimulus and answers the questions: Are we missing a set of vectors required to reach a particular state in the design (or stimulate a line of code)?

Although current research in the area of determining the completeness of the property set exists, its focus is on identifying structures in the implementation that are not covered by an assertion (that is, hole analysis)[11][12][13]. These approaches still fail to answer the question, “Is the property set complete?” With the lack of automated means to solve this inherent verification problem, we must depend on a systematic process to ensure high-quality verification IP. This section presents a set of steps that are useful as a process for creating assertion-based verification IP.

Step 1: Identify the target verification approach

Your first step in developing verification IP is to identify blocks for formal verification and blocks for simulation.

Counter to the popularity of Myth 5, a single form of specification is not necessarily ideally efficient or effective for all verification processes. For example, it is generally more efficient in formal verification to specify a property on the output of a block with respect to a single input path through the block than to account for all input paths at once. When there are multiple input paths, it is recommended that you write multiple properties describing each path (input to output) separately.

The following discussion should help you decide which blocks are ideally suited for formal verification and which blocks are not.

Blocks suitable for formal verification: Formal verification is particularly effective for control logic and data transport blocks containing high concurrency, as illustrated in Figure 1.

Figure 1. Concurrent paths

The following list includes examples of blocks ideally suited for formal verification:

• Arbiters of many different kinds
• On-chip bus bridge
• Power management unit
• DMA controller
• Host bus interface unit
• Scheduler, implementing multiple virtual channels for QoS
• Clock disable unit (for mobile applications)
• Interrupt controller
• Memory controller
• Token generator
• Credit manager block
• Standard interface (for example, PCI Express)
• Proprietary interfaces

An example of a bug identified using formal verification on a block involving concurrent paths is as follows:

During the first three cycles of a transaction start from one side of the interface, a second transaction start unexpectedly came in on the other side of the interface and changed the configuration register.

Blocks not suitable for formal verification: In contrast, design blocks that generally do not lend themselves to formal verification tend to be sequential in nature (that is, a singlestream of data) and potentially involve some type of data transformation (see Figure 2).

Figure 2. Sequential paths

Examples of designs that perform mathematical functions or involve some type of data transformation include:

• Floating point unit
• Graphics shading unit
• Convolution unit in a DSP chip
• MPEG decoder

An example of a bug associated with this class of design includes the following: partition

The IFFT result is incorrect if both inputs are negative.

Step 2: Describe IP behavior

The second step in creating a developing verification IP is to briefly describe the behavior of the block to be verified. The importance of this step cannot be understated. Without clearly articulating what it is you are planning to verify, your assertion-based specification will be hopelessly incomplete. By describing and illustrating the intended behavior, you focus on what is to be verified. In fact, in many cases, errors in the design are identified through the thought process that occurs during this step—prior to any form of verification [3].

This description does not have to be long or wordy. On the contrary, it can consist entirely of a set of block diagrams and interface waveforms that illustrate the expected end-to-end behavior accompanied by a brief description. It is, however, critical that you take this step prior to creating your assertionbased specification to ensure completeness.

Step 3: Define the interface for assertion-based specification

The third step is to identify the IP block’s interface signals that must be monitored. Create a table that lists the signal names and their functionality. This list of signals will form your assertion-based specification (for example, high-level requirements module) interface. In addition to identifying the requirement's interface signals, this step also describes any special considerations in the cycle timing relationships between the various interface signals that must be checked.

Step 4: Create a requirements checklist

The fourth step is to create a requirements checklist, which is the list of requirements you plan to formally verify. We suggest that you create a table that lists the specific assertion name that you will code in your high-level requirements model (or verification IP) as shown in Figure 3, along with a description in English of what the requirement checks. In a separate table, list all required assumptions.

Figure 3. Assertion-based requirements model

When creating an assertion-based specification checklist, focus on what you want to verify versus how you plan to verify the design. This focus contrasts sharply with a traditional simulation-based testplan, which normally describes both what you want to verify (in terms of checks) and how you plan to verify the design (focusing on input sequences or scenarios as stimulus) [14].

Often, you can derive the requirements checklist directly from an existing natural languages specification, such as a microarchitectural specification, a vendor’s specification (for example, the Intel PC SDRAM), or an industry protocol standard (for example, PCI). However, for some blocks (particularly a company’s internal proprietary IP) there might not be (unfortunately) a clear specification. Hence, in those cases, you start the process of creating the requirements checklist in terms of the design's outputs, not in terms of its inputs. Then, you should think about end-to-end requirements versus internal structural or implementation requirements or assertions.

Step 5: Formalize the requirements

Using the interface signals identified in Step 3, and the set of requirements identified in Step 4, create your assertion-based specification. Encapsulate the set formalized requirements into a high-level requirements model that will monitor the IP’s input and output signals, as shown in Figure 3.

When creating your high-level requirements model concurrently during the design implementation phase (as opposed to prior to implementation), do the following:

• Ask yourself: Which high-level requirement from the requirements checklist should I specify first?
• Specify the ones that capture the essence of what the block is supposed to do from the micro-architecture perspective.
• Specify the ones related to the most complete RTL functionality.

Step 6: Document verification strategy

In this step, you will define the verification plan and proof strategy. For example, you might choose to prove certain requirements by initially applying a set of restrictions (that is, add constraints to restrict the explored behavior to only read-mode transaction, or only write-mode transactions). This approach lets you focus the verification on specific modes of operation, and simplifies the verification process. Once the various modes function correctly, the restrictions are removed and the IP is verified under all modes of operation.

In addition, this step lists any verification strategies you might choose to apply during the verification process, such as abstraction or symmetry for formal verification.

Step 7: Define coverage goals

The final step in formalizing the VIP process is to define a set of coverage goals that must be met during the verification process. For example, to ensure that you are verifying what you think you are verifying, check that constraints on specific states in your requirements model have not over-constrained the states. The checking procedure varies depending on your verification process. For example, in formal verification, you can check to see if specific states in your requirement model are reachable. For simulation-based approaches, you can apply functional coverage to various states or sequences of states in the requirements model.

6. CONCLUSIONS

This paper explored a number of myths that have accompanied the growing interest in assertion-based specification for IP compliance and interoperability verification. In particular, this paper highlights the misuse of assertion languages during the specification process. This is predominately due to the lack of good guidelines on how to effectively code an assertion-based specification. Hence, the main contribution of this paper is the process we present as a systematic set of steps we have found useful in developing assertion-based verification IP.

7. REFERENCES

[1] Accellera Property Specification Language (PSL) LRM v1.1, June 2004.

[2] Accellera SystemVerilog LRM v3.1a, March 2004.

[3] H. Foster, A. Krolnik, D. Lacey. Assertion-Based Design, Kluwer Academic Press, 2003.

[4] H. Foster, C. Coelho, “Assertions Targeting A Diverse Set of Verification Tools”, Proc. Intn’l HDL Conference, March, 2001.

[5] S. Smith. “Synergy between Open Verification Library and Specman Elite”, Proceedings of Club Verification: Verisity Users’ Group Meeting, 2002.

[6] Abarbanel, I. Beer, L. Gluhovsky, S. Keidar, Y. Wolfsthal, “FoCs--Automatic Generation of Simulation Checkers from Formal Specifications”, Proc. Computer Aided Verification, 12th International Conference, CAV 2000, pp. 414-427, July 15-19, 2000.

[7] A. Pnueli, “The Temporal Logic of Programs”. Proc. of 18th IEEE Symposium on Foundations of Computer Science, 1977: 46-57.

[8] AMBATM Specification, Revision 2.0, ARM Limited, 1999.

[9] L. Loh, H. Wong-Toi, C.N. Ip, H. Foster, D. Perry. “Overcoming the Verification Hurdle for PCI Express”, DesignCon 2004.

[10] S. Katz, D. Geist, and O. Grumberg. “Have I written enough properties?”, in 10th CHARME, LNCS 1703, pp. 280–297, 1999.

[11] Yatin Hoskote, Timothy Kam, Pei-Hsin Ho, Xudong Zhao, ”Coverage Estimation for Symbolic Model Checking”, in DAC99.

[12] H. Chockler, O. Kupferman, R.P. Kurshan, and M.Y. Vardi, "A practical approach to coverage in model checking", In Proc. 13th CAV, LNCS 2102, pp. 66–78, 2001.

[13] H. Foster, C. N. Ip, D. Perry, H. Wong-Toi, Formal verification of block-level requirements., DesignCon 2004.

¹ This paper does not propose to present a comprehensive overview of PSL or SVA. The goal is to present fundamental elements of these languages.