Improvements for Constraint Solving in the
                                                                  SystemC Verification Library

     Daniel Große        Rudiger Ebendt¨                                                             Rolf Drechsler

Institute of Computer Science German Aerospace Center Institute of Computer Science University of Bremen Institute of Transport Research University of Bremen 28359 Bremen, Germany 12489 Berlin, Germany 28359 Bremen, Germany grosse@informatik.uni- ruediger.ebendt@dlr.de drechsle@informatik.uni- bremen.de bremen.de

ABSTRACT To reduce the amount of time for the specification of sim- For verification of complex system-on-chip designs often ulation scenarios constraint-based random stimulus genera- constraint-based randomization is used. This allows to sim- tion has been introduced (see e.g. [13]). For the simulation ulate scenarios that may be difficult to generate manually. only those stimulus pattern are generated that satisfy cer- For the system description language SystemC the SystemC tain given constraints. By this, the random stimulus genera- Verification (SCV) Library has been introduced. Besides tion process is controlled. The resulting stimuli allow to test advanced verification features like data introspection and scenarios that may be difficult to generate manually. This transaction recording the SCV library enables constraint- helps to uncover bugs that may otherwise remain undetected based randomization for SystemC models. However, the especially because corner cases are not excluded. SCV library has two disadvantages that restrict their prac- In the context of system description languages, like Sys- tical use: There is no support of bit operators in SCV con- temC, the SystemC Verification (SCV) library [12] has been straints and the SCV constraint solver cannot guarantee a introduced for constraint-based random stimulus generation uniform distribution of the constraint solutions. In this pa- and was used successfully in industrial verification projects per we provide a detailed analysis of these problems and (see e.g. [9, 4]). The SCV library allows for system level present solutions that have been integrated in the library. verification using constrained randomization. However, the Categories and Subject Descriptors: J.6 [Computer- SCV library has two major disadvantages that restrict their aided Engineering]: Computer-aided design (CAD) practical use. On the one hand in the constraints no bit operators are supported. On the other hand the constraint General Terms: Verification solver does not fulfill the important requirement that the Keywords: SystemC, Constraint-based Randomization, constraint solutions must be uniformly distributed. SystemC Verification Library In this paper we analyze these two problems and describe improvements that overcome these limitations. The paper

1. INTRODUCTION is structured as follows. Section 2 starts with an introduc- Today circuit and system design is a very challenging task. tion of SystemC, the SCV library and BDDs, the basic data Due to the increasing usage of circuit and systems in all structure that is used in the SCV to represent constraints. kinds of devices – ranging from cell phones to safety critical Then, in Section 3 the improvements for the SCV library are systems – functional verification has become an important presented. First, new bit operators for SCV constraints are issue. Since complete formal verification methods are only introduced. In the second part we explain how a uniform applicable to medium sized designs, simulation-based tech- distribution across all constraint solutions can be guaran- niques are used most frequently [3, 13]. teed. Finally, the paper is summarized in Section in 4. In directed simulation explicitly specified stimulus pattern 2. PRELIMINARIES are applied over a number of clock cycles to the design in order to stimulate a certain functionality and the response In this section, first SystemC and the SCV library are is compared with the expected result. However, directed described. Next the basic underlying data structure that is simulation only checks single scenarios. Since these scenarios used by the SCV library to represent constraints is briefly have to be generated manually, this is a very time consuming reviewed. and expensive task. 2.1 SystemC In order to overcome this limitation random pattern sim-

ulation is used to generate random stimulus patterns for the As a C++ class library SystemC [11] enables modeling design. E.g. random address and data is computed to verify of systems at different levels of abstraction starting at the communication over a bus. functional level and ending at a cycle-accurate model. The well-known concept of hierarchical descriptions of systems is transferred to SystemC by describing a module as a C++ class. Furthermore, fast simulation is possible at an early Permission to make digital or hard copies of all or part of this work for stage of the design process and hardware/software co-design personal or classroom use is granted without fee provided that copies are can be carried out in the same environment. For details on not made or distributed for profit or commercial advantage and that copies SystemC we refer to [5, 7]. bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific 2.2 SystemC Verification Library permission and/or a fee. GLSVLSI’07, March 11–13, 2007, Stresa-Lago Maggiore, Italy. The first version of the SCV library was introduced in Copyright 2007 ACM 978-1-59593-605-9/07/0003 ...$5.00. December 2002 as an open source class library [12, 8, 6]. It

layers on top of the system description language SystemC 1 and adds tightly integrated verification capabilities to Sys- struct m y c o n s t r a i n t : public temC. In the following the main features of the SCV library 2 s c v c o n s t r a i n t b a s e { s c v s m a r t p t r <s c u i n t <32> > a , b ; are summarized: 3 • Data introspection for SystemC and C++ data types 4 SCV CONSTRAINT CTOR( m y c o n s t r a i n t ) { 5 SCV CONSTRAINT( a ( ) > 100 ) ; – Manipulation of arbitrary data types 6 SCV CONSTRAINT( b ( ) == 0 ) ; 7 } – Manipulation of data objects without compile time 8 } ; information Figure 1: Example constraint • Transaction API – Transaction monitoring and recording 1 struct c o n s t r a i n t : public s c v c o n s t r a i n t b a s e { – Basis for debugging, visualization and coverage 2 s c v s m a r t p t r <s c u i n t <32> > a , b ; 3 • Constraint-based stimulus generation for SystemC and 4 SCV CONSTRAINT CTOR( c o n s t r a i n t ) { C++ 5 SCV CONSTRAINT( a ( ) . r a n g e ( 1 , 3 ) == 5 ) ; – High quality pseudo random generator 6 SCV CONSTRAINT( b ( ) [ 1 0 ] == 1 ) ; 7 } – Integrated constraint solver based on BDDs 8 } ; Since this paper presents improvements for constraint solv- Figure 2: Example constraint with bit operators ing using the SCV library in the following we briefly review the basic underlying data structure used by the constraint 3. IMPROVEMENTS FOR CONSTRAINT solver. SOLVING 2.3 Binary Decision Diagrams After a detailed analysis of the SCV constraint solver two As is well-known a Boolean function f : Bⁿ → B can be disadvantages were found that restrict the practical use. In represented by a Binary Decision Diagram (BDD) which is the following two sections we describe the problems and the a directed acyclic graph where a Shannon decomposition solutions. f = xifₓi=0 + xifₓi=1 (1 ≤ i ≤ n) 3.1 Bit Operators is carried out in each node. Constraint expressions over variables to be randomized A BDD is called ordered if each variable is encountered at can only use the following operators: most once on each path from the root to a terminal node and if the variables are encountered in the same order on • Arithmetic operators: +, -, * all such paths. A BDD is called reduced if it does not con- • Relational operators: ==, !=, >, >=, <, <= tain isomorphic subgraphs nor does it have redundant nodes. Reduced and ordered BDDs are a canonical representation • Logical operators: !, &&, || since for each Boolean function the BDD is uniquely spec- ified [2]. In the following, we refer to reduced and ordered As can be seen there is no support for bit operators in BDDs for brevity as BDDs. the SCV constraint solver. However, bit operators are very important for the verification engineer during the specifica- Example 1. In Figure 3 a BDD for the function f = tion of constraints. Bit operators allow for simpler and more x₁x₂ + x₁x₂x₃ is shown. The BDD is shown using comple- compact formulations of complex constraints. In detail the ment edges [1]. These allow to represent both a function and following bit operators have been implemented: its complement by the same node, modifying the edge point- ing to the node instead. Therefore the BDD only contains 1. Bitwise and: a() & b() the 1-terminal. 2. Bitwise or: a() | b() 2.4 Constraints in the SCV Library 3. Bitwise not: ˜ a() In the SCV library constraints are declared as classes. This allows an object-oriented way to manage constraints 4. Bit-select: a()[i] for constant i using hierarchy and inheritance. In detail a constraint is derived from the scv constraint base class. The data to 5. Slice-select: a().range(x,y) for constant x and y be randomized is specified as scv smart ptr variables. Example 3. In Figure 2 an example constraint that uses Example 2. An example of an SCV constraint is shown bit operators is shown. Note that these kinds of constraints in Figure 1. The name of the constraint is my constraint. can otherwise not be written in such a simple and compact Here, the two unsigned integer variables a and b are random- way. ized. The conditions on the variables a and b are defined by expressions in the SCV CONSTRAINT() macro. For the implementation first in the class scv expression the according operators were overloaded and new member Internally a constraint in the SCV library is represented functions were added. The class scv expression is used for by the corresponding characteristic function, i.e. the func- the internal representation of the constraint expressions in tion is true for all solutions of the constraint. This charac- form of an expression tree. In such a tree leaf nodes are teristic function of a constraint is represented as a BDD. As variables or constants and non-terminal nodes are marked BDD package CUDD [10] is used in the SCV library. with operators.

                    f
                                                              Table 1: Probabilities for solutions
                    x₁                                            x0₁     x1₂          x0₃  probability
                                                                                                25%
x₂      x₂                                                        01     11             11      25%
                                                                                                50%

x₃                                                            and x₂ = 1; the 1-edge of this node as well as the uncomple-
                                                              mented 0-edge point to the 1-terminal.
                                                              In total, the probabilities following the intuitive traversal
                    1                                         algorithm are shown in Table 1.

   Figure 3: BDD for f = x₁x₂ + x₁x₂x₃                            This example demonstrates that the probability for choos-
                                                              ing the 1-edge of the root node should be corrected to 33%
                                                              instead of 50%.     By this a uniform distribution across all

The class scv expr is used to store the BDD representa- solutions is achieved. tion of an scv expression. For the construction of the BDD In the SCV constraint solver a special weighting algo- in this class each bit operator has to be mapped to the ac- rithm is implemented to guarantee the uniform distribution cording BDD synthesis operations. For example in case of of all solutions. In a pre-processing step the BDD of all a “bitwise and“ the resulting bit vector is computed by the initial constraints is traversed and the correct probabilities BDD-AND operation for each bit of the two input vectors. are computed for each node. The basic idea of the recursive Of course there are several special cases like different length weighting algorithm is to compute weights of the else- and of vectors, different data types etc. that have to be taken then-child of a node while taking into account whether nodes into account. have been removed due to BDD reduction rules. Based on 3.2 Uniform Distribution the weights a probability is assigned to each BDD node. Then, for the generation of values – one constraint solution is The uniform distribution of the solutions of constraints picked uniformly distributed across all solutions of the con- is a very important aspect for the quality of a constraint straint – the computed probabilities of the pre-processing solver. However, we observed that the solutions are not step are used during the BDD traversal. always uniformly distributed. This problem occurs in sce- The SCV constraint solver calls the weighting algorithm narios of high practical relevance. If variables are fixed to a only once at the beginning for the initial BDD that repre- certain value for constraint solving, i.e. these variables are sents the constraints. Thus, the SCV constraint solver is disabled for randomization then the solutions computed by not able to handle simplifications like e.g. fixing variables the constraint solver are not uniformly distributed across to a certain value. In this case the BDD that represents the set of all possible solutions. Later we will illustrate the constraints is modified due to the simplification but the this phenomenon by a simple example. Before describing probabilities are not updated. This causes a non-uniform our remedy we explain the constraint solving process of the distribution of the constraint solution. We provide an ex- SCV library in more detail. ample for this observation. For simplicity we only use one The constraint solver works on individual bits when solv- single constraint in the following example. Note that the ing constraints. As explained in Section 2 for a constraint, presented technique is not restricted to this case. An arbi- a BDD representation is computed. The constraint solver trary number of constraints as well as derived constraints generates a solution of a constraint by using the BDD that including the hard/soft constraint mechanism of the SCV represents the constraint. For this purpose the algorithm library are fully supported. After the example we give some starts at the root node and traverses the BDD down to the technical details for solving the problem. 1-terminal. A path starting from the root and ending at the 1-terminal determines the values of the variables along Example 5. Consider the constraint in Figure 4. This the path. These values correspond to a solution of the con- constraint specifies that a + b = c and c is fixed to 99 (see straints since the BDD is the characteristic function of the lines 7 and 8). The distribution shown in Figure 5 was the constraint. One could assume that choosing the 0- or 1- result from running this constraint 100,000 times in the SCV assignment for a Boolean variable with a probability of 50% constraint solver. As can be seen there is a strong bias of guarantees a uniform distribution. However, the following the solutions in the middle part. observation shows that this is not true. As explained above all constraint solutions are paths to the 1-terminal start- One has to overcome several difficulties while correcting ing from the root node. But during the BDD traversal some this behavior. This is due to the design of the SCV library sub-BDDs can have more paths to the 1-terminal than other which divides the functionality of handling the BDD-based sub-BDDs. Thus, if a sub-BDD with fewer paths is selected representation of constraints roughly into two parts, i.e. one this leads to an overweighting of the fewer represented solu- global constraint manager object and the respective con- tions. This is illustrated by the following example. straint objects (one for each constraint specified). On the one hand, it may seem natural to direct all BDD-related Example 4. In Figure 3 the BDD for the function f = tasks via one dedicated constraint manager object (which x₁x₂ + x₁x₂x₃ is shown, where dashed lines are used for is encapsulated in a class called scv constraint manager the 0-assignment and a dot on an edge represents a comple- and creates a CUDD manager object at start). On the other ment edge (i.e. the function below is inverted). If during the hand, a closer inspection unveils serious flaws in the central- BDD traversal of the function the 1-edge of the root node ized design: is choosen there is exactly one path to the 1-terminal. If The SCV constraint manager maintains the number of instead the 0-edge is chosen, the reached sub-BDD has two BDD variables necessary for representing the least recently paths to the 1-terminal: In the non-reduced BDD there is used constraint object. However, this number is reseted a node marked with x₃ that is reached by assigning x₁ = 0 (i.e., “forgotten”) as soon as a new constraint object is cre-

1 struct t r i a n g l e c : public ity/structure of the SCV interfaces (e.g., the possibility of s c v c o n s t r a i n t b a s e { overloading C++ virtual member functions like 2 s c v s m a r t p t r <s c u i n t <7> > a , b ; scv constraint base::next which triggers the next ran- 34 s c v s m a r t p t r <s c u i n t <8> > c ; dom assignment of the constraint variables). In order to 5 SCV CONSTRAINT CTOR( t r i a n g l e c ) { achieve this, it was necessary to give the simplified BDD to 6 SCV CONSTRAINT( a ( ) + b ( ) == c ( ) ) ; the constraint object in several methods of the class 7 c−>d i s a b l e r a n d o m i z a t i o n ( ) ; scv constraint manager, e.g. assignRandomValue, as well 8 ∗ c = 9 9 ; as in several internal utility routines called from other code 9 } within the SystemC verification standard, e.g. in 10 } ; scv set value. The result of our redesign now is a tight integration of Figure 4: Triangle constraint the weighting algorithm and the BDD synthesis operations. After structural modifications in the interfaces and correct hits initialization of internal data structures now the weighting hits algorithm is called after a simplification. Thus, the weights 1800 and probabilities are recomputed and a uniform distribution 1600 is achieved. In Figure 6 the result for the constraint from 1400 Example 5 is shown again for 100,000 times calling the SCV 1200 constraint solver. As can be seen a uniform distribution 1000 among all solution was established. 800 4. CONCLUSIONS 600 400 120 Constraint-based randomization using the SCV library is 200 100 crucial for complex verification tasks in todays system-on- 0 0 20 40 60 40 60 80 b chip designs. In this paper, two major problems of the SCV a 80 100 library have been tackled by a careful redesign and several 120 0 20 extensions of the SCV core. As a result, all issues that previously existed due to non-uniform distribution of gen- erated stimuli have been resolved. Moreover, as a benefit Figure 5: Distribution for a + b = 99 with original for the verification engineer during constraint creation, the SCV constraint specification language has been extended in ex- pressiveness. Both means a significant improvement in prac- hits ticality of the SystemC Verification Library. hits

1800                                                                                          5.      ACKNOWLEDGMENTS
1600                                                                                                           This research work was supported in part by the German
1400                                                                                          Federal Ministry of Education and Research (BMBF) in the
1200                                                                                          project URANOS under the contract number 01M3075.
1000
800
600                                                                                           6.[1]   REFERENCES
400                                                                                                   K. Brace, R. Rudell, and R. Bryant. Efficient implementation
200                                                                                     120           of a BDD package. In Design Automation Conf., pages 40–45,
                                                                                     100              1990.
   0 0          20 40              60                                40     60   80     b      [2]    R. Bryant. Graph-based algorithms for Boolean function
                                                                                                      manipulation. IEEE Trans. on Comp., 35(8):677–691, 1986.
                                            80                       20                        [3]    R. S. French, M. S. Lam, J. R. Levitt, and K. Olukotun. A
                            a                    100         120 0                                    general method for compiling event-driven simulations. In
                                                                                                      Design Automation Conference, pages 151–156, 1995.
                                                                                               [4]    D. Große, R. Siegmund, and R. Drechsler. Processor
                                                                                                      verification. In P. Ienne and R. Leupers, editors, Customizable

Figure 6: Distribution for a + b = 99 with improved Embedded Processors, pages 281–302. Elsevier, 2006. SCV [5] T. Gr¨otker, S. Liao, G. Martin, and S. Swan. System Design with SystemC. Kluwer Academic Publishers, 2002. ated. Hence if a previous constraint is simplified, this num- [6] C. N. Ip and S. Swan. A tutorial introduction on the new ber is not available anymore. This is a problem since the SystemC verification standard. http://www.systemc.org. weighting algorithm crucially depends on this number. There White paper, 2003. are similar problems with the information contained in two [7] W. M¨uller, W. Rosenstiel, and J. Ruf, editors. SystemC Methodologies and Applications. Kluwer Academic Publishers, hash tables stored at the constraint manager object: the ta- 2003. bles nodeHashP and nodeWeightHash hold the probability in- [8] J. Rose and S. Swan. SCV randomization version 1.0. 2003. formation for all nodes of the BDD representing a constraint [9] R. Siegmund, U. Hensel, A. Herrholz, and I. Volt. A functional and the according weighting information, respectively. At coverage prototype for SystemC-based verification of chipset designs. In 9th European SystemC User Group Meeting at the time of simplification of a previous constraint, the data Design, Automation and Test in Europe, 2004. stored in the table needs to be cleared which is not done by [10] F. Somenzi. CUDD: CU Decision Diagram Package Release the SCV system. 2.3.0. University of Colorado at Boulder, 1998. We did a complete redesign of the constraint management [11] Synopsys Inc., CoWare Inc., and Frontier Design Inc., classes that also solved these problems. Furthermore we http://www.systemc.org. Functional Specification for SystemC 2.0. put more intelligence into the constraint objects. E.g. now [12] SystemC Verification Working Group, every constraint object is capable of giving back a pointer http://www.systemc.org. SystemC Verification Standard to its BDD representation via a method getBddNodeP. We [13] Specification Version 1.0e. have preserved backwards compatibility and full functional- J. Yuan, C. Pixley, and A. Aziz. Constraint-based Verification. Springer, 2006.