SOURCE ARCHIVE
EXTRACTED CONTENT
49,155 chars CRAVE: An Advanced Constrained RAndom
Verification Environment for SystemC
Finn Haedicke1 Hoang M. Le1 Daniel Große1 Rolf Drechsler1,2
1Institute of Computer Science, University of Bremen, 28359 Bremen, Germany
2Cyber-Physical Systems, DFKI GmbH, 28359 Bremen, Germany
{finn, hle, grosse, drechsle}@informatik.uni-bremen.de
Abstract—A huge effort is necessary to design and verify com- unexpected assertion violations since scenarios are simulated
plex systems like System-on-Chip. Abstraction-based methodolo- which the verification engineer might have not thought of.
gies have been developed resulting in Electronic System Level Second, the stimulus generation process is automated and
(ESL) design. A prominent language for ESL design is SystemC
offering different levels of abstraction, interoperability and the hence a huge set of scenarios can be executed leading to
creation of very fast models for early software development. higher coverage. Hence, for large and complex systems the
For the verification of SystemC models, Constrained Random confidence in the correct functionality significantly increases.
Verification (CRV) plays a major role. CRV allows to automati- For SystemC CRV is available through the SystemC Ver-
cally generate simulation scenarios under the control of a set of ification (SCV) library [13], [14], [15]. However, the SCV constraints. Thereby, the generated stimuli are much more likely to hit corner cases. However, the existing SystemC Verification library has several deficiencies: library (SCV), which provides CRV for SystemC models, has 1) Poor dynamic constraint support, hence no control of several deficiencies limiting the advantages of CRV. In this paper constraint effects at run-time we present CRAVE, an advanced constrained random verification environment for SystemC. New dynamic features, enhanced 2) No constraint specification for dynamic data-structures usability and efficient constraint-solving reduce the user effort 3) Low usability when specifying constraints for composed and thus improve the verification productivity. data structures I. INTRODUCTION 4) Poor information in case of over-constraining Creating a new System-on-Chip (SoC) involves many tasks. 5) Limits in complexity of constraints, since constraint- Once the specification is agreed on, the modeling phase solving is based on Binary Decision Diagrams starts to derive a potential solution. To manage the complex- (BDDs) [16] only ity of today’s SoCs high-level languages are used for the In this paper we present CRAVE, an advanced Constrained first models. For this Electronic System Level (ESL) design RAndom Verification Environment for SystemC.1 To overcome phase [1] a widely accepted approach is SystemC [2], [3], the limitations of the SCV library CRAVE provides the follow- [4], [5]. Integrated hardware and software models can be ing features: developed, exchanged and refined based on the SystemC IEEE • New constraint specification API standard [6]. In particular, Transaction Level Modeling [7], [8] An intuitive and user-friendly Application Programming allows to create high performance virtual platforms for early Interface (API) to specify random variables and random software development and architectural analysis. In addition, objects has been developed. the high-level models serve as reference to verify the behavior • Dynamic constraints and data structures of the more detailed descriptions built in the following stages. Constraints can be controlled dynamically at run-time. In general, facing today’s verification challenges a verifica- Moreover, constraints for elements of dynamic data struc- tion environment needs to be constructed. From a high-level tures like e.g. STL vectors can be specified. perspective three major components are necessary: stimuli, • Improved usability assertions and coverage. Assertions are used to check the func- Inline constraints can be formulated and changed incre- tional correctness and therefore monitor design variables [9]. mentally at run-time. Furthermore, automatic debugging The task of functional coverage is to measure which design of unsatisfiable constraints is supported. functionality has been exercised during simulation [10]. Both • Parallel constraint-solving are not in the focus of this work. Here, we target the BDD-based and SAT/SMT-based techniques have been problem of stimuli generation. But instead of deterministic integrated for constraint-solving. A portfolio approach is values as defined in traditional directed testbenches we make used to enable very fast generation of constraint solutions. use of Constrained Random Verification (CRV) [11], [12]. Please note the usage of CRAVE is not limited to pure CRV applies input stimuli to the design that are solutions of hardware designs. For example, the constraint solutions can constraints. These solutions are determined by a constraint- also be used to describe software tests running on a SoC. In solver. CRV offers two key benefits: First, CRV enables to find the experiments such an example is presented. This work was supported in part by the German Federal Ministry of For an industrial application of CRAVE we refer to [17]. Education and Research (BMBF) within the project SANITAS under contract no. 01M3088 and by the German Research Foundation (DFG) within the 1CRAVE is freely available (w/ source code) under MIT license at Reinhart Koselleck project DR 287/23-1. www.systemc-verification.org.
The rest of this paper is structured as follows: Related 1 struct packet : public rand_obj {
work is discussed in Section II. Section III presents the 2 randv< unsigned int > src_addr;
API of CRAVE. Then, in Section IV the dynamic features of 3 randv< sc_uint<16> > dest_addr;
CRAVE are introduced. The usability aspects are described in 4
Section V. Section VI presents the constraint-solving approach 5 packet() : src_addr(this), dest_addr(this) {
of CRAVE and Section VII compares CRAVE to the SCV library 6 constraint(src_addr() <= 0xFFFF);
in an experimental evaluation. Finally, the paper is concluded 7 constraint("diff", src_addr() != dest_addr());
in Section VIII. 8 soft_constraint(dest_addr() % 4 == 0);
II. RELATED WORK 9 }
As mentioned above, the CRV techniques of the SCV library 10 };
have several weaknesses which limits their use in practice. Figure 1: A basic constrained random packet
Therefore, several improvements for the SCV library have
been developed. In [18] bit-vector operators have been added 1 struct packet1 : public packet {
and the uniform distribution among all constraint solutions 2 randv< char > data;
is ensured in all cases. An approach to determine the exact 3 packet1() : data(this) {
reasons in case of over-constraining has been presented in [19]. 4 constraint(’a’ <= data() && data() <= ’z’);
In [20] the BDD-based constraint-solver is replaced by a 5 constraint(dest_addr() % 2 == 1);
method which uses a generalization of Boolean Satisfiability 6 }
(SAT). 7 };
However, all these approaches compensate only some of
the SCV weaknesses. In particular, no constraints on dynamic Figure 2: An inherited packet
data structures can be specified, constraints cannot be con-
trolled dynamically during run-time, references to the state
of constraints are not available, and no inline constraints are B. Random object
possible restricting the usability. In addition, the integration of
different constraint-solvers working in parallel is mandatory to Complex constrained random objects can also be specified.
reduce the time for stimuli generation to a minimum. They must inherit from the class rand_obj provided by CRAVE.
To standardize verification processes the so-called Universal Such an object can contain several instances of randv
Table I: The APIs of randv<int>
Description API
Supported operators +, −, ∗, /, %, ==, ! =, >, <, >=, <=, !, &&, ||, ∼, &, |, <<, >>, ^
Add range to distribution addRange(left, right)
Add weighted range addWeightedRange(left, right, weight)
Generate random value next() returns true on success
Symbolic link x() with x being a variable of type randv<int>
Table II: The basic APIs of rand_obj Currently only C/C++ and SystemC built-in data types are sup-
Description API ported as the template parameter T. The class rand_vec<T>
Add hard constraint constraint(expression) also implements the APIs of the STL class vector and thus
Add named hard constr. constraint(name, expression) behaves as if it is an STL vector. Similar to randv<T>, for
Add soft constraint soft_constraint(expression) an instance v of rand_vec<T>, v refers to the actual vector,
Randomize the object next() returns true on success while v() is the symbolic vector used to specify constraints. For
the symbolic vector v(), v().size() refers to the size, v()[_i] to a
symbolic vector element, and v()[_i - c] to a previous element
relative to v()[_i] (_i is a predefined constant in CRAVE and
C. Constraint Inheritance c is a positive constant). The symbolic elements v()[_i] and
The inheritance/reuse of constraints in CRAVE is straight- v()[_i - c] are used in a foreach constraint. forward. The user can add more fields and constraints to an Figure 3 shows an extension of our packet with the data existing random constrained object by using C++ class inher- field, now being a constrained random vector. The constraint itance. Figure 2 shows an extension of the packet introduced on the vector is declared in line 5. In the next lines, three in the last section. Line 2 adds a data field to the packet. foreach constraints are specified for the vector. The first two The constraint for this data field is declared in line 4. The ensure that the first element is an upper case letter and the destination address of the packet is further constrained to be rest are lower case letters. Both are hard constraints. The third an odd integer on line 5. This new hard constraint contradicts constraint (line 14) is a soft foreach constraint: two consecutive the soft constraint specified on line 8 of Figure 1 and therefore elements cannot be aa, ab or ba. renders the soft constraint useless. The APIs of CRAVE described in this section are the B. Dynamic Constraint Management basics to specify constrained random objects. Similar APIs During the constrained random verification process, it is are also available in the SCV library to a greater or lesser very useful that the user can enable/disable specific con- extent. However, CRAVE enables an enhanced usability in straints of a random object. This functionality is not avail- comparison to the SCV library as discussed in Section V. In able in the SCV library. The user must mimic the feature the next section we introduce the distinctive features of CRAVE by adding an auxiliary variable and constrain this variable regarding dynamic constraints and data structures. in an implication with the constraints to be enabled/dis- abled. Moreover, this is inconvenient and inefficient. In the CRAVE framework, named constraints can be enabled/disabled IV. DYNAMIC CONSTRAINTS AND DATA STRUCTURES directly via the constraint management APIs of rand_obj: This section introduces three distinctive features of CRAVE enable_constraint(name) and disable_constraint(name). For which are not supported by the SCV library: constraints on example, the constraint on line 7 of Figure 1 can be disabled dynamic data structures (currently only vector is supported), by calling disable_constraint("diff"). Disabled constraints will dynamic enabling/disabling of constraints, and the concept of have no effect in the randomization via next() until they are references that allows the randomization to interact tightly with enabled again. Note that the vector constraint foreach can the verification environment. also be named and intentionally soft constraints cannot be enabled/disabled.
A. Vector Constraints C. References
The SCV library offers no direct support for the constrained In many use cases, the randomization depends on the
randomization of dynamic data structures such as vectors, dynamically changing state of the verification environment.
lists and trees. The user must mimic dynamic data structures Using the SCV library, to include the state in the constraints
by using arrays of fixed-size. This is inconvenient and not the user must use additional variables to save the state and
memory-efficient. Furthermore, the upper-bound on size of update them manually whenever the state is changed. For this
dynamic data structures might not be known at the time purpose, CRAVE provides references as a convenient shortcut.
of constraint specification. CRAVE offers a template class References in CRAVE basically links a “real” variable with
rand_vec
1 struct packet2 : public packet { 1 randv<int> x,y;
2 rand_vec< char > data; 2 Generator gen;
3 3
4 packet2() : data(this) { 4 gen(x() != y());
5 constraint( data().size() % 4 == 0 5 for (int i =0 ; i < 1000; ++i) {
6 && data().size() < 100 ); 6 gen.next();
7 7 run_test(x,y);
8 constraint.foreach( data, _i, IF_THEN( _i == 0, 8 }
9 ’A’ <= data()[_i] && data()[_i] <= ’Z’) ); 9
10 10 gen( x()∗x() == y() );
11 constraint.foreach( data, _i, IF_THEN( _i != 0, 11 for (int i =0 ; i < 500; ++i) {
12 ’a’ <= data()[_i] && data()[_i] <= ’z’) ); 12 gen.next();
13 13 run_test(x,y) ;
14 constraint.soft_foreach( data, _i, 14 }
15 data()[_i] + data()[_i−1] > ’a’ + ’b’); 15
16 } 16 gen( y()%2 == 0 );
17 }; 17 for (int i =0 ; i < 500; ++i) {
18 gen.next();
Figure 3: An inherited packet using vector constraints 19 run_test(x,y) ;
20 }
1 packet2(int &expected_max_size) : data(this) {
2 constraint(data().size() % 4 == 0 Figure 5: Incremental constraint modification
3 && data().size() <=
4 reference(expected_max_size)); 1 randv<int> x,y;
5 ... 2 Generator gen;
6 } 3
4 gen( x() < y() );
Figure 4: Example of CRAVE reference 5 gen( x() > 100 || y() < −100);
6
7 if (gen.next()) run_test(x,y);
specification. Before the constraints are solved, the value of
this symbolic variable is fixed to the actual value of the linked This example declares two variables x, y (line 1) and a
variable. Figure 4 gives an example for using references: The constrained random generator (gen, line 2). The generator
size of the constrained random vector data of the packet in can simply be called to add new constraints: the relation of x
Figure 3 should not exceed the value of environment variable and y (line 4) is specified and that either x has to be larger
expected_max_size, which is constantly changing. As can be than 100 or y is less that −100 (line 5) is constrained. To
seen, the construct reference links expected_max_size to a generate values, the next function can be called which returns
symbolic variable and data().size() is constrained to be smaller false if the generator is over-constrained, i.e. the constraints
or equal to this symbolic variable. are contradictory and hence no solution exists. When the
The new features introduced in this section demonstrated constraint-solver has generated a stimulus, the randv
over-constrained and hence the constraint-solver is unable to
generate valid stimuli. Debugging the contradiction manually CRAVE
is very time-consuming. Therefore CRAVE can automatically Syntax, Data types, randv, rand_obj
identify which named constraints are part of a conflict.
As discussed earlier the soft constraint in Figure 1 (line 8) METASMT
and the constraint in Figure 2 (line 5) form a conflict. If
the former constraint would have been declared as a hard METASMT FRONTEND (C++)
constraint, no constraint solution exists. For such situations Domain Specific Language
CRAVE provides an analyzer, that identifies the conflicting
constraints and returns their names. The analysis includes METASMT MIDDLE-END
each named constraint and checks them against all unnamed Transformations, APIs, Parallelization
constraints, which are always enabled. In a first step the
analyzer determines how many and which constraints need
to be disabled to resolve all contradictions. In subsequent METASMT BACKEND
steps each of these constraints is expanded to determine the SWORD Z3 MiniSAT CUDD
“complete” contradiction. For the example, the first step would
determine that one contradiction exists and identify the first Boolector PicoSAT AIGER
constraint. In the next step the second constraint is identified.
This is completely done on a formal level, therefore the
algorithm is complete and will return all minimal subsets of SOLVER API
the constraints that form a conflict. For the described example the run-time of the analysis was negligible. Figure 6: Constraint-Solving Architecture VI. PARALLEL CONSTRAINT-SOLVING Various alternatives to BDD-based constraint-solving have Then, the result of the fastest solver would be used. However, been studied, see e.g. [22]. Approaches based on Boolean for CRV a predictable quality of the stimuli is required. Satisfiability (SAT) [23], [24] or Satisfiability Modulo The- Therefore, if a BDD can be built for the overall constraint this ories (SMT) [20] have shown to give very good results for is preferred since a uniform distribution among all solutions constraints which are hard to solve for BDDs. However, in can be guaranteed2. In CRAVE this is reflected by running the general it is not possible to know in advance which type of SMT-solver only until the BDD is build. From this point on constraint-solver will show the best performance. Therefore, only the BDD is used and execution the SMT solver is stopped. CRAVE uses a portfolio approach. Instead of running a specific constraint-solver, an SMT-based constraint-solver as well as a VII. EXPERIMENTAL E VALUATION BDD-based constraint-solver are executed in parallel for the same set of constraints. This section describes the basics for In the following examples we demonstrate the advantages constraint solving and how the portfolio approach works. The of CRAVE for stimuli generation. next section will compares the run-times of CRAVE and the SCV library. A. Arithmetic Constraints To integrate the most recent reasoning engines we use Figure 7 shows a constraint object for a 16 bit ALU (later metaSMT [25] for implementing the constraint-solving in we scale the size of the ALU). The constraint specifies four CRAVE. Essentially, metaSMT allows engine independent pro- operations with their respective input ranges. Table III shows gramming by providing a unified interface to different solvers. the differences between the classical BDD constraints solver Hence, no algorithmic changes are necessary when switch- of the SCV and the portfolio approach of CRAVE. The first ing to another solver. The overall architecture is depicted column gives the name of the library. Two rows are given in Figure 6. As can be seen CRAVE forms the top layer for both: The first row shows the run-time needed to generate which implements all the features described in the previous the first solution, and the second row shows the run-time in sections. This layer connects to the metaSMT front-end layer seconds for the complete execution of the constraint generator, using the unified input language. In the middle-end layer the respectively. The following columns provide the data for transformations for optimization and the basic parallelization different bit width of the ALU constraints. As can be seen with features (e.g. threading of different engines) is available. increasing bit width of the ALU the SCV fails to solve the Finally, the backend gives access to a wide range of solvers constraints. In contrast, in CRAVE the SMT-solver can already (see e.g. SWORD [26], Z3 [27], Boolector [28], MiniSAT [29], generate stimuli before the BDD is ready. Furthermore, note PicoSAT [30], CUDD [31] and AIGER [32]). that for ALU16 the 32 bit memory restriction of the SCV Based on these constraint-solving techniques we have made the following observations for parallelization. In a simple port- 2A BDD represents all solutions and hence to select each solution with folio approach each constraint would be evaluated (at least) the same probability is simple. Essentially each path to the 1-terminal needs twice using different solvers in a multi-threaded environment. to be weighted accordingly respecting the reduction rules of reduced ordered BDDs.
1 struct ALU16 : public rand_obj { 1 class sudoku : public rand_obj {
2 randv< sc_bv<2> > op ; 2 public:
3 randv< sc_uint<16> > a, b ; 3 // variable to store solved sudoku
4 randv< sc_dt::sc_uint<4> > res_sdk[9][9];
4 5 // variable to hold given sudoku
5 ALU16() : op(this), a(this), b(this) { 6 int given_sudoku[9][9];
6 constraint(IF_THEN(op() == 0, 7
8 sudoku(rand_obj∗ parent = 0) : rand_obj(parent) {
7 65535 >= a() + b()) ); 9 // constrain given numbers
8 constraint(IF_THEN(op() == 1, 10 for (int i = 0; i < 9; i++)
9 65535 >= a() − b() 11 for (int j = 0; j < 9; j++)
12 constraint( IF_THEN( reference(given_sudoku[i][j]) != 0,
10 && b() <= a()) ); 13 res_sdk[i][j]() == reference(given_sudoku[i][j]) ) );
11 constraint(IF_THEN(op() == 2, 14
12 65535 >= a() ∗ b()) ); 15 // only numbers from 1 to 9 are allowed
16 for (int i = 0; i < 9; i++)
13 constraint(IF_THEN(op() == 3, 17 for (int j = 0; j < 9; j++)
14 b() != 0)); 18 constraint((res_sdk[i][j]() >= 1) && (res_sdk[i][j]() <= 9));
15 } 19
20 // every number must appear exactly one time in one row
16 }; 21 for (int i = 0; i < 9; i++)
22 for (int j = 0; j < 9; j++)
Figure 7: 16 bit ALU constraint 23 for (uint k = j + 1; k < 9; k++)
24 constraint( res_sdk[i][j]() != res_sdk[i][k]() );
25
Table III: Comparison of CRAVE and the SCV 26 // every number must appear exactly one time in one column
27 for (int j = 0; j < 9; j++)
28 for (int i = 0; i < 9; i++)
ALU4 ALU12 ALU16 ALU24 ALU32 29 for (int k = i + 1; k < 9; k++)
first < 0.01 13.77 MO TO TO 30 constraint( res_sdk[i][j]() != res_sdk[k][j]() );
SCV finished 0.09 19.84 MO TO TO 31
32 // every number must appear exactly one time in one region
first < 0.01 < 0.01 0.01 0.01 0.01 33
CRAVE finished 0.14 0.30 0.37 0.40 0.49 34 for (int i = 0; i < 9; i++)
for (int j = 0; j < 9; j++)
35 constraint
TO = time out, MO = memory out, run-time in seconds 36 ( res_sdk[i][j]() != res_sdk[ index(i,1) ][ j ]() )
37 ( res_sdk[i][j]() != res_sdk[ index(i,2) ][ j ]() )
library was hit. CRAVE can also be build on 64 bit architectures 38
39 ( res_sdk[i][j]() != res_sdk[ i ][ index(j,1) ]() )
which was however not required for theses experiments. 40 ( res_sdk[i][j]() != res_sdk[ index(i,1) ][ index(j,1) ]() )
41 ( res_sdk[i][j]() != res_sdk[ index(i,2) ][ index(j,1) ]() )
42
B. Sudoku Constraints 43 ( res_sdk[i][j]() != res_sdk[ i ][ index(j,2) ]() )
In the second experiment we formulated the rules of the 44 ( res_sdk[i][j]() != res_sdk[ index(i,1) ][ index(j,2) ]() )
45 ( res_sdk[i][j]() != res_sdk[ index(i,2) ][ index(j,2) ]() );
Sudoku puzzle in CRAVE and the SCV library. Figure 8 gives 46 }
the respective constraints. In line 4 the 81 random variables 47 };
of 4 bit size each are declared as the two-dimensional array 48
49 int index(int x, int by ) {
res_sdk. Then, in line 6 the standard C++ two-dimensional 50 return (x + by) % 3 + x − (x % 3);
array given_sudoku is declared which is filled when reading 51 }
the Sudoku numbers from a file. From line 9 on five types of Figure 8: Sudoku Constraints
constraints follow. At first, the numbers of the given_sudoku
array are assigned to the constraint variables (line 13). Note Table IV: Comparison of CRAVE and the SCV
that we use here the reference feature of CRAVE. Hence, if Sudoku min max median
a solution for the Sudoku-constraint is requested (by calling
next), then the current values of given_sudoku are used as SCV time 2 636.60 4 529.07 3 165.34
values for the constraint variables. In other words the standard mem MO MO MO
C++ array given_sudoku can be changed anywhere and the CRAVE time 0.81 1.83 1.42
actual values will be used in the constraint automatically. Next, mem 14.00 15.40 14.40
the ”obvious” constraints stating a valid solution range for each MO = memory out, run-time in seconds
field (line 15), difference of rows and columns (line 20 and
26) are formulated. Finally, from line 32 on the difference per
region is modeled. aggregated results in Table IV. Although plenty of memory
For 15 puzzles the constraint-solver had to find a solution was provided, the SCV library could not solve a single (between 16-32 numbers are set in the puzzle; 1 was unsolv- instance3. In contrast, CRAVE solved all instances very fast. able). The run-time (in seconds) and the memory consumption (in MB) were measured with a limit of 2 CPU hours or 3 Note these instances are not inherently hard for BDD-based solvers. A 4 GB of memory for each Sudoku instance. The evaluation showed largely homogeneous result, hence we only present the dedicated BDD-based Sudoku solving algorithm was able to find the solution for each instance in less than a minute using no more than 216 MB of memory.
1 struct bubble_sort_input : public rand_obj { summary, CRAVE improves the verification productivity for
2 // start address in mem SystemC models significantly.
3 randv< unsigned int > start; A possible direction for future work is to extend the support
4 rand_vec< unsigned int > data; for dynamic data structures and to improve the distribution of
5 the SAT/SMT generated stimuli.
6 bubble_sort_input() : start(this), data(this) { REFERENCES
78 constraint(0x70 <= start() && start() < 1024); [1] B. Bailey, G. Martin, and A. Piziali, ESL Design and Verification: A
constraint(start() % 4 == 0); Prescription for Electronic System Level Methodology. Morgan Kaufman-
9 [2] n/Elsevier, 2007.
10 constraint( 0 < data().size() Accellera Systems Initiative, “SystemC,” 2012, available at
http://www.systemc.org.
11 && data().size() < 1024); [3] T. Grötker, S. Liao, G. Martin, and S. Swan, System Design with SystemC.
12 constraint(start() + 4 ∗ data().size() <= 1024); [4] Kluwer Academic Publishers, 2002.
D. C. Black and J. Donovan, SystemC: From the Ground Up. Springer-
13 Verlag New York, Inc., 2005.
14 constraint.foreach( [5] D. Große and R. Drechsler, Quality-Driven SystemC Design. Springer,
2010.
15 data, _i, data()[_i] <= 0x00FFFFFF ); [6] IEEE Standard SystemC Language Reference Manual, IEEE Std. 1666,
16 constraint.foreach( [7] 2005.
17 data, _i, data()[_i] <= data()[_i−1] + 5); L. Cai and D. Gajski, “Transaction level modeling: an overview,” in
CODES+ISSS, 2003, pp. 19–24.
18 } [8] F. Ghenassia, Transaction-Level Modeling with SystemC: TLM Concepts
19 }; [9] and Applications for Embedded Systems. Springer, 2006.
H. Foster, A. Krolnik, and D. Lacey, Assertion-Based Design. Kluwer
[10] Academic Publishers, 2003.
Figure 9: Input data constraints for bubble sort S. Tasiran and K. Keutzer, “Coverage metrics for functional validation of
hardware designs,” IEEE Design and Test of Computers, vol. 18, no. 4, pp.
[11] 36–45, 2001.
C. Program Input Generation for CPU Testbench [12] J. Bergeron, Writing Testbenches Using SystemVerilog. Springer, 2006.
J. Yuan, C. Pixley, and A. Aziz, Constraint-based Verification. Springer,
2006.
We also apply CRAVE to verify a CISC CPU with 8 [13] SystemC Verification Standard Specification Version 1.0e, SystemC Verifi- registers of 32 bit data width each. The CPU implements a [14] cation Working Group, http://www.systemc.org, 2003. J. Rose and S. Swan, SCV Randomization Version 1.0, 2003. subset of the instructions of the IA-32 architecture including [15] C. N. Ip and S. Swan, “A tutorial introduction on the new SystemC load/store, arithmetic, jump and halt instructions [33]. The [16] verification standard,” www.systemc.org, White Paper, 2003. R. E. Bryant, “Graph-based algorithms for Boolean function manipulation,” CPU is available at three different levels of abstraction: an IEEE Trans. on Comp., vol. 35, no. 8, pp. 677–691, 1986. Instruction Set Architecture (ISA) model in C++, a SystemC [17] M. F. S. Oliveira, C. Kuznik, W. Mueller, F. Haedicke, H. M. Le, D. Große, TLM model using OSCI TLM-2.0, and a SystemC RTL model R. Drechsler, W. Ecker, and V. Esen, “The system verification methodology for advanced TLM verification,” in CODES+ISSS, 2012. implementing a five-stage pipeline [34], [35]. We use CRAVE [18] D. Große, R. Ebendt, and R. Drechsler, “Improvements for constraint solv- to generate programs (i.e. instruction sequences) as well as ing in the SystemC verification library,” in ACM Great Lakes Symposium on VLSI, 2007, pp. 493–496. their inputs, which can be used as stimuli for all three models. [19] D. Große, R. Wille, R. Siegmund, and R. Drechsler, “Contradiction analysis Then, the simulation-based equivalence checking approach [20] for constraint-based random simulation,” in FDL, 2008, pp. 130–135. R. Wille, D. Große, F. Haedicke, and R. Drechsler, “SMT-based stimuli in [35] for models at different levels of abstraction is applied. generation in the SystemC verification library,” in FDL, 2009, pp. 1–6. We describe only one verification scenario: for an instruction [21] Accellera Systems Initiative - Universal Verification Methodology 1.1, N. Kitchen and A. Kuehlmann, “Stimulus generation for constrainted ran- sequence implementing the bubble sort algorithm, we random- [22] http://www.accellera.org, 2011. ize its input under the constraints shown in Figure 9. The first [23] dom simulation,” in Int’l Conf. on CAD, 2007, pp. 258–265. four constraints ensure that the array to be sorted fits into the S. M. Plaza, I. L. Markov, and V. Bertacco, “Random stimulus generation using entropy and XOR constraints,” in DATE, 2008, pp. 664–669. CPU memory and does not collide with the loaded program. [24] H. Kim, H. Jin, K. Ravi, P. Spacek, J. Pierce, B. Kurshan, and F. Somenzi, The last constraint forces the array to be nearly non-increasing “Application of formal word-level analysis to constrained random simula- tion,” in CAV, 2008. (and thus challenging for bubble sort). Such a concise set of [25] F. Haedicke, S. Frehse, G. Fey, D. Große, and R. Drechsler, “metaSMT: constraints would have not been possible with the SCV library Focus on your application not on solver integration,” in DIFTS’11: 1st International workshop on design and implementation of formal tools and due to the lack of support for dynamic data structures. The systems, 2011, pp. 22–29. average time for CRAVE to generate the first 1000 arrays is [26] R. Wille, G. Fey, D. Große, S. Eggersglüß, and R. Drechsler, “Sword: A approximately 90s (0.09s per array). SAT like prover using word level information,” in VLSI of System-on-Chip, [27] 2007, pp. 88–93. L. de Moura and N. Bjørner, “Z3: An efficient SMT solver,” in TACAS, [28] 2008, pp. 337–340. VIII. CONCLUSIONS R. Brummayer and A. Biere, “Boolector: An efficient SMT solver for bit- [29] vectors and arrays,” in TACAS, 2009, pp. 174–177. In this paper we have presented the advanced constrained N. Eén and N. Sörensson, “An extensible SAT-solver,” in SAT, 2003, pp. 502–518. random verification environment CRAVE. After the introduc- [30] A. Biere, “Picosat essentials,” JSAT, vol. 4, no. 2-4, pp. 75–97, 2008. tion of the API for constraint specification we have shown [31] F. Somenzi, CUDD: CU Decision Diagram Package Release 2.4.1. Uni- versity of Colorado at Boulder, 2009. the advantages of CRAVE in comparison to the existing SCV [32] “Aiger,” http://fmv.jku.at/aiger/. library. The advantages include dynamic constraint specifica- [33] IA-32 Architecture Software Developer’s Manual, Intel Corporation, 2003. [34] A. Biere, D. Kroening, G. Weissenbacher, and C. Wintersteiger, Digitaltech- tion and management, enhanced usability and much faster [35] nik - eine praxisnahe Einführung. Springer, 2008. constraint-solving based on a portfolio approach. All these D. Große, M. Groß, U. Kühne, and R. Drechsler, “Simulation-based equiva- lence checking between SystemC models at different levels of abstraction,” aspects have been demonstrated by means of examples. In in ACM Great Lakes Symposium on VLSI, 2011, pp. 223–228.