Using Constraint Satisfaction
Formulation and Solution Techniques
for Random Test Program Generation
Roy Emek
12-Sep-2002
IBM Research Lab in Haifa
Outline
Random
test program generation
H
R
Constraint
Satisfaction Problems (CSP)
L
Modeling
test programs as CSP
CSP for random test generation:
characteristics
Solution building blocks
[ Based on a paper by E. Bin,
R. Emek, G. Shurek and A. Ziv ]
Verification Through Simulation
H
R
Test
L program:
Instructions
Resource
initializations
Architecture
Simulator
Expected
behavior
?
Design
Simulator
Actual
behavior
Random Test Program Generator
H
R
System model:
What's valid
What's interesting
L
User
requirements
Generate N
tests
Random Test
Generator
N distinct tests
Valid, Interesting
Satisfy user requirements
Test Program Constraints
Test quality: sum
H overflow
R
L
add R1 b R2 + R3
load Rx b 1000(Ry)
???? ??, Rz
mult Rz b R6 % R7
Validity: x ! y
User request: same register
CSP Definition
[ Mackworth, Freuder, Montanari, Dechter, Rossi, ...]
H
Variables of the problem
R
L
address, register_value
Domain (set) for each variable
address: 0x0000 - 0xFFFF
number of bytes in a 'load': { 1, 2, 4, 8, 16 }
Constraints (relations) over variables
(load n bytes) u (align address to n bytes
boundary)
value(base_reg) + displacement = address
CSP Definition (cont)
Solution for a CSP
H
Every variable is assigned a value from its domain
R
The assignments satisfy all the constraints
L
Example
Variables: a, b, c
Domains:
A = {1,2,3} ; B = {2,3,4,5} ; C = {1,3,5}
Constraints:
a2 < b ; c g b
; a<c-1
Solution:
a=1; b=4
; c=3
Random Test Program Generator (2)
H
R
System model:
What's valid
What's interesting
L
User
Requirements
Generate N
tests
A Constraint
Satisfaction
Problem
Random Test Generator
(CSP solver)
N distinct tests (solutions)
Valid, Interesting
Satisfy user requirements
CSP@RTG Characteristics
Random,
uniform distribution solution
H
[Yuan
et al. '99, Dechter et al. '02]
R
As opposed to one, all, or 'best' solution
Huge domains: 264 and more
L
Example: address space
Representing and operating on large sets becomes an
issue
Hierarchy of constraints [Borning et al., '87]
Mandatory: test case validity
Non-mandatory: makes the test 'interesting'
And we want it fast ...
H
R
L
Solution Algorithm:
Consistency - A Single Constraint
H
R
L
X
Y
Z
{1, 2, 3} {1, 2, 3} {1, 2, 3}
R: (x,y,z) c X%Y%Z, x=y+z
{1, 2, 3} {1, 2, 3} {1, 2, 3}
Solution Algorithm:
Maintaining Arc Consistency (MAC)
[ Mackworth, 1977 ]
H
Arc = C
on
The process: reducing domains to
R
single-values
L
1. Make
all constraints locally consistent
Some constraints are handled repeatedly
Achieve fixed-point
2. Choose a variable: address
3. Choose a value: address b 0x1234
0x1234 c domain ( address )
4. Go to step 1
5. On failure - backtrack
Failure results in an empty set / domain
straint
Consistency as Projection
H
R
L
C
1
C
C
B'
B
B
2
B
A
A
A
A'
3
Formula Based Constraint Projector
MAC scheme – projectors for constraints
Developing
arithmetic / logical / bit-wise projectors time
H
after
R time again ?
a=b+c, a+b=c+d, a + b = c bit-xor d, ...
L
Error prone, labour intensive
C
Constraint (formula)
a=b+c1a
Reduced output
sets:
Input sets:
A'
A
B
C
Projector
B'
C'
Example: Projecting Disjoint Constraints
Constraint: (a=b) - (b=a+c) - (c=3$a)
H
Domains: A={1,2,3}; B={3,4,5};C={4,5}
R
(1)L Project sub-constraints separately
(2) Join* sub-constraints projections
Input
domain
a=b
b=a+c
c=3a
Results
A
{1,2,3}
B
{3,4,5}
C
{4,5}
{3}
{1}
!
{1,3}
{3}
{5}
!{3,5}
{4,5}
{4}
!
{4,5}
Domain (Set) Representation Example: bit-vectors
Origin of the challenge: large H/W resources
H
128-bit registers
R
64-bit wide memory address space
L
All the addresses such that
addr = base + displacement
// architectural
addr[3:6] = 01?1
// cache line
addr c [0x2000 : 0x10FFF]
// memory space
'Masks' (DNF) representation:
01?1 d 0101, 0111
Problem: Exponential Explosion
01010101 + 0?0?0?0? d
H
{10101010, 01101010, 10011010, 01011010,
R
10100110, 01100110, ..., 10010101}
L
The general case: a + b d 2(n/2) clauses
Coping with the problem
Binary Decision Diagrams (BDDs)
Sometimes: space explosion
Approximations
We only have partial solutions
Summary
Viewing test generation as CSP
Characteristics:
random, huge domains
H
Solution
scheme
R
L Consistency based
HRL's test generators are CSP based
The basis for test generators for all the processors
designed in IBM
Using Constraint Satisfaction
Formulation and Solution Techniques
for Random Test Program Generation
End of Presentation
12-Sep-02
IBM Research Lab in Haifa
Floating Point Operations – Stochastic Approach
a$$2✍ op b$$2✎ = c$$2✏
H op: +, -, $, ...
R Limited number of bits:
L
non-continuous domain, rounding
Constraints:
'op' itself
bit #n = '0'
Number of '1's = m
a c [a1 ... a2]
mantissa:53
exp:11
mantissa:53
exp:11
mantissa:53
exp:11
op
Stochastic solution scheme:
assign random 64 % 3 bits
Hill-climbing
Simple heuristics
Local maximum: flip random bits
After some time - give up and start all over again
Instruction Constraints
Modelling a PowerPC instruction
Instruction
H
R
Load DS(RA) → RT
Operands
L
=
+
Memory
Address
Register
Operands
Register
Address
Data
Format
Immediate
Data
Problem Partition, Dynamic Modeling
H Partitioning the problem
R
L
Easier to model, easier to solve
Hard to handle interdependencies
Dynamic problem structure
?
CSP Definition
[ Mackworth, Freuder, Montanari, Dechter, Rossi, ...]
H
Variables of the problem
R
address, register_value
L
Domain (set) for each variable
address: 0x0000 - 0xFFFF
number of bytes in a 'load': { 1, 2, 4, 8, 16 }
Constraints (relations) over variables
(load n bytes) u (align address to n bytes boundary)
value(base_reg) + displacement = address
last_instruction = "branch" ?
yes: PC = branch-target
no : PC = increase (last_instruction_address)