English
Case Study: Annotating OVL 2.0 with SVA Assertions
Long Jianga, Talukdar Bipula, Seawright Andrew, Viswanathan Vibarajana & Larsen Kennethb
Mentor Graphics Corporation
Abstract:
In this case study we attempt to annotate a subset of OVL 2.0 checkers using equivalent SVA properties. In doing so, we define the equivalence between checkers, or assertions, based on what input sequences they can detect as failure sequences. A methodology using a commercial formal tool is employed to compute such a relationship and is utilized to validate the correctness of the annotation. Experiences and lessons-learned during the experiments are presented at the end of the paper.
INTRODUCTION
The new Accellera Open Verification Library (OVL) [2][3] standard provides a vendor and language independent assertion library that can be used across multiple verification processes; such as traditional simulation, dynamic-formal, and static-formal verification tools. SystemVerilog Assertions (SVA), part of the IEEE Std. 1800-2005 SystemVerilog Standard [1], is a general assertion language for specifying temporal behavior of the design and is supported by many EDA vendors’ design and verification tool flows. OVL is widely applicable because it is easy to use and its open source code allows users to understand the underlying semantics when necessary. On the other hand, the expressiveness of SVA as a temporal language enables succinct descriptions of temporal behavior, and existing assertion compilation algorithms generate efficient checker logic for use with formal verification. Thus it is no surprise that users choose between OVL and SVA based on their own knowledge and past experience, rather than the attributes of the languages.
However, because OVL definitions are implicit in implementation details, and documentation through waveforms or natural languages yields inaccurate definitions for more complex assertions, there exists a problematic ambiguity with OVL semantics. Moreover, in order to apply formal verification efficiently, choosing the appropriate OVL instantiation using different parameter settings is crucial toward minimizing the complexity of a successful application of formal tools. Unfortunately, these subtle characteristics are not well known and are obscured by the underlying implementation of each OVL assertion.
The contribution of this paper is to provide OVL users with a guideline for using OVL in real-world design situations by annotating a representative subset of the OVL assertions with its equivalent SVA assertions. In doing so, the implementation overhead of different OVL assertions are compared with their counterpart SVA descriptions, in terms of checker logic size. We demonstrate our results through a methodology that checks the equivalence between OVL and SVA assertions in terms of their contextual usage; in other words, as target assertions, coverage monitors, or assumptions based on formal techniques.
This paper contains five sections. First, we provide an overview of assertions, assertion languages, and assertion libraries. Second, we briefly summarize the usage of OVL in design and verification—namely in property verification and coverage monitoring—and the difference in the requirements of these two applications. Third, OVL is categorized to illustrate the underlying implementation details, which are mainly through auxiliary state machine modeling, with or without counters. Fourth, characteristics and relationships between similar OVL assertions are discussed, defining equivalence and redundancy relationships between assertions with regard to coverage and property checking. Their differences are also discussed. In the fifth section, the equivalent SVA description is exemplified for the OVL assert_window family of assertions, illustrating that SVA can be used as an accurate and succinct specification for OVL semantics.
PRELIMINARIES
This section reviews assertions, assertion libraries, and assertion languages for use in hardware verification.
ASSERTION-BASED VERIFICATION
The use of assertions is very valuable in verification. An assertion is a verifiable statement of design intent that allows the finding of bugs closer to their source. They are used to fortify interfaces, improve communication between design and verification engineers, enable better coverage measurements, and allow the mainstream use of formal techniques for functional verification.
Assertion-based verification (ABV) is the use of assertions throughout the design and verification flow to improve quality and shorten time to market. In terms of IP, assertions are even more valuable to ensure that components and interfaces are used and reused properly. Assertions are often used to increase design confidence in such areas as interfacing, corner-case behavior, and integration, as well as ensuring that critical structures obey their specification.
The ABV methodology attempts to address the challenges of observability and controllability of a system. The two challenges are mathematical duals. Observability is a measure of how well internal states of a system can be inferred by knowledge of its external outputs. Controllability denotes the ability to move a system around within its entire configuration space using only certain admissible manipulations.
Generally, in verification assertions help solve the observability challenge by providing an internal testing point, but assertions by themselves do not help with controllability. However, by adopting assertion-based, constraint-driven simulation, or by applying formal property checking techniques to the design assertions, we are able to address the controllability challenge. By including coverage measurements with the assertions, the verification process provides valuable insights by uncovering holes in the input stimuli and identifying missing scenarios.
Assertions can be specified in a variety of ways and at different levels of abstraction. For example, an assertion can be specified in a property language, through a checker module, or in the form of a directive. Standardized assertion languages, such as SVA and the Property Specification Language (PSL) [4], and standardized assertions libraries, such as OVL, have been available for a few years.
There are tradeoffs to consider when choosing the type of assertions and the methodology to use. It is useful to compare using an assertion language versus an assertion library component for coding any particular assertion. Assertion languages allow the description of customized properties. The benefits are abstract and powerful pattern matching and temporal behavior checking. Assertion languages are often very concise for specific properties. The downsides of using an assertion language directly are: the language must be learned, mistakes in specifying the properties must be avoided, and complex checking may require additional modeling code.
Assertion libraries are pre-verified checker IP. They are drop in solutions for the most common checks. Designers may be more comfortable using checker modules than assertion languages. There are two downsides of assertion libraries: if the exact checking requirements don’t match the available components, the components have a lot of parameters that need to be understood for proper application; a checker module is sometimes not as transparent as an assertion language.
Assertion library checkers can be implemented in a variety of ways. For example, checkers can be implemented using assertion languages, RTL modeling code, or a mixture of both.
Figure 1 illustrates some different approaches to using assertion checkers.
Figure 1. Assertion/checker methodologies
Figure 1a shows the use of SVA to directly check design signals. Figure 1b shows the use of an assertion checker that includes SVA code internally. Figure 1c shows the use of an assertion checker which is implemented using some modeling code and SVA. The method of 1a is the most transparent and can be very concise for specific properties. The method of 1c might be best for very complex checking, such as protocol checking for PCI Express.
Because of these choices and methodologies it is often the case that one would want to compare one assertion to another. This paper focuses on this topic in more detail in sections 4 and 5.
OVL
The OVL is composed of a set of assertion checkers that verifies specific properties of a design (refer to Table 1 for complete list of the 50 OVL checkers). These checkers are instantiated in the design to guarantee that a particular condition holds true. Each checker includes one or more properties, a coverage measure, a severity control, and reporting features.
After its ratification as an Accellera industry standard in August 2005, the OVL has grown in user adoption. With the recent release of OVL Version 2.0, which supports simulation, formal verification, emulation/acceleration, and synthesis, the OVL is a truly open, unifying methodology.
SVA and SVA Synthesis
SVA is part of SystemVerilog [1]. In SVA, temporal properties are created in layers. Boolean propositions form the lowest layer. Verilog expressions are used to define the Boolean propositions. Certain special functions are used frequently to form the propositions: $rose(), $fell(), $stable(), $onehot(), $prev(). These simplify the specification of signal changes, characteristics, and delayed values.
SVA sequences are created from Boolean expressions using the SVA sequence operators. Sequence operators are similar to an extended, regular expression language. SVA has operators for concatenation and cycle delay using ## notation, various types of sequence repetition, sequence or, sequence and, and the specification that a proposition be true throughout another sequence.
Properties are defined using SVA sequences. The most common forms of properties use the powerful sequence implication operators |-> and |=> to define properties from operand sequences.
Finally, assertions, constraints, and coverage points are defined from SVA properties in the form of the SVA verification statements assume, assert, and cover.
Table 1. OVL classification
SVA assertions can be simulated in dynamic simulation. SVA can also be used to check design properties in formal verification [6]. For formal verification, SVA is usually synthesized into logic that a formal verification tool can operate on, and the design logic and the assertions are compiled into a formal model of the system for verification. SVA assertions can be used in formal as target properties; these are the properties to check. SVA can also be used to define design and interface assumptions; these assumptions are also called constraints.
In this paper, we will restrict our focus to safety property checking. Safety properties are assertions that detect bad states of the system. Failure of these properties can be presented in the form of a waveform trace from the initial state (typically reset) to the state where the property fails.
The synthesis of an SVA safety property involves the compilation of the temporal assertion into an equivalent logic circuit, which monitors the respective design signals used by the assertion and detects the failure states by asserting a failure signal that is observed by the tools.
Generally, to get the best results, performance, and capacity when using formal verification, it is desirable for the formal tool to compile the design and assertion logic into as compact a logic representation as possible.
Since assertion coding styles vary and methodologies to specify assertions differ it is useful to understand their complexity when synthesized and how they compare in terms of logic size.
Categorizing OVL 2.0
OVL 2.0 contains implementations in four different languages; namely, Verilog, SVA, PSL, and VHDL. OVL 2.0 has the original 33 components in Verilog and PSL, 50 (originally 33 plus 17 new) components in SVA, and 10 (a subset of 10 from the original 33) components in VHDL. For research and pure SVA annotation, this paper picks up a subset of the original 33 components from the SVA version of OVL 2.0.
The OVL contains five different classes of assertions; namely, combinatorial, 1-cycle, 2-cycle, N-cycle, and event-bound (refer to Table 1. for complete listing of the OVL components and their classes). Because N-cycle and event bound assertions are the trickiest ones to model in pure SVA, this paper chooses a maximum of such components for research. The paper advocates a methodology for writing equivalent assertions using formal verification. Using this same methodology, it also presents analysis for a dozen OVL components.
The paper excludes studies of X/Z checking and coverage-driven verification that can be done by the OVL 2.0 components. The objective of the experiments was to concentrate on the main assertions in the components that were considered.
Design Decisions behind OVL Implementation
Keeping the coverage and X/Z checking implementations aside, the design of a specific OVL component in the SVA version of the library depends upon the class of the component.
Being the simplest ones to model, all single cycle and combinatorial components are implemented using pure SVA. No auxiliary modeling code—for example, ovl_always and ovl_proposition—was needed or used As such, the library contains only two combinatorial components: ovl_proposition and ovl_assert_never_unknown_async. No single cycle or combinatorial components are chosen for analysis in this paper. All 2-cycle components—for example assert_always_on_edge and assert_decrement—are also based on pure SVA implementation. Hence, no such components are chosen for analysis in this paper.
Design of most of the N-cycle and event bound components in the library uses auxiliary, Verilog modeling state machines and counters. These state machines and counters—for example, assert_frame, assert_next, assert_win_change, and assert_window—are employed to model windows and maintain the counting of elapsed cycles over a multi-cycle path. This paper annotates these classes of OVL components using pure SVA, thereby avoiding use of auxiliary Verilog state machines or counters to achieve the same functionality.
OVL Implementation
The implementation of most of the N-cycle and event bound assertions in the OVL uses auxiliary, Verilog modeling code based on counters and state shifting.
Taking an example of an N-cycle OVL component, ovl_change, the implementation uses two states, START and CHECK, to encode the state of the active component. The state diagram is shown in Figure 2.
Figure 2. State diagram for ovl_change
Auxiliary logic is necessary to model functionality that ignores new start events while checking is already in progress after an earlier start event. The design is such that checking can happen only within the allowed window. The window is modeled per the above state machine. The window opens after the start event is true and the state of the machine is START. This implementation is applied to components that require IGNORE_NEW_START functionality. An ERROR-ON-NEW-START functionality implementation also makes use of this window. However, such functionality can be modeled using pure SVA without the help of a Verilog state machine. The experiments in this paper will demonstrate this. The OVL components, ovl_unchange, ovl_win_change, ovl_win_unchange, ovl_frame, and ovl_time have similar implementations.
OVL components, such as ovl_next, employ decrementing counters to define the window within which the checking logic of the component is active. The counter is used to maintain the current elapsed cycles once a checking window opens. The overlap check restricts re-occurrence of start event within the checking window, as follows:
start_event |-> count <= 1
This means that a new start event can occur only when the previously opened window is closing or already closed. However, such functionality can be modeled using pure SVA without the help of an auxiliary Verilog counter that has been modeled separately. The experiments will demonstrate this as well.
The OVL Window Concept
Every OVL assertion has various options that are configurable through parameters. Parameters, such as severity_level, property_type, coverage_level, and msg, are common for all components in the OVL. Similarly, function-specific parameters, such as action_on_new_start, are common for OVL subset assertions such as assert_frame and assert_change.
These assertions use the concept of a window of active clock edges within which the checking of the test expression, test_expr, occurs. The window opens with the assertion of start_event. It either closes with the assertion of end_event in some of the checkers or automatically closes after a specified number of clocks (num_cks) in another set of checkers. These checkers have the following operating modes:
It is important to note that, depending on the type of checker, the clock edge where the window starts or closes is either included within the window or excluded out of the window. If included, the checking of test_expr would also happen on those clock edges.
In most cases, test_expr checking is excluded at the clock edge at which a window opens, and the checking is included at the clock edge where a window closes. However, this feature varies across the window-based family of checkers in the OVL.
For example, in the ovl_unchange checker, by default the clock edge at which the window closes is included within the window. However, when a window is reset upon the arrival of a new start_event (with the OVL_RESET_ON_NEW_START1 option enabled), at this clock edge, the checking of test_expr is disabled where the old window closes, and a new window opens.
These are the sweet spots for annotating the OVL assertions into complete SVA.
Figure 3. Window-based OVL checker implementation
Methodology for Comparing Assertions
To compare two different assertions (checkers) that are coded to achieve a similar checking requirement, a methodology for comparing them is required. In this work we focus on a methodology for comparing checkers based on the failure sequences they detect over finite traces. For example, in a simulation, one checker may detect a failure that is ignored by another implementation.
To compare assertions formally, a miter circuit could be created, as is commonly done in equivalence checking. This miter circuit is constructed from the synthesized implementation of the assertions or checkers to be compared. However, often no such tool is available because the compiled failure signals are not readily available for construction of a miter circuit.
To achieve a similar comparison to a miter circuit, we employed an assert/assume methodology that is readily supported by most formal tools. In this assert/assume method, one assertion is used as the assumption or constraint for the other, which is set up as the target assertion to be proven or falsified. Formal verification is performed to check all possible assertion traces. Then, the assertion and assumption roles of the two checks are reversed and the verification is repeated.
In each cycle of the trace, the checker may detect a failure based on the sequence seen up to that point. Abstractly, what a particular checker checks can be visualized as a space that covers all possible sequences. The failures detected by the checker form a subset of this space. Comparing two checkers is equivalent to comparing two failure subsets.
Consider the different possible situations shown in Figure 4.
Figure 4. Relationship between two assertions
In the first situation, P1 and P2 both detect failures that the other does not. Only some of the failures are detected by both P1 and P2. Using the assert/assume method, both P1 and P2 would be falsified when one is the assumption and the other is the target assertion and vice versa. In this case, both checkers need to be examined to determine if the failures are correct and why there are differences.
In the second and third situations, one checker finds all the failures of the other, plus more. The assert/assume method proves one assertion, but when the reverse (assert/assume switched) is run, the other assertion is falsified. These checkers are not the same, as one checks more cases than the other, and these results need to be inspected to see why.
In the fourth situation, when P1 and P2 are exactly equivalent, whether the assert/assume methodology runs P1 as an assumption and P2 as the assertion or vice versa, the formal verification will find a proof that the assertions are the same. In this case, it is certain that both implementations are in fact checking the same failure sequences. However, it is still possible that both implementations have a common bug if they do not meet the intended high-level checking requirements.
SVA Annotation of the assert_window Family of Assertions
Case Study: ovl_frame
In OVL, ovl_frame is one of the window-based checkers. The window is started at start_event and controlled by two parameters: min_cks and max_cks. According to the OVL LRM, the test expression test_expr should not hold in the min_cks of the window, and it should hold at least once before the window closes in max_cks cycles. In the following sections, we rewrite the checker with different configurations using equivalent SVA.
The experimental result is valid in the chosen, specific and typical, parameter setting. A stronger and general proof of the equivalent for all boundary conditions is not presented.
ERROR_ON_NEW_START
The first thing we noticed was that the start_event in this checker is edge-sensitive; in other words, $rose(start_event) is the triggering condition for the start of the window, and subsequent checking for NEW_START is also based on $rose(start_event).
RESET_ON_NEW_START
The OVL-SVA version of the library seems to have some problems with this configuration. Instead, we used the OVL-PSL version of the library for the equivalence comparison. The following shows the equivalent SVA assertion for the OVL-PSL implementation of this checker. Note that the RESET only affects the cycle between min_cks and max_cks, as $rose(start_event) is associated with the later part of the LHS sequence.
IGNORE_ON_NEW_START
For this configuration, it turns out to be very difficult for SVA to model, because the start and end of the window implicitly defined in the OVL checker are very hard to model using SVA. On the other hand, a simple Verilog modeling state-machine can model this window behavior in a straightforward way; thus, using SVA and the state-machine seems to be the best way to model such a property. Hence, a pure SVA annotation is not constructed for this property.
Summary of Results
The complete results are shown in Figure 5. The third column shows the results of our experiments, whether the equivalent SVA property for the corresponding OVL checker with a specific parameter are obtained or not. For these 12 window-based OVL checkers, equivalent SVA descriptions are available except for the ones with the configuration of IGNORE_NEW_START.
Figure 5. Annotation results
During this process, the OVL semantics are better understood, and a few issues have been found with the SVA and PSL implementation of the checker with regard to its conformance with the LRM. As there are many OVL flavors being implemented because of their ease-of-use and easy integration with various HDL flavors, a systematic way to validate their correctness and conformance with the LRM turns out to be important to ensure the semantics of the checker itself. The methodology of comparing the equivalence between two assertions provides a easy way of writing and debugging the conformance between various OVL implementations. Issues from this study will be submitted to the OVL committee for further study.
Conclusion and Future Work
In this case study, we presented our work annotating the OVL 2.0 with SVA descriptions in order to create a concise and accurate semantic definition, and we explored a different methodology for implementing an assertion library. For an efficient implementation of the widely used OVL, a methodology of employing assertion languages as well as judiciously using auxiliary modeling produces the most efficient implementation. The practice of using SVA to annotate OVL checker semantics along with using a formal tool for equivalence checking should be applied on any OVL implementation with other language flavors.
ACKNOWLEDGMENT
We would to like thank Todd Burkholder for proofreading and editing of the original abstract and the draft of this paper.
REFERENCES
[1] IEEE Std 1800-2005 SystemVerilog Language Standard, IEEE 2005
[2] Foster, H., Larsen, K., Turpin, Mike. Introduction to the new Accellera Open Verification Library. DVCon 2007
[3] Accellera Open Verification Library Standard, Accellera 2007.
[4] IEEE Std 1850-2005 IEEE Standard for Property Specification Language (PSL).
[5] Turpin, M. Timing Diagrams for Accellera Standard OVL V2.1. September, 2007.
[6] Long, J., Seawright, A. Synthesizing SVA Local Variables for Formal Verification. IEEE 44th Design Automation Conference, San Diego, July 2007.
Mentor Graphics Corporation
Abstract:
In this case study we attempt to annotate a subset of OVL 2.0 checkers using equivalent SVA properties. In doing so, we define the equivalence between checkers, or assertions, based on what input sequences they can detect as failure sequences. A methodology using a commercial formal tool is employed to compute such a relationship and is utilized to validate the correctness of the annotation. Experiences and lessons-learned during the experiments are presented at the end of the paper.
INTRODUCTION
The new Accellera Open Verification Library (OVL) [2][3] standard provides a vendor and language independent assertion library that can be used across multiple verification processes; such as traditional simulation, dynamic-formal, and static-formal verification tools. SystemVerilog Assertions (SVA), part of the IEEE Std. 1800-2005 SystemVerilog Standard [1], is a general assertion language for specifying temporal behavior of the design and is supported by many EDA vendors’ design and verification tool flows. OVL is widely applicable because it is easy to use and its open source code allows users to understand the underlying semantics when necessary. On the other hand, the expressiveness of SVA as a temporal language enables succinct descriptions of temporal behavior, and existing assertion compilation algorithms generate efficient checker logic for use with formal verification. Thus it is no surprise that users choose between OVL and SVA based on their own knowledge and past experience, rather than the attributes of the languages.
However, because OVL definitions are implicit in implementation details, and documentation through waveforms or natural languages yields inaccurate definitions for more complex assertions, there exists a problematic ambiguity with OVL semantics. Moreover, in order to apply formal verification efficiently, choosing the appropriate OVL instantiation using different parameter settings is crucial toward minimizing the complexity of a successful application of formal tools. Unfortunately, these subtle characteristics are not well known and are obscured by the underlying implementation of each OVL assertion.
The contribution of this paper is to provide OVL users with a guideline for using OVL in real-world design situations by annotating a representative subset of the OVL assertions with its equivalent SVA assertions. In doing so, the implementation overhead of different OVL assertions are compared with their counterpart SVA descriptions, in terms of checker logic size. We demonstrate our results through a methodology that checks the equivalence between OVL and SVA assertions in terms of their contextual usage; in other words, as target assertions, coverage monitors, or assumptions based on formal techniques.
This paper contains five sections. First, we provide an overview of assertions, assertion languages, and assertion libraries. Second, we briefly summarize the usage of OVL in design and verification—namely in property verification and coverage monitoring—and the difference in the requirements of these two applications. Third, OVL is categorized to illustrate the underlying implementation details, which are mainly through auxiliary state machine modeling, with or without counters. Fourth, characteristics and relationships between similar OVL assertions are discussed, defining equivalence and redundancy relationships between assertions with regard to coverage and property checking. Their differences are also discussed. In the fifth section, the equivalent SVA description is exemplified for the OVL assert_window family of assertions, illustrating that SVA can be used as an accurate and succinct specification for OVL semantics.
PRELIMINARIES
This section reviews assertions, assertion libraries, and assertion languages for use in hardware verification.
ASSERTION-BASED VERIFICATION
The use of assertions is very valuable in verification. An assertion is a verifiable statement of design intent that allows the finding of bugs closer to their source. They are used to fortify interfaces, improve communication between design and verification engineers, enable better coverage measurements, and allow the mainstream use of formal techniques for functional verification.
Assertion-based verification (ABV) is the use of assertions throughout the design and verification flow to improve quality and shorten time to market. In terms of IP, assertions are even more valuable to ensure that components and interfaces are used and reused properly. Assertions are often used to increase design confidence in such areas as interfacing, corner-case behavior, and integration, as well as ensuring that critical structures obey their specification.
The ABV methodology attempts to address the challenges of observability and controllability of a system. The two challenges are mathematical duals. Observability is a measure of how well internal states of a system can be inferred by knowledge of its external outputs. Controllability denotes the ability to move a system around within its entire configuration space using only certain admissible manipulations.
Generally, in verification assertions help solve the observability challenge by providing an internal testing point, but assertions by themselves do not help with controllability. However, by adopting assertion-based, constraint-driven simulation, or by applying formal property checking techniques to the design assertions, we are able to address the controllability challenge. By including coverage measurements with the assertions, the verification process provides valuable insights by uncovering holes in the input stimuli and identifying missing scenarios.
Assertions can be specified in a variety of ways and at different levels of abstraction. For example, an assertion can be specified in a property language, through a checker module, or in the form of a directive. Standardized assertion languages, such as SVA and the Property Specification Language (PSL) [4], and standardized assertions libraries, such as OVL, have been available for a few years.
There are tradeoffs to consider when choosing the type of assertions and the methodology to use. It is useful to compare using an assertion language versus an assertion library component for coding any particular assertion. Assertion languages allow the description of customized properties. The benefits are abstract and powerful pattern matching and temporal behavior checking. Assertion languages are often very concise for specific properties. The downsides of using an assertion language directly are: the language must be learned, mistakes in specifying the properties must be avoided, and complex checking may require additional modeling code.
Assertion libraries are pre-verified checker IP. They are drop in solutions for the most common checks. Designers may be more comfortable using checker modules than assertion languages. There are two downsides of assertion libraries: if the exact checking requirements don’t match the available components, the components have a lot of parameters that need to be understood for proper application; a checker module is sometimes not as transparent as an assertion language.
Assertion library checkers can be implemented in a variety of ways. For example, checkers can be implemented using assertion languages, RTL modeling code, or a mixture of both.
Figure 1 illustrates some different approaches to using assertion checkers.
Figure 1. Assertion/checker methodologies
Figure 1a shows the use of SVA to directly check design signals. Figure 1b shows the use of an assertion checker that includes SVA code internally. Figure 1c shows the use of an assertion checker which is implemented using some modeling code and SVA. The method of 1a is the most transparent and can be very concise for specific properties. The method of 1c might be best for very complex checking, such as protocol checking for PCI Express.
Because of these choices and methodologies it is often the case that one would want to compare one assertion to another. This paper focuses on this topic in more detail in sections 4 and 5.
OVL
The OVL is composed of a set of assertion checkers that verifies specific properties of a design (refer to Table 1 for complete list of the 50 OVL checkers). These checkers are instantiated in the design to guarantee that a particular condition holds true. Each checker includes one or more properties, a coverage measure, a severity control, and reporting features.
After its ratification as an Accellera industry standard in August 2005, the OVL has grown in user adoption. With the recent release of OVL Version 2.0, which supports simulation, formal verification, emulation/acceleration, and synthesis, the OVL is a truly open, unifying methodology.
SVA and SVA Synthesis
SVA is part of SystemVerilog [1]. In SVA, temporal properties are created in layers. Boolean propositions form the lowest layer. Verilog expressions are used to define the Boolean propositions. Certain special functions are used frequently to form the propositions: $rose(), $fell(), $stable(), $onehot(), $prev(). These simplify the specification of signal changes, characteristics, and delayed values.
SVA sequences are created from Boolean expressions using the SVA sequence operators. Sequence operators are similar to an extended, regular expression language. SVA has operators for concatenation and cycle delay using ## notation, various types of sequence repetition, sequence or, sequence and, and the specification that a proposition be true throughout another sequence.
Properties are defined using SVA sequences. The most common forms of properties use the powerful sequence implication operators |-> and |=> to define properties from operand sequences.
Finally, assertions, constraints, and coverage points are defined from SVA properties in the form of the SVA verification statements assume, assert, and cover.
Table 1. OVL classification
SVA assertions can be simulated in dynamic simulation. SVA can also be used to check design properties in formal verification [6]. For formal verification, SVA is usually synthesized into logic that a formal verification tool can operate on, and the design logic and the assertions are compiled into a formal model of the system for verification. SVA assertions can be used in formal as target properties; these are the properties to check. SVA can also be used to define design and interface assumptions; these assumptions are also called constraints.
In this paper, we will restrict our focus to safety property checking. Safety properties are assertions that detect bad states of the system. Failure of these properties can be presented in the form of a waveform trace from the initial state (typically reset) to the state where the property fails.
The synthesis of an SVA safety property involves the compilation of the temporal assertion into an equivalent logic circuit, which monitors the respective design signals used by the assertion and detects the failure states by asserting a failure signal that is observed by the tools.
Generally, to get the best results, performance, and capacity when using formal verification, it is desirable for the formal tool to compile the design and assertion logic into as compact a logic representation as possible.
Since assertion coding styles vary and methodologies to specify assertions differ it is useful to understand their complexity when synthesized and how they compare in terms of logic size.
Categorizing OVL 2.0
OVL 2.0 contains implementations in four different languages; namely, Verilog, SVA, PSL, and VHDL. OVL 2.0 has the original 33 components in Verilog and PSL, 50 (originally 33 plus 17 new) components in SVA, and 10 (a subset of 10 from the original 33) components in VHDL. For research and pure SVA annotation, this paper picks up a subset of the original 33 components from the SVA version of OVL 2.0.
The OVL contains five different classes of assertions; namely, combinatorial, 1-cycle, 2-cycle, N-cycle, and event-bound (refer to Table 1. for complete listing of the OVL components and their classes). Because N-cycle and event bound assertions are the trickiest ones to model in pure SVA, this paper chooses a maximum of such components for research. The paper advocates a methodology for writing equivalent assertions using formal verification. Using this same methodology, it also presents analysis for a dozen OVL components.
The paper excludes studies of X/Z checking and coverage-driven verification that can be done by the OVL 2.0 components. The objective of the experiments was to concentrate on the main assertions in the components that were considered.
Design Decisions behind OVL Implementation
Keeping the coverage and X/Z checking implementations aside, the design of a specific OVL component in the SVA version of the library depends upon the class of the component.
Being the simplest ones to model, all single cycle and combinatorial components are implemented using pure SVA. No auxiliary modeling code—for example, ovl_always and ovl_proposition—was needed or used As such, the library contains only two combinatorial components: ovl_proposition and ovl_assert_never_unknown_async. No single cycle or combinatorial components are chosen for analysis in this paper. All 2-cycle components—for example assert_always_on_edge and assert_decrement—are also based on pure SVA implementation. Hence, no such components are chosen for analysis in this paper.
Design of most of the N-cycle and event bound components in the library uses auxiliary, Verilog modeling state machines and counters. These state machines and counters—for example, assert_frame, assert_next, assert_win_change, and assert_window—are employed to model windows and maintain the counting of elapsed cycles over a multi-cycle path. This paper annotates these classes of OVL components using pure SVA, thereby avoiding use of auxiliary Verilog state machines or counters to achieve the same functionality.
OVL Implementation
The implementation of most of the N-cycle and event bound assertions in the OVL uses auxiliary, Verilog modeling code based on counters and state shifting.
Taking an example of an N-cycle OVL component, ovl_change, the implementation uses two states, START and CHECK, to encode the state of the active component. The state diagram is shown in Figure 2.
Figure 2. State diagram for ovl_change
Auxiliary logic is necessary to model functionality that ignores new start events while checking is already in progress after an earlier start event. The design is such that checking can happen only within the allowed window. The window is modeled per the above state machine. The window opens after the start event is true and the state of the machine is START. This implementation is applied to components that require IGNORE_NEW_START functionality. An ERROR-ON-NEW-START functionality implementation also makes use of this window. However, such functionality can be modeled using pure SVA without the help of a Verilog state machine. The experiments in this paper will demonstrate this. The OVL components, ovl_unchange, ovl_win_change, ovl_win_unchange, ovl_frame, and ovl_time have similar implementations.
OVL components, such as ovl_next, employ decrementing counters to define the window within which the checking logic of the component is active. The counter is used to maintain the current elapsed cycles once a checking window opens. The overlap check restricts re-occurrence of start event within the checking window, as follows:
start_event |-> count <= 1
This means that a new start event can occur only when the previously opened window is closing or already closed. However, such functionality can be modeled using pure SVA without the help of an auxiliary Verilog counter that has been modeled separately. The experiments will demonstrate this as well.
The OVL Window Concept
Every OVL assertion has various options that are configurable through parameters. Parameters, such as severity_level, property_type, coverage_level, and msg, are common for all components in the OVL. Similarly, function-specific parameters, such as action_on_new_start, are common for OVL subset assertions such as assert_frame and assert_change.
These assertions use the concept of a window of active clock edges within which the checking of the test expression, test_expr, occurs. The window opens with the assertion of start_event. It either closes with the assertion of end_event in some of the checkers or automatically closes after a specified number of clocks (num_cks) in another set of checkers. These checkers have the following operating modes:
- OVL_IGNORE_NEW_START — Once a window opens, the subsequent stat_event will be discarded until the current window closes.
- OVL_RESET_ON_NEW_START 1 — For every new start_event, the old window will be reset and a new window will open (if there is one already open; otherwise, only a new window open).
- OVL_ERROR_ON_NEW_START 2 — When a window is already open and in progress, if there is a new start_event, it will be discarded and an assertion error will be generated; otherwise, a new window opens.
It is important to note that, depending on the type of checker, the clock edge where the window starts or closes is either included within the window or excluded out of the window. If included, the checking of test_expr would also happen on those clock edges.
In most cases, test_expr checking is excluded at the clock edge at which a window opens, and the checking is included at the clock edge where a window closes. However, this feature varies across the window-based family of checkers in the OVL.
For example, in the ovl_unchange checker, by default the clock edge at which the window closes is included within the window. However, when a window is reset upon the arrival of a new start_event (with the OVL_RESET_ON_NEW_START1 option enabled), at this clock edge, the checking of test_expr is disabled where the old window closes, and a new window opens.
These are the sweet spots for annotating the OVL assertions into complete SVA.
Figure 3. Window-based OVL checker implementation
Methodology for Comparing Assertions
To compare two different assertions (checkers) that are coded to achieve a similar checking requirement, a methodology for comparing them is required. In this work we focus on a methodology for comparing checkers based on the failure sequences they detect over finite traces. For example, in a simulation, one checker may detect a failure that is ignored by another implementation.
To compare assertions formally, a miter circuit could be created, as is commonly done in equivalence checking. This miter circuit is constructed from the synthesized implementation of the assertions or checkers to be compared. However, often no such tool is available because the compiled failure signals are not readily available for construction of a miter circuit.
To achieve a similar comparison to a miter circuit, we employed an assert/assume methodology that is readily supported by most formal tools. In this assert/assume method, one assertion is used as the assumption or constraint for the other, which is set up as the target assertion to be proven or falsified. Formal verification is performed to check all possible assertion traces. Then, the assertion and assumption roles of the two checks are reversed and the verification is repeated.
In each cycle of the trace, the checker may detect a failure based on the sequence seen up to that point. Abstractly, what a particular checker checks can be visualized as a space that covers all possible sequences. The failures detected by the checker form a subset of this space. Comparing two checkers is equivalent to comparing two failure subsets.
Consider the different possible situations shown in Figure 4.
Figure 4. Relationship between two assertions
In the first situation, P1 and P2 both detect failures that the other does not. Only some of the failures are detected by both P1 and P2. Using the assert/assume method, both P1 and P2 would be falsified when one is the assumption and the other is the target assertion and vice versa. In this case, both checkers need to be examined to determine if the failures are correct and why there are differences.
In the second and third situations, one checker finds all the failures of the other, plus more. The assert/assume method proves one assertion, but when the reverse (assert/assume switched) is run, the other assertion is falsified. These checkers are not the same, as one checks more cases than the other, and these results need to be inspected to see why.
In the fourth situation, when P1 and P2 are exactly equivalent, whether the assert/assume methodology runs P1 as an assumption and P2 as the assertion or vice versa, the formal verification will find a proof that the assertions are the same. In this case, it is certain that both implementations are in fact checking the same failure sequences. However, it is still possible that both implementations have a common bug if they do not meet the intended high-level checking requirements.
SVA Annotation of the assert_window Family of Assertions
Case Study: ovl_frame
In OVL, ovl_frame is one of the window-based checkers. The window is started at start_event and controlled by two parameters: min_cks and max_cks. According to the OVL LRM, the test expression test_expr should not hold in the min_cks of the window, and it should hold at least once before the window closes in max_cks cycles. In the following sections, we rewrite the checker with different configurations using equivalent SVA.
The experimental result is valid in the chosen, specific and typical, parameter setting. A stronger and general proof of the equivalent for all boundary conditions is not presented.
ERROR_ON_NEW_START
The first thing we noticed was that the start_event in this checker is edge-sensitive; in other words, $rose(start_event) is the triggering condition for the start of the window, and subsequent checking for NEW_START is also based on $rose(start_event).
RESET_ON_NEW_START
The OVL-SVA version of the library seems to have some problems with this configuration. Instead, we used the OVL-PSL version of the library for the equivalence comparison. The following shows the equivalent SVA assertion for the OVL-PSL implementation of this checker. Note that the RESET only affects the cycle between min_cks and max_cks, as $rose(start_event) is associated with the later part of the LHS sequence.
IGNORE_ON_NEW_START
For this configuration, it turns out to be very difficult for SVA to model, because the start and end of the window implicitly defined in the OVL checker are very hard to model using SVA. On the other hand, a simple Verilog modeling state-machine can model this window behavior in a straightforward way; thus, using SVA and the state-machine seems to be the best way to model such a property. Hence, a pure SVA annotation is not constructed for this property.
Summary of Results
The complete results are shown in Figure 5. The third column shows the results of our experiments, whether the equivalent SVA property for the corresponding OVL checker with a specific parameter are obtained or not. For these 12 window-based OVL checkers, equivalent SVA descriptions are available except for the ones with the configuration of IGNORE_NEW_START.
Figure 5. Annotation results
During this process, the OVL semantics are better understood, and a few issues have been found with the SVA and PSL implementation of the checker with regard to its conformance with the LRM. As there are many OVL flavors being implemented because of their ease-of-use and easy integration with various HDL flavors, a systematic way to validate their correctness and conformance with the LRM turns out to be important to ensure the semantics of the checker itself. The methodology of comparing the equivalence between two assertions provides a easy way of writing and debugging the conformance between various OVL implementations. Issues from this study will be submitted to the OVL committee for further study.
Conclusion and Future Work
In this case study, we presented our work annotating the OVL 2.0 with SVA descriptions in order to create a concise and accurate semantic definition, and we explored a different methodology for implementing an assertion library. For an efficient implementation of the widely used OVL, a methodology of employing assertion languages as well as judiciously using auxiliary modeling produces the most efficient implementation. The practice of using SVA to annotate OVL checker semantics along with using a formal tool for equivalence checking should be applied on any OVL implementation with other language flavors.
ACKNOWLEDGMENT
We would to like thank Todd Burkholder for proofreading and editing of the original abstract and the draft of this paper.
REFERENCES
[1] IEEE Std 1800-2005 SystemVerilog Language Standard, IEEE 2005
[2] Foster, H., Larsen, K., Turpin, Mike. Introduction to the new Accellera Open Verification Library. DVCon 2007
[3] Accellera Open Verification Library Standard, Accellera 2007.
[4] IEEE Std 1850-2005 IEEE Standard for Property Specification Language (PSL).
[5] Turpin, M. Timing Diagrams for Accellera Standard OVL V2.1. September, 2007.
[6] Long, J., Seawright, A. Synthesizing SVA Local Variables for Formal Verification. IEEE 44th Design Automation Conference, San Diego, July 2007.
|
||||||
