[LOGO]

Universität Bremen - Computer Architecture

An Advanced

Constrained Random Verification Environment for SystemC

Daniel Große, Finn Haedicke,

Hoang M. Le, Rolf Drechsler

Group of Computer Architecture, University of Bremen, Germany

1

[LOGO]

Universität Bremen - Computer Architecture

Outline

1. Motivation
2. Constraint Specification Random Variable Random Object Constraint Inheritance
3. Dynamic Constraints Dynamic Data Structures Constraint Management References in Constraints
4. Inline Generators usage
5. Parallel Constraint Solving
6. Summary

2

[LOGO]

Universität Bremen - Computer Architecture

Motivation

• ESL design to handle complexity (abstraction!)

3

[LOGO]

Universität Bremen - Computer Architecture

Motivation

• ESL design to handle complexity (abstraction!)
• Widely accepted ESL language: SystemC

3

[LOGO]

Universität Bremen - Computer Architecture

Motivation

• ESL design to handle complexity (abstraction!)
• Widely accepted ESL language: SystemC
• Verification dictates design costs

3

[LOGO]

Universität Bremen - Computer Architecture

Motivation

• ESL design to handle complexity (abstraction!)
• Widely accepted ESL language: SystemC
• Verification dictates design costs
• Manage verification effort by testbench automation ⇒ Constrained Random Verification (CRV)

3

[LOGO]

Universität Bremen - Computer Architecture

Motivation

• ESL design to handle complexity (abstraction!)
• Widely accepted ESL language: SystemC
• Verification dictates design costs
• Manage verification effort by testbench automation ⇒ Constrained Random Verification (CRV)
  • CRV for SystemC through SCV library

3

[LOGO]

Universität Bremen - Computer Architecture

Motivation

• ESL design to handle complexity (abstraction!)
• Widely accepted ESL language: SystemC
• Verification dictates design costs
• Manage verification effort by testbench automation ⇒ Constrained Random Verification (CRV)
  • CRV for SystemC through SCV library
  • SCV has several weaknesses

3

[LOGO]

Universität Bremen - Computer Architecture

Motivation

• ESL design to handle complexity (abstraction!)
• Widely accepted ESL language: SystemC
• Verification dictates design costs
• Manage verification effort by testbench automation ⇒ Constrained Random Verification (CRV)
  • CRV for SystemC through SCV library
  • SCV has several weaknesses
  • Development of Advanced CRV Environment

3

[LOGO]

Universität Bremen - Computer Architecture

Random Variable

randv x;

• x: variable of built-in or SystemC type T

4

U

Universität Bremen - Computer Architecture

Random Variable

randv x;

• x: variable of built-in or SystemC type T
• Simple constraints: addRange(1, r) addWeightedRange(1,r,w)

4

U

Universität Bremen - Computer Architecture

Random Variable

randv x;

• x: variable of built-in or SystemC type T
• Simple constraints: addRange(1, r) addWeightedRange(1,r,w)
• x(): symbolic variable used in complex constraints

4

U

Universität Bremen - Computer Architecture

Random Variable

randv x;

• x: variable of built-in or SystemC type T
• Simple constraints: addRange(1, r) addWeightedRange(1,r,w)
• x(): symbolic variable used in complex constraints
• C++ operators available for x and x() (+,-,*,/%, ==, !=, <,>, >=, <=, <<, >>, &&, ||, !, ~, &, |, ^)

4

U

Universität Bremen - Computer Architecture

Random Variable

randv x;

• x: variable of built-in or SystemC type T
• Simple constraints: addRange(1, r) addWeightedRange(1, r, w)
• x(): symbolic variable used in complex constraints
• C++ operators available for x and x() (+, -, *, /, %, ==, !=, <, >, >=, <=, <<, >>, &&, ||, !, ~, &, |, ^)

randv x;

// 30% in [0, 9] x.addWeightedRange(0, 9, 30);

// 70% in [90, 99] x.addWeightedRange(90, 99, 70);

// get value x.next();

4

[LOGO]

Universität Bremen - Computer Architecture

Random Object

rand_obj

• a random object extends rand_obj, contains randvs and other rand_objs.

5

[LOGO]

Universität Bremen - Computer Architecture

Random Object

rand_obj

• a random object extends rand_obj, contains randvs and other rand_objs.
• constraint specification in constructor/later via API call

5

[LOGO]

Universität Bremen - Computer Architecture

Random Object

rand_obj

• a random object extends rand_obj, contains randvs and other rand_objs.
• constraint specification in constructor/later via API call
• constraint([name,] expr): [named] hard constraint

5

[LOGO]

Universität Bremen - Computer Architecture

Random Object

rand_obj

• a random object extends rand_obj, contains randvs and other rand_objs.
• constraint specification in constructor/later via API call
• constraint([name,] expr): [named] hard constraint
• soft_constraint(expr): ignorable constraint

5

[LOGO]

Universität Bremen - Computer Architecture

Random Object

rand_obj

• a random object extends rand_obj, contains randvs and other rand_objs.
• constraint specification in constructor/later via API call
• constraint([name,] expr): [named] hard constraint
• soft_constraint(expr): ignorable constraint
• next() invokes constraint solver, returns true on success

5

U

Universität Bremen - Computer Architecture

Random Object

rand_obj

• a random object extends rand_obj, contains randvs and other rand_objs.
• constraint specification in constructor/later via API call
• constraint([name,] expr): [named] hard constraint
• soft_constraint(expr): ignorable constraint
• next() invokes constraint solver, returns true on success

struct packet : public rand_obj {

randv<unsigned> src;
randv< sc_uint<16> > dest;

packet() : ... {
    constraint(src() <= 0xFFFF);

    constraint("diff",
            src() != dest());

    soft_constraint(
            dest() % 4 == 0);
}

}

5

[LOGO]

Universität Bremen - Computer Architecture

Constraint Inheritance

• realized by C++ inheritance

6

[LOGO]

Universität Bremen - Computer Architecture

Constraint Inheritance

• realized by C++ inheritance
• inherit everything of the base class

6

[LOGO]

Universität Bremen - Computer Architecture

Constraint Inheritance

• realized by C++ inheritance
• inherit everything of the base class
• allows to add more random variables/objects and constraints to the base class

6

U

Universität Bremen - Computer Architecture

Constraint Inheritance

• realized by C++ inheritance
• inherit everything of the base class
• allows to add more random variables/objects and constraints to the base class

struct packet1 : public packet { randv data;

packet1() : ... {
    constraint('a' <= data() && data()
        <= 'z');
    constraint(dest_addr() % 2 == 1);
}

}

6

[LOGO]

Universität Bremen - Computer Architecture

Vector Constraints

rand_vec v;

• no support in SCV, mimic via fixed-size arrays (inconvenient and not always possible)

7

[LOGO]

Universität Bremen - Computer Architecture

Vector Constraints

rand_vec v;

• no support in SCV, mimic via fixed-size arrays (inconvenient and not always possible)
• v mimics a STL vector std::vector (T built-in type)

7

[LOGO]

Universität Bremen - Computer Architecture

Vector Constraints

rand_vec v;

• no support in SCV, mimic via fixed-size arrays (inconvenient and not always possible)
• v mimics a STL vector std::vector (T built-in type)
• v(): symbolic vector used in constraints

7

[LOGO]

Universität Bremen - Computer Architecture

Vector Constraints

rand_vec v;

• no support in SCV, mimic via fixed-size arrays (inconvenient and not always possible)
• v mimics a STL vector std::vector (T built-in type)
• v(): symbolic vector used in constraints
• v().size(): size of symbolic vector

7

[LOGO]

Universität Bremen - Computer Architecture

Vector Constraints

rand_vec v;

• no support in SCV, mimic via fixed-size arrays (inconvenient and not always possible)
• v mimics a STL vector std::vector (T built-in type)
• v(): symbolic vector used in constraints
• v().size(): size of symbolic vector
• v()[_i]: symbolic element (_i predefined constant)

7

U

Universität Bremen - Computer Architecture

Vector Constraints

rand_vec v;

• no support in SCV, mimic via fixed-size arrays (inconvenient and not always possible)
• v mimics a STL vector std::vector (T built-in type)
• v(): symbolic vector used in constraints
• v().size(): size of symbolic vector
• v()[_i]: symbolic element (_i predefined constant)
• v()[_i-c]: previous element relative to v()[_i] (c > 0)

7

U

Universität Bremen - Computer Architecture

Vector Constraints

rand_vec v;

• no support in SCV, mimic via fixed-size arrays (inconvenient and not always possible)
• v mimics a STL vector std::vector (T built-in type)
• v(): symbolic vector used in constraints
• v().size(): size of symbolic vector
• v()[_i]: symbolic element (_i predefined constant)
• v()[_i-c]: previous element relative to v()[_i] (c > 0)
• constraint.foreach and constraint.soft_foreach to build constraints over the elements

7

Universität Bremen - Computer Architecture

Vector Constraints - Example

struct packet2 : public packet { rand_vec data;

packet2() : ... {
    constraint(data().size() % 4 == 0);
    constraint(data().size() < 100);

    // data[0] upper case
    constraint.foreach(data, _i,
        IF_THEN(_i == 0, 'A' <= data()[_i] && data()[_i] <= 'Z'));
    // the rest lower case
    constraint.foreach(data, _i,
        IF_THEN(_i != 0, 'a' <= data()[_i] && data()[_i] <= 'z'));
    // forbid aa, ab and ba
    constraint.soft_foreach(data, _i,
        data()[_i] + data()[_i-1] > 'a' + 'b');
}

};

8

[LOGO]

Universität Bremen - Computer Architecture

Constraint Management

• Enable/disable specific constraints during verification process

9

[LOGO]

Universität Bremen - Computer Architecture

Constraint Management

• Enable/disable specific constraints during verification process
• Not available in SCV, mimic via auxiliary variables and implication constraints (inconvenient and inefficient)

9

[LOGO]

Universität Bremen - Computer Architecture

Constraint Management

• Enable/disable specific constraints during verification process
• Not available in SCV, mimic via auxiliary variables and implication constraints (inconvenient and inefficient)
• Supported via named constraints constraint(name, expr).

9

[LOGO]

Universität Bremen - Computer Architecture

Constraint Management

• Enable/disable specific constraints during verification process
• Not available in SCV, mimic via auxiliary variables and implication constraints (inconvenient and inefficient)
• Supported via named constraints constraint(name, expr).
• API: enable_constraint(name) and disable_constraint(name) of rand_obj

9

[LOGO]

Universität Bremen - Computer Architecture

Constraint Management

• Enable/disable specific constraints during verification process
• Not available in SCV, mimic via auxiliary variables and implication constraints (inconvenient and inefficient)
• Supported via named constraints constraint(name, expr).
• API: enable_constraint(name) and disable_constraint(name) of rand_obj
• Disabled constraints have no effect in the randomization via next() until enabled again

9

[LOGO]

Universität Bremen - Computer Architecture

References

• Randomization depends on dynamically changing environment state

10

[LOGO]

Universität Bremen - Computer Architecture

References

• Randomization depends on dynamically changing environment state
• In SCV inefficient and tedious (additional variables, manual update)

10

[LOGO]

Universität Bremen - Computer Architecture

References

• Randomization depends on dynamically changing environment state
• In SCV inefficient and tedious (additional variables, manual update)
• Here via reference(x): link a C++ variable x to a symbolic variable used in constraints

10

[LOGO]

Universität Bremen - Computer Architecture

References

• Randomization depends on dynamically changing environment state
• In SCV inefficient and tedious (additional variables, manual update)
• Here via reference(x): link a C++ variable x to a symbolic variable used in constraints
• Each call to next() uses actual value of x

10

U

Universität Bremen - Computer Architecture

References

• Randomization depends on dynamically changing environment state
• In SCV inefficient and tedious (additional variables, manual update)
• Here via reference(x): link a C++ variable x to a symbolic variable used in constraints
• Each call to next() uses actual value of x

struct packet3 : public packet { rand_vec data;

packet3(int &expected_max_size) : ... {
    constraint(data().size() % 4 == 0);

    constraint(data().size() <=
        reference(expected_max_size));
    // data[0] upper case
    ...
}

};

10

[LOGO]

Universität Bremen - Computer Architecture

Inline Generators

• Constraint specification without random_obj

11

[LOGO]

Universität Bremen - Computer Architecture

Inline Generators

• Constraint specification without random_obj
• Based on Generator object

11

[LOGO]

Universität Bremen - Computer Architecture

Inline Generators

• Constraint specification without random_obj
• Based on Generator object
• Usable anywhere independent of other constraints

11

[LOGO]

Universität Bremen - Computer Architecture

Inline Generators

• Constraint specification without random_obj
• Based on Generator object
• Usable anywhere independent of other constraints
• All features except for inheritance

11

[LOGO]

Universität Bremen - Computer Architecture

Inline Generators

• Constraint specification without random_obj
• Based on Generator object
• Usable anywhere independent of other constraints
• All features except for inheritance

randv x,y; Generator gen;

gen( x() < y() ); gen( x() > 100 || y() < 50);

if (gen.next()) run_test(x,y);

11

[LOGO]

Universität Bremen - Computer Architecture

Incremental Generator usage

• Incrementally add new constraints

12

[LOGO]

Universität Bremen - Computer Architecture

Incremental Generator usage

• Incrementally add new constraints
• Previous constraints stay valid

12

U

Universität Bremen - Computer Architecture

Incremental Generator usage

• Incrementally add new constraints
• Previous constraints stay valid
• Trigger specific behavior after generic behavior executed

randv x,y; Generator gen; gen(x != y) for (int i =0 ; i < n; ++i) { gen.next(); run_test(x,y); }

gen( x*x == y ); for (...) { gen.next(); run_test(x,y) ; }

gen( y%2 == 0 ); for (...) { gen.next(); run_test(x,y) ; }

12

[LOGO]

Universität Bremen - Computer Architecture

Parallel Constraint Solving

• SCV: Limits in constraint complexity due to BDD-based constraint-solving

13

[LOGO]

Universität Bremen - Computer Architecture

Parallel Constraint Solving

• SCV: Limits in constraint complexity due to BDD-based constraint-solving
• Alternatives: SAT/SMT

13

[LOGO]

Universität Bremen - Computer Architecture

Parallel Constraint Solving

• SCV: Limits in constraint complexity due to BDD-based constraint-solving
• Alternatives: SAT/SMT
• But: BDD guarantees uniform distribution, hard for SAT/SMT

13

[LOGO]

Universität Bremen - Computer Architecture

Parallel Constraint Solving

• SCV: Limits in constraint complexity due to BDD-based constraint-solving
• Alternatives: SAT/SMT
• But: BDD guarantees uniform distribution, hard for SAT/SMT
• Here: Portfolio approach

13

U

Universität Bremen - Computer Architecture

Parallel Constraint Solving

• SCV: Limits in constraint complexity due to BDD-based constraint-solving

• Alternatives: SAT/SMT

• But: BDD guarantees uniform distribution, hard for SAT/SMT

• Here: Portfolio approach

• Multi-threaded

• SMT provides fast solutions

• BDD provides uniform distribution

• use BDD once created

13

[LOGO]

Universität Bremen - Computer Architecture

Parallel Constraint Solving (2)

• Comparison to SCV
• Focus: How fast can the solutions be generated?
• Example: Constraint inputs of ALU such that output is computed w/o overflow or divide-by-zero exceptions

14

U

Universität Bremen - Computer Architecture

Parallel Constraint Solving (2)

• Comparison to SCV
• Focus: How fast can the solutions be generated?
• Example: Constraint inputs of ALU such that output is computed w/o overflow or divide-by-zero exceptions

randv< sc_bv<2> > op; randv< sc_uint<16> > a; randv< sc_uint<16> > b;

constraint( op() != 0 || 65535 >= a() + b() );

constraint( op() != 1 || (65535 >= a() - b() && b() <= a() ) );

constraint( op() != 2 || 65535 >= a() * b() );

constraint( op() != 3 || b() != 0 );

14

U

Universität Bremen - Computer Architecture

Parallel Constraint Solving (2)

• Comparison to SCV

• Focus: How fast can the solutions be generated?

• Example: Constraint inputs of ALU such that output is computed w/o overflow or divide-by-zero exceptions

• run-time in sections for first/all stimuli

• SCV 1.0e 32 bit vs. new approach

tbl-0.md

14

[LOGO]

Universität Bremen - Computer Architecture

Summary and Future Work

• Advanced Constraint Random Verification Environment
• Natural C++ Syntax, easy to use API
• Dynamic constraints/constraint management
• Parallel constraint solving with advanced decision engines

15

[LOGO]

Universität Bremen - Computer Architecture

Summary and Future Work

• Advanced Constraint Random Verification Environment
• Natural C++ Syntax, easy to use API
• Dynamic constraints/constraint management
• Parallel constraint solving with advanced decision engines
• Extended support for dynamic data structures
• SMT distribution quality
• Automated constraint debugging

15

[LOGO]

Universität Bremen - Computer Architecture

Summary and Future Work

• Advanced Constraint Random Verification Environment

• Natural C++ Syntax, easy to use API

• Dynamic constraints/constraint management

• Parallel constraint solving with advanced decision engines

• Extended support for dynamic data structures

• SMT distribution quality

• Automated constraint debugging

Thank you for your attention.

15

U

Universität Bremen - Computer Architecture

References I

[1] OSCI, “SystemC,” 2011, available at http://www.systemc.org.

[2] IEEE Standard SystemC Language Reference Manual, IEEE Std. 1666, 2005.

[3] J. Yuan, C. Pixley, and A. Aziz, Constraint-based Verification. Springer, 2006.

[4] SystemC Verification Standard Specification Version 1.0e, SystemC Verification Working Group, http://www.systemc.org, 2003.

[5] J. Rose and S. Swan, SCV Randomization Version 1.0, 2003.

[6] C. N. Ip and S. Swan, “A tutorial introduction on the new SystemC verification standard,” www.systemc.org, White Paper, 2003.

[7] F. Haedicke, S. Frehse, G. Fey, D. Große, and R. Drechsler, “metaSMT: Focus on your application not on solver integration,” in DIFTS’11: 1st International workshop on design and implementation of formal tools and systems, 2011.

[8] D. Große and R. Drechsler, Quality-Driven SystemC Design. Springer, 2010.

[9] D. Große, R. Ebendt, and R. Drechsler, “Improvements for constraint solving in the SystemC verification library,” in ACM Great Lakes Symposium on VLSI, 2007, pp. 493–496.

16

[LOGO]

Universität Bremen - Computer Architecture

References II

[10] D. Große, R. Wille, R. Siegmund, and R. Drechsler, “Debugging contradictory constraints in constraint-based random simulation,” in Languages for Embedded Systems and their Applications: Selected Contributions on Specification, Design, and Verification from FDL’08, M. Radetzki, Ed. Springer, 2009, pp. 273–290.

[11] R. Wille, D. Große, F. Haedicke, and R. Drechsler, “SMT-based stimuli generation in the SystemC verification library,” in Advances in Design Methods from Modeling Languages for Embedded Systems and SoC’s: Selected Contributions on Specification, Design, and Verification from FDL 2009, D. Borrione, Ed. Springer, 2010, pp. 227–244.

17