Implementation of a SystemC Assertion Library

Wolfgang Ecker - Infineon Technologies AG
Volkan Esen, Thomas Steininger, Michael Velten - Infineon Technologies AG, Darmstadt University of Technology
Jacob Smit - University of Southampton

Abstract

Implementing advanced temporal assertions in SystemC is an error prone process due to the limited assertion capabilities of the class library. Current approaches focus on linking assertion languages such as PSL or SVA to SystemC code to overcome this restriction. However, linking other languages to SystemC to overcome some language deficiencies contradicts the purely object oriented class library approach, which was used for creating SystemC. Therefore we propose a native SystemC assertion library which is designed in a similar fashion to the OVL, in order to enable assertion based verification especially for system level designs and IP-integration verification in SystemC. Each assertion is implemented as a generic, fully parameterisable SystemC module for easy integration into any system design. It is our aim to provide each assertion implementation with a consistent structure containing the same parameters. Furthermore using SystemC as the implementation language for this library is compliant to the OSCI provided compiler simulator architectures and thus follows the open concept of SystemC.

I. INTRODUCTION

SystemC gains more and more momentum in the systemlevel domain. Abstraction layers such as cycle callable (CC), programmers view with timing (PVT) and pure programmers view (PV) reflect the main domains of its usage. Assertion based verification (ABV) has already proven to enhance design quality and verification time tremendously in the RT-level domain where HDLs are applied. It is obvious that the introduction of ABV to SystemC would provide the same benefits to system-level design on a CC-level. This is especially true for IP-integration and SoC assembly as due to their complex nature they require advanced assertions which are beyond SystemC's limited assertion capabilities.

With regard to the development of ABV for RTL designs the first steps were taken by implementing assertion libraries, as, for example, described in [1]. Applying ABV to SystemC would involve the usage of an assertion language such as PSL or SVA and proprietary simulators. Since proprietary solutions contradict the open concept of OSCI-SystemC we implement an assertion library in SystemC similar to the OVL and compatible to OSCI. Each assertion is implemented as a generic, fully parameterisable SystemC module for easy integration into any system design. It is our aim to provide each assertion implementation with a consistent structure containing the same set of parameters. Thus no additional proprietary software tools will be required to benefit from a library based approach as already shown with the OVL [2].

In contrast to the current implementation of the Verilog and VHDL version of the OVL we propose a wider set of parameters including for instance X-check activations or alternatives for the reset modeling and more.

The provided assertions cover a wide range of checks such as Boolean checks (e.g. one-hot), transitional checks (e.g. over/underflow), and multi-cycle checks (e.g. handshakes). The latter can be run in five different modes with regard to a reoccurrence of an asserted enabling condition before check termination. These include the three modes known from the OVL, where a reoccurrence leads to either a restart or a continuation of the check, whereas the latter case can be configured to issue an additional warning.

Our approach also provides two pipelined modes, where parallel threads of the same check can be terminated with one occurrence of a true check condition (this is the underlying semantics of SVAs) or where each check in the pipe is terminated one by one, i.e., the fulfilling condition is mapped unambiguously against the corresponding enabling condition. See later sections for details.

This paper is structured as follows: after discussing work relating to our topic we clarify some prerequisites, which are important for introducing the implementation of our library including checker classifications, checker structure, interfaces and execution modes. We close by giving a short conclusion and overview of further work still to be done.

II. RELATED WORK

For most common HDLs assertion libraries both proprietary and free have been introduced over the last years such as the OVL [2], and CheckerWare [3]. Furthermore assertion languages like OVA [4], PSL [5], and SVA [6] have been introduced to allow the specification of more specialized properties. Some approaches have been published to cope with assertions in the field of SystemC which allows more and more possibilities in system-level design as described in [7].

In [8], [9], and [10] approaches are shown which let PSL and SVA assertions interact with SystemC. In contrast to that we designed a checker library which is written in native SystemC and thus does not rely on a specific property language. The idea of integrating a property language to SystemC is taken a step further, by an assertion class library as presented in [8]. Since this implementation works with proprietary tools only it contradicts the open concept of OSCI-SystemC. Furthermore our library offers a pipelined execution mode which can only be realized with a huge effort using SVA.

Steps are also being taken towards formal model checking of SystemC models as shown in [11] and [12]. Since these approaches work on the basis of clocks as synchronization events they are most applicable to CC-models.

Further approaches focus on time abstractions and obtain a graph-based view of transactions in order to raise the abstraction level for system-level verification as presented in [13] and [14].

III. DEFINITIONS

In this section we introduce some definitions, which will form the prerequisites of our further descriptions.

• A property is an abstract description of a desired design behavior.

• An assertion is an abstract directive for checking a corresponding property. It is not part of the implementation language and should not be confused with an assert statement.

• An assert statement is a language dependant directive to simulation tools to check the condition to be observed.

• A checker / monitor is a module which contains the implementation of one or more assertions. Finite state machines (FSMs) are used to describe a property with native language objects. The branches which are reached when the property is not fulfilled contain assert statements which fire everytime when being processed.

• An implication consists of a left and right-hand side condition which are correlated to each other using a boolean implication. The left-hand side condition is referred to as the antecedent expression or enabling condition. The right-hand side condition is referred to as the consequent expression or fulfilling condition.

In this example the antecedent expression A implies the consequent expression B.

In contrast to boolean implications we also use temporal implications which add a further time requirement which has to be met in order for the implication to hold.

IV. SYSTEMC ASSERTION LIBRARY

Our SystemC assertion library is organized in modules and fully compatible to the OSCI SystemC standard. This implies that it is completely independent from third party tools apart the OSCI SystemC. All checker modules are fully parameterisable for an easy integration into any system design. The different checkers have a consistent structure and all of them provide the same parameters. The assertion library exists for bit and sc_logic signal types. The sc_logic library supports X-checks with a parameterisable severity level. Table I gives an overview about the checkers we implemented in our SystemC assertion library so far.

One Hot	Req Ack Restart
Zero One Hot	Req Ack No-Restart
One Cold	Req Ack Error-On-Restart
Out of Range	Req Ack Overlap
Valid Opcode Pattern	Req Ack Pipe
Gray Code	Sequence Implication
Past Value	Future Value
Forbidden Sequence

TABLE I: IMPLEMENTED ASSERTIONS

A. Checker classifications

1) Boolean (one cycle) checkers: Boolean checkers observe properties which span a time window of exactly one clock cycle. They monitor the validity of one or more boolean expressions on the given input signals at a specific clock edge. All common boolean operators can be used to set up a boolean expression as a property to be asserted. If a condition fails the violated assertion fires with the given severity level and reports the specified message. The simulation time is printed to the output to provide easy debugging of the design under test. An example for a boolean checker is the onehot check, which asserts a high value on exactly one bit of a bit vector. The X-check in sc_logic modules is a boolean check as well, which monitors all signals for a presence of an X-value prior to starting the actual checking algorithm.

2) Temporal (transitional/multi-cycle) checkers: Temporal checkers incorporate assertions which check temporal relations between boolean expressions, i.e., properties which span time windows. Time windows greater than one clock cycle require handling of current, previous or future values of signals. Hence it is necessary to implement various storage elements to preserve previous values of signals. Implementation of transitional checks, i.e., checks that monitor transitions from one cycle to the next, can be achieved using variables to store previous values of signals. In monitors like e.g. the gray-code checker, the gray-code property is evaluated using the current signal value and comparing it to the previous value stored in a corresponding variable. Properties which span bigger time windows become more complicated with regard to their implementation. Besides storing previous values it is necessary to additionally store temporal information which correlates to the stored values and monitored conditions.
A handshake checker (i.e., Req Ack checker as listed in table I) is an example of assertions monitoring properties with temporal implications. Such an implication could be: "A request implies the occurrence of an acknowledge within three to five clock cycles later!" For implementing such assertions a mechanism of setting, shifting and erasing flags in a FIFO is used, which is explained in more detail later.

B. Monitor structure

The checker modules are implemented in a similar fashion as the OVL checkers. The monitor modules are fully parameterisable and can be connected to any design by simple module instantiations and port maps. During the simulation signals of the design are passed into the assertion module (see Fig. 1). Each SystemC module contains only one thread  which handles the assertion.

Fig. 1. Monitor diagram

First the system behavior, like reset type and clock edge, is set up using generic parameters. After that the assertion mechanism starts using current signal values to solve boolean conditions. In the case of temporal checkers signal values have to be stored and FIFOs need to be parsed (see Fig. 2). For reporting violated properties SystemC assert macros SC_REPORT_INFO, SC_REPORT_WARNING, SC_REPORT_ERROR, SC_REPORT_FATAL are used.

Fig. 2. Basic monitor structure

C. Generic parameters

1) Overview: Generic parameters of the assertion modules are an important topic to keep the checker fully parameterisable. The generics enable the connection of the assertion module to any system design without the need of modifying the source code of the checker if the reset level or the active clock edge has to be changed. Therefore generics can be passed into the modules at elaboration time. A list of the available generic parameters is given in table II.

Signal Type	Required Properties
signal	width
clock	rising edge, falling edge
reset	active low, active high
	sync, async, none
enable	active high, active low
Severity level	info, warning, error, fatal

TABLE II: GENERIC PARAMETERS

Each assertion module has the same generic interface to ensure a consistent structure. The information passed through generic values into the checker module is used to customize the checker to a certain extent. The severity level of the assertion is set using generic values as well. In case of the sc_logic library e.g. the X-check behavior with an independent severity level can be customized with our generic mechanism as well.

2) Implementation: Generic parameters are implemented by templating the checker modules using C++ templates. Another possibility would be using preprocessor directives. However, this leads to a too complex and hard to maintain code architecture and makes the process of developing further checkers error prone. Additionally templates also provide stricter type checking to avoid mistakes during the set up phase of the assertion behavior. To enable generic values in SystemC we include an assertion header file in each checker module. This header file contains declarations of enumeration types e.g. for the clock edge and reset behavior. A template for the width of a bitvector and the function for the X-check is defined in the assertion header file. Listing 1 shows the source code of the header file. Each enumeration type accepts only the defined values. In case of an illegal generic value setting the compiler will bail out with an error.

Listing 1. ASSERTION HEADER

At the beginning of each checker module the templates are declared using the enumeration types of the assertion header file. The generic values are stored in the m_* variables. These variables are used in the SystemC module to set the system behavior. The source code of the template declaration is shown in listing 2.

Listing 2. TEMPLATE DECLARATION

The templates are initialized in the main C++ file. There the checker module is instantiated passing the generic values in. Listing 3 shows an example source code where constants are initialized and are used when instantiating the checker module. This is the place where the generic values are changed to provide a customized checker to fit into the surrounding system.

Listing 3. TESTBENCH GENERIC PASSING

D. Execution Modes for Multi-Cycle Checkers

1) Overview: We implemented five different execution modes for multi-cycle checkers. i.e. the properties being checked span time windows greater than two. Such a property would be for example: "A request implies an acknowledge within 3 to 5 cycles!" Such properties are ambiguous with regard to multiple occurrences of the enabling condition when the time windows overlap. Therefore it is necessary to define five execution modes which differ with regard to this special issue. Table III gives an overview of the different execution modes. 

restart	Every occurrence of the enabling condition restarts the check. Any running check is aborted.
no-restart	Any further occurrence of the enabling condition while a check is currently running is ignored.
error-on-restart	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 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.

TABLE III: EXECUTION MODES

Figures 3 and 4 show the execution modes with the example that a request implies an acknowledge. The range can be specified using generic values for the start and the endtime of a temporal implication. Most interesting is the pipe mode shown in figure 4. It allows checking pipelined behavior of a system design. In this mode it does not take one single acknowledge to satisfy all occurrences of a request. Each acknowledge which occurs responds to the oldest request. The assertion fires if a request has not been answered within the range or an acknowledge has occurred without a request. 

Fig. 3. Execution modes

The temporal execution semantics of SVA and PSL are similar to the overlap mode and thus result in a big overhead when it comes to specify pipelined behavior. Local variables have to be used to tag enabling and fulfilling conditions for determining exact matches, which is a very error prone process.

Fig. 4. Pipe execution mode

2) Implementation: The implementation of the different execution modes in SystemC is achieved by checking the enabling and fulfilling conditions and performing FIFO operations (see figure 7) to model the temporal behavior. In case of temporal implications a flag is written to the FIFO if the enabling condition has occurred. This flag is shifted across the FIFO every clock cycle. If the fulfilling condition occurs the FIFO is searched for the flag in the corresponding time range and if found the flag is deleted. If the flag reaches the end of the FIFO it shows that the fulfilling condition has not occurred in time and thus the assertion fires. 

Fig. 5. FIFO flag shifting

The implementation of temporal implications and the various execution modes can be accomplished in a very consistent way since all execution modes follow the same pattern. Figure 6 shows the different stages of execution for multi-cycle checkers.

Fig. 6. Multi-cycle checker execution

1. At first a FIFO is declared and initialized. The time window size n requires n+1 FIFO elements.

2. In the second code block the consequent expression is monitored (if ack = 1). If true the FIFO is searched for a corresponding flag signaling the antecedent expression. If a corresponding flag is found it is deleted. In the case that no flag could be found the assertion fires. In the pipe mode the oldest flag and in the overlap mode all flags are cleared. The other execution modes only allow one flag in the FIFO which is cleared on a successful check.

3. Next the antecedent expression is checked (if req = 1). If this condition becomes true the FIFO is searched within the time range for other flags. In case of the pipe and overlap mode a further flag is written to the FIFO. In the restart mode the FIFO will be cleared and the new flag will be put in. The no-restart mode and the error-on-restart mode are handled in a similar way. If another flag is present the new one is ignored or an assertion fires respectively.

4. This block deals with shifting the FIFO content.

5. In the final step the last element of the FIFO is checked for a flag. If a flag has propagated to this position the failure of the assertion is signaled.

V. CONCLUSION AND OUTLOOK

Our library approach allows use of temporal assertions in SystemC in a straight forward way. We demonstrated how to build a SystemC class library which is highly customizable for easy integration of assertions into SystemC designs which are cycle callable. The straight forward and consistent module structure of each monitor can be used by SystemC designers as a starting point to model their own assertions.

We also showed that our library supports execution modes which are hard to handle using assertion description languages such as PSL or SVA.

Fig. 7. FIFO execution mode handling

Further work will include the development of more monitors increasing the applicability of the library. Issues as functional coverage and higher abstraction layers will be targeted as SystemC's main areas of usage focus on the transactional level. Due to the modularity of our checkers we also develop an assertion generator which can be used to generate assertion libraries for all sorts of hardware and system description languages and thus can ease ABV for mixed language SoCs.

REFERENCES

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

[2] Accellera, "Open Verification Library." [Online]. Available: http://www.accellera.org/activities/ovl/

[3] Mentor Graphics, "0-in CheckerWare." [Online]. Available: http://www.mentor.com/products/fv/cdv/checkerware/index.cfm

[4] Synopsys, "Open Vera Assertions." [Online]. Available: http://www.synopsys.com/products/simulation/assertion_based_wp.html

[5] H. Foster, E. Marschner, and Y. Wolfsthal, "IEEE 1850 PSL: The Next Generation." [Online]. Available: http://www.pslsugar.org/papers/ieee1850psl-the next generation.pdf

[6] Accellera, "SystemVerilog LRM." [Online]. Available: http://www.systemverilog.org

[7] G. Martin, "Systemc and the future of design languages: Opportunities for users and research," in 16th Symposium on Integrated Circuits and Systems Design, 2003, pp. 61-62.

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

[9] A. Habibi and S. Tahar, "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.

[10] - - , "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.

[11] R. J. Weiss, J. Ruf, T. Kropf, and W. Rosenstiel, "Efficient and customizable integration of temporal properties into systemc," Lausanne, Switzerland, September 2005.

[12] D. Große and R. Drechsler, "Formal verification of ltl formulas for systemc designs," in International Symposium on Circuits and Systems, vol. 5, May 2003, pp. 245-248.

[13] M. Moy, F. Maraninchi, and L. Maillet-Contoz, "LusSy: A toolbox for the analysis of systems-on-a-chip at the transactional level," in Fifth International Conference on Application of Concurrency to System Design, June 2005.

[14] A. Habibi and S. Tahar, "Assertion and model checking of systemc," in North American SystemC Users Group Meeting, San Diego, California, USA, June 2004.