XML-Based Assertion Generation

Wolfgang Ecker, Volkan Esen, Michael Hull, Thomas Steininger, Michael Velten Infineon Technologies AG, Munich, Germany

Abstract :

Implementing comprehensive assertions traditionally involves writing complicated temporal expressions and properties using an assertion language or hand-coding tests procedurally; this is tedious, time consuming and error prone.

We propose an XML based assertion library generator that generates checkers similar to the Open Verification Library (OVL) [1]. OVL checkers can be generated using our generator in a very regular way in Verilog, VHDL, SystemVerilog, or SystemC.

XML is shown to have good frontend support, data validation through schemas and powerful exibility, making it a good meta language that can be specified using a XML editor in a quite comfortable way. It is our intention to implement each assertion as a generic, fully parameterizable module which can be easily, unintrusively, integrated into any system design. As these modules are generated automatically, they provide a consistency accross varying configurations which can be contrasted to the current status of the OVL.

The generator currently supports specification of good cases and bad cases which are used to generate self tests as well as extensions to the also automatically generated documentation.

I. INTRODUCTION

Assertion Based Verification (ABV) has led to a breakthrough in verification methodology by increasing design insight and improving verification time. A huge variety of different approaches to ABV have been developed, among them assertion libraries and assertion languages. The Accellera committee has put great effort into the definition of standards in order to aid ABV to become widely accepted in the industry. Yet there are still inherent problems to solve with regard to ensuring consistency in verification. An analysis of the Open Verification Library (OVL) for example has revealed severe quality issues, such as bugs and inconsistent featuring of its monitors. The OVL also lacks some important customization capabilities relevant for increasing its applicability, such as multiple clock inputs, clock edge specification and more.

Furthermore, as the OVL is not implemented in either SystemC or in VHDL its usage will result in more targeting costs since mixed language semantics have to be applied.

The use of assertion languages reveals similar problems since for most cases language boundaries have to be crossed. Additionally those languages lack necessary execution semantics which results in complicated and error-prone work-around code.

Considering the trend to perform as much verification as possible at a system level, the question of verification consistency and equivalence when comparing a system level design and its corresponding RTL implementation is raised.

In this paper we present an XML-based assertion generator which produces assertion monitor modules similar to the OVL. For this generator we define an XML schema which allows the description of assertions independent from any particular implementation language. Furthermore, it supports the generation of assertion modules for different abstraction layers. Such a methodology in assertion generation clearly has a number of advantages. Once the algorithms within the generator are shown to be mature, confidence can be placed in the effectiveness of assertions, and time need not be spent writing and debugging handcrafted assertions. Furthermore, coverage tests are also generated automatically, again increasing confidence and quality assurance in the design and improving productivity.

II. RELATED WORK

Several library based concepts have been introduced such as OVL [1] [2] or CheckerWare [3] which are not flexible enough to serve the needs of verification engineers. In contrast to these approaches we enable higher flexibility and quality through code generation. Work [4] [5] [6] [7] has been presented also with regards to the integration of ABV into SystemC based on SVA [8]  or PSL [9] which is similar to our approach. However, since the main domain of PSL and SVA is RT-Level verification, it is harder to extend these languages towards higher levels of abstraction which we intend to do. Furthermore, also the SPIRIT movement indicates that XML will be more and more focused to ease IP interchange and to achieve consistency by code generation.

Figure 1. XML structure overview

III. XML-BASED META LANGUAGE

Current assertion specification languages such as PSL or SVA have been successfully applied in the field of assertion based verification of RTL designs. As system level verification becomes more important with the steady increase of design complexity, it is necessary to lift ABV to higher layers of abstraction. Most prominently, timing within the models is an issue; higher level system descriptions use more abstract mechanisms for synchronisation and do not contain clocks. PSL and SVA use clocks as underlying synchronisation, limiting their applicability to cycle accurate models. The highly flexible nature of XML makes it possible to elegantly resolve this; the modular and extensible character of XML allows a more general and extendable way for specifying multi-abstraction layer assertions. In the following sections we introduce a first approach to an assertion meta-language for the specification of RTL assertions first.

A. XML Assertion Stucture

An XML assertion contains a number of details, e.g., the conditions themselves, the signals involved, circuit properties, and descriptions. These are all stored in subnodes inside the XML file, as shown in Figure 1. To assist the user in the completion of the XML file an XSD schema was created. This schema can be used to validate the document by checking that mandatory fields in the XML have been supplied. It can also be used to ensure that legal values have been given.

1) Message & Description Nodes: These nodes hold the assertion message and description. The message is reported when the assertion fires in the simulation. The description holds general textual information about the assertion. This field is used later on for documentation purposes.

2) Signals & Generics Nodes: The signals to be used for the interface declaration of the assertion are specified in the signals node. Each signal has two attributes: name and kind. Furthermore, each signal needs to have certain attributes defined depending on what kind of signal it is. Therefore each signal node contains a further child node called parameter. The attributes for each signal kind are outlined in Table 1.

If any generic values need to be used when creating

Signal Kind Attribute Values signal sign signed, unsigned width , generic clock edge rising, falling, generic type clocked, selftimed, generic period , generic starttime , generic reset active low, high, generic type sync, async, generic enable active high, low, generic debug —  the conditions of the assertion, they can be entered within the generics node as children. Generics can take three attributes: name, type and value.

Table 1. Signal Attributes

3) Sequences and Properties Nodes: These nodes form the basic building blocks of the assertion mechanism. The sequences node contains the definitions of one or more sequences. As in PSL or SVA sequences correlate boolean expressions to each other over time.

Analog to that the properties node contains the definitions of properties. Properties include the specification of desired behavior.

The children of these two nodes are built up of a tree of operators and operands. Depending on the operator, one or more child nodes may be appended as operands. Another operator node can be used in place of an operand node thus allowing a complex expression to be implemented. A more detailed explanation of the assertion mechanism is given in Section III-C.

4) Asserts Nodes: Assert statements can be specified within the asserts node and represent directives to the simulator to check for the validity of conditions. An assert node has an attribute severity, which specifies the severity level of assert. The values for severity are: info, warning, error, fatal, and generic; the latter value implements the severity level as a generic which has to be passed to the generated assertion.

5) Testbenches: This tag holds the description of good case and bad case patterns which the user can specify in order to perform quality assurance of the designed assertion. A pattern tag has three attributes which describe one signal, its value and the delay to the next pattern. The generator uses these patterns for the generation of a testbench which the user later can run automatically. The results of this process can be reused later on for the generation of a documentation for the assertion. Details on the documentation generation are described in the next chapter.

B. Operators & Layers

Similar to SVA, an XML assertion condition is built up from the following building-blocks, shown in ascending hierarchical order:

• Boolean Expressions
• Sequences
• Properties

Each of these layers is composed of building blocks of the same level, lower levels and particular Operators. Each of these operators is represented as a tree node, with parameters specified as subnodes; an assertion is eventually a tree of operators and operands, of the different layers. An example of how to build up a tree on top of the operators outlined below is given later.

1) Boolean Expressions: The Boolean layer is the lowest level, composed of signals, constants and the following boolean operators:

For any given clock cycle, a boolean expression will be evaluated to either true or false. Momentarily excluding the Future operator, the Boolean layer has no concept of time. Furthermore, this layer encompasses both BitVector and Boolean Expressions, and care must be taken with conversions.

2) Sequences: The Sequence or Temporal layer associates boolean expressions with time, allowing temporal assertions to be modeled. In order to achieve a consistent separation of boolean and sequence layer this level contains one operator for converting a Boolean Expression into a Sequential Expression (using an offset-time), the remaining operators all act on Sequences. However this conversion operator is used as an intermediate operator within the generator, such that the user does not have to specify it. Both the fundemental operations, and also aliases for compound operations are shown, composed from fundemental operations, provided for readability in the XML.

Fundamental:

• And
• Or
• Intersect
• Within
• ConcatenateSequences
• Occurs-AtLeast-N-TimesInWindow

Aliases:

• SequenceAlwaysInWindow
• SequenceAtLeastOnceInWindow
• SequenceNeverInWindow

3) Properties: The Property layer connects several sequences, usually by using implications. The implication operator connects an antecedent sequence and a consequent sequence. Detailed information about the implication modes is outlined later in this chapter.

C. Assertion Construction: Example

Figure 2. Example of an assert construction tree

In order to explain the basic building blocks of an assertion described with our XML meta language, the following example will be used which is written in an SVA like notation:

In this example s1, s2 are sequence nodes, p1 is a property node, and a1 is an assert node. Note that p1 specifies that the antecedent expression s1 implies that three to seven cycles later the consequent expression s1 has to match. The XML-tree that represents the construction of a1 is shown in Figure 2. The time ranges in this example are specified by using the sequence operator SequenceAtLeastOnce. This operator has a start and end time parameter and an operand expression which can be either a boolean operator (syntactic sugar: the generator automatically converts the boolean operator to a sequence) or another subsequence. Its semantic denotes that the operand which is on the left hand side of the operator occurs within the given time range. The time range is relative to the point where the operator is inserted in the tree. Note that fixed delay values are mapped to an SequenceAtLeastOnceinWindow operator where start and endtime are equal to the delay.

The implication does not include a delay in time.

D. Execution Semantics

1) Execution Semantics of Implications: The implication operator from Section III-B.3 is defined for properties only. Since the consequent expression of an implication can take several clock cycles until it matches, it is possible that several matches of the antecedent expression can occur while an implication is being evaluated. The OVL for instance defines three modes which determine the behavior of the checkers on the occurrence of further start events while a check is still running. These modes are the first three of the modes that we implemented.

Considering PSL or SVA the execution semantics allow an overlap of evaluation attempts of one implication. However the occurence of a match of the consequent expression terminates all evaluation attempts which are in the corresponding range.

In addition to that we defined a further mode, which allows a pipelined evaluation of one implication, but the occurence of a match of the consequent expression terminates only the first of all evaluation attempts within the corresponding range.

Overall, we implemented the following modes:

• Restart: Every occurrence of the enabling condition (antecedent) restarts the check. Any running check is aborted.

• NoRestart: Any further occurrence of the enabling condition while a check is currently running is ignored.

• ReportOnRestart: Any further occurrence of the enabling condition while a check is currently running is reported.

• Overlap: Every occurrence of the enabling condition starts a further check. The occurrence of the fulfilling condition (consequenct) satisfies all enabling conditions within the corresponding time window.

• Pipe: Every occurrence of the enabling condition starts a further check. The occurrence of the fulfilling condition satisfies only the oldest occurrence of the enabling condition within the corresponding time window.

A more detailed description of these execution modes can be found in [10]. All modes can be specified as an attribute to the property node, i.e. any property within the properties node can be combined with any of these modes.

2) Execution Semantics of Sequences: The antecedent expression s1 of the example given above is a pattern of a and b, where b occurs 3 to 5 cycles later than a. Since sequences can contain time ranges it is necessary to define execution semantics which determine how a match of a sequences is obtained.

To discuss this further the following example can be considered:

a [1:3] b;

By default this sequence matches three times if a is followed by three times b for three consecutive clock cycles. SVA syntax allows the use of a first match semantics, where the sequence matches on the first occurrence of b. Therefore we also define an attribute to sequence nodes which defines how the sequence should be matched. This attribute also specifies whether the sequence should be matched using an overlap or a pipe semantic similar to the modes specified for the property node.

IV. ASSERTION GENERATOR

The backend to our XML assertion meta language is a generator which produces the assertion monitors for the desired view; these monitors are used in a fashion similar to OVL monitors. The subsequent sections give an overview of the characteristics of the generated code and further potential features enabled by a generatorbased approach, as well as a comparison to other ABV approaches.

A. Output Formats

The generator currently supports output to VHDL, SystemVerilog, and SystemC. A SPIRIT XML interface description is in preparation. The mapping of the XML meta language operators and semantics is achieved by defining internal language templates which is described in more detail later.

In addition to the different output languages, the generator also supports the configuration of the actual data types of the interface signals. Thus it is possible to generate an assertion interface which is compliant with the data type of the target design.

The generator can also be configured to produce either clock-synchronized or self-timed assertions. The latter case is intended as a first step towards higher abstraction layers. Self-timed assertions use initial wait directives as replacement of a reset signal. The clock is substituted by a cyclic wait directive with a given cycle period. Which view is generated can be specified from within the XML-description either as a fixed value, or as a generic parameter. The latter case will result in the generation of both views in one assertion module, with a corresponding generic in its interface. The generation of parameterizable behavior is described in the next section.

B. Parameterization

The parameter set of an assertion is defined in the XML-description. The generator parses all generic parameters and evaluates the types assigned to it. If necessary it generates packages for defining the adequate types and embeds a decoding section within the assertion monitor. Parameterizable assertion alternatives are implemented using compile time directives, depending on the target language capabilities. In case of VHDL and SystemVerilog for instance generate statements are used.

This mechanism allows each assertion to be parameterized with regard to its reset behavior (asynchronous vs. synchronous, active high/low) and clocking (positive vs. negative edge).

The differentiation of clocked and self-timed is implemented in a similar fashion. The parameterization mechanism leads to a consistent structure which is common for all assertions as depicted in Figure 3.

Figure 3. Assertion module structure

C. Consistency

The concept of consistency is carried on by the implementation of the actual assertion logic. Through the language independent specification of assertions, the generator allows a clean and consistent implementation of assertions with regard to both functional implementation and target language utilization.

A concise implementation is achieved by mapping all operators of the XML-meta language to a language independent concept first and then mapping this concept to a language template. Thus, a consistent way of implementing assertions is possible as depicted in Figure 4. This figure shows that implications are implemented using a separate antecedent and consequent evaluation logic and a FIFO logic for implementing its execution mode. Sequences in turn are implemented using cascades of FIFOs, since sequences can contain several time range operators.

Figure 4. Antecedent sequence implies consequent sequence

D. Testbenches, Regression, and Documentation

As already mentioned in chapter III the XML frontend also allows the specification of test patterns in order to automate the validation of a generated assertion. The generator uses this information to generate a complete test environment. This environment consists of a testbench, a clock generator, and the instantiation of the corresponding assertion module. This testbench contains both the good case and the bad case patterns which can be looped. The amount of reiterations of good case and bad case in sum can be specified with a generic parameter. The amount of bad case runs with regard to the total number of iterations can be specified using another generic. This mechanism is also used to perform a regression on the generated assertion for performance analysis. Furthermore, the test environment supports the generation of VCD files which are used for documentation purposes.

The generator also supports an automated documentation of the assertion. The documentation includes interface descriptions which are extracted from the XML in the same way as the actual interface of the generated assertion. Furthermore, the documentation includes waveforms which show good case and bad case behavior. The waveforms are based on the generated VCD Files.

V. RESULTS

In this section we discuss the results of a performance regression of one generated assertion. For comparison reasons we use the assert_change monitor of the SVA-implementation of the OVL [1]. We chose this particular checker because it includes both an implication over time and a past operator within the consequent expression, therefore generating a corresponding checker for all supported target languages. Both monitors were run in the same regression environment. We use the same testbench concept as described in the previous section in order to be able to measure the influence of the ratio of good case and bad case runs. In order to get a more reliable result, we incremented the total number of runs stepwise. We repeated each step three times and calculated the average runtime for each step. One step includes the simulation of several good to bad case ratios. The following language setups and combinations were measured:

• VHDL Testbench with OVL
• VHDL Testbench with generated VHDL checker
• SV Testbench with OVL

SV Testbench with generated SV checker We used the Restart mode for all simulations. The window of the checker was initially set to 5 and later 50 clock cycles.

Figure 5 shows the average performance increase when comparing the performance of the generated checker with the OVL checker. As Figure 5 shows, the generated checker simulates at least 20% faster than the OVL.

Figure 5. Speed adventage of the GEN to the OVL assertion

Besides the performance data it is also important to compare the targeting effort involved when either using an OVL checker or a generated checker.

Linking the OVL with a VHDL environment implies that a mixed language simulation has to be performed since the OVL is not implemented in VHDL anymore. Mixed language simulation can be a reason for slowing down simulation speed. Figure 6 shows the simulation measures when simulating the OVL checker in conjunction with a VHDL environment. The linear increase of all curves indicates that the overall simulation time is partially affected by the assertion report mechanism since the amount of bad cases per run increases the number of calls to the report mechanism. Additionally to that also the window size of the checker can have an effect on the simulation speed since with a growing window size bigger internal data objects have to be processed. The difference between OVL and the generated assertion is that big that even the OVL 100% good case takes up more time than the 100% bad case simulation of the generated assertion.

These results show that by generating assertions using our XML-meta language we do not introduce bad effects on performance. Indeed by generating the target language directly we avoid mixed-language simulations.


Figure 6. Performance comparison of the GEN and OVL assertion (window size = 50)

A. Advantages Compared to the OVL

While setting up the regression mentioned above we encountered several issues with the assert_change monitor in the OVL. A closer look into the OVL checker has revealed an inconsistent reset handling. Parts of the checker are reset synchronously whereas other parts of the checker use an asynchronous reset. Furthermore the reset handling is not parameterizable by the user.

Our assertion generator allows more freedom with regard to the interface and supports the generation of highly generic code, as mentioned earlier. The implementation of the OVL checker also included a bug considering the management of the check window which had to be fixed for our regression.

Using a generator based approach ensures that once the generator algorithms are mature that the generated code is correct-by-generator construction. We also encountered that the OVL has inconsistencies with regard to implementations of equal functionality. This makes the library harder to follow and could also be the source of errors.

In contrast to that the generator has well defined mappings from XML structures into design implementations. Thus similar assertions will also result in similar implementations.

VI. OUTLOOK

Research into automated and prefabricated assertions has yielded some interesting insights, and exposed some of the problems designers currently face. The OVL, whilst in a similar vein to our work, is let down by its immaturity and parameterization limit, furthermore the use of handcrafted assertions suffers from too many drawbacks to make it a viable solution for adequately testing every new model. The ability to automate assertion testing and seamlessly plug tests into new models and check coverage is very advantageous.

We expect to be able to extend the current architecture to support a variety of abstraction levels. The design has purposefully been kept modular to facilitate this. Additionally, our experience of XML has been very positive. The use of a naturally expressible, recursive, flexible data structure which is supported by strong type checking through schemas has been ideal for the assertion generator.

VII. CONCLUSION

Assertion Based Design has shown its strengths, but currently its weaknesses of being either intrusive or time-consuming have prevented it taking a more central role in Design Automation. Currently, available solutions are both immature and insufficient to solve these, however we have shown both of these can be remedied and furthermore, a highly parameterizable, cross platform, unintrusive, XML based assertion generator could eventually become an invaluable EDA tool.

ACKNOWLEDGMENT

This work was developed within the scope of the European funded project SPRINT (IST-2004-027580).

REFERENCES

[1] Accellera, “Open Verification Library Homepage,” http://www.accellera.org/activities/ovl/, 2005.

[2] H. Foster, A. Krolnik, and D. Lacey, Assertion-Based Design. Norwell: Kluwer Academic Publishers, 2003.

[3] Mentor Graphics, “0-in CheckerWare,”.

[4] A. Dahan, D. Geist, L. Gluhovsky, D. Pidan, G. Shapir, Y. Wolfsthal, L. Benalycherif, R. Kamdem, and Y. Lahbib, “Combining system level modeling with assertion based verification,” Sixth International Symposium on Quality of Electronic Design (ISQED’05), March 21 - 23 2005.

[5] A. Habibi and S. Tahar, “Towards an efficient assertion based verification of systemc designs,” in In Proc. of the High Level Design Validation and Test Workshop, Sonoma Valley, California, USA, November 2004, pp. 19–22.

[6] ——, “On the extension of systemc by systemverilog assertions,” in Canadian Conference on Electrical & Computer Engineering, vol. 4, Niagara Falls, Ontario, Canada, May 2004, pp. 1869–1872.

[7] T. Peng and B. Baruah, “Using assertion-based verification classes with systemc verification library,” Synopsys Users Group, Boston, 2003.

[8] IEEE Computer Society, SystemVerilog LRM P1800, http://www.ieee.org.

[9] Accellera, Accellera PSL v1.1 LRM, http://www.eda.org/vfv/docs/PSL-v1.1.pdf.

[10] W. Ecker, V. Esen, J. Smit, T. Steininger, and M. Velten, “IP Library For Temporal SystemC Assertions,” in Forum on Specification & Design Languages (FDL), Darmstadt, Germany, September 2006, pp. 301–308.