Stochastic Approach to CSP’s in the Hardware
Verification Domain
Yehuda Naveh
Simulation Based Methods, Systems and Modeling
IBM Labs in Haifa
© Copyright IBM
IBM Labs in Haifa
Constraints in test case generation
Verification task:
Real address in some corner memory space,
Effective address aligned to 64K.
Testing knowledge:
Reuse cache row.
Architecture:
Effective address translates into real address in a complex
way.
EA: 0x????????_????0000
0x????????_????????
0x0B274FAB_0DBC0000
0x????????_????????
RA: 0x0002FF??_????????
0x0002FF??_??A4D???
0x0002FFC5_90A4D000
Huge Domains (264)
Quality of solution: Random uniformity
EA: 0x0002FF00_00000000
RA: 0x0002FF00_00000000
Correct, but worthless!
2
Simulation Based Methods, Systems and Modeling
© Copyright IBM
IBM Labs in Haifa
Deterministic Methods (DPLL, MAC, k-consistency, …)
User: Aligned EA
User: Special RA’s
X
RA
EA
X
EA-RA Translation
1. Reach a level of consistency through successive reductions of sets
2. Choose a random assignment for a variable, and maintain the consistency
3
Simulation Based Methods, Systems and Modeling
© Copyright IBM
IBM Labs in Haifa
Limitations of Deterministic Methods: An example
a, b, c
0,..., N , N
1. a
0
b 0
2. a
0
c
0
3. b 0
c
0
4. c
a 1
0
264
Only solution:
a 1, b
c
0
Local consistency at onset: Choose randomly with probability 1/N of being correct
(Solution reached at 600 million years)
4
Simulation Based Methods, Systems and Modeling
© Copyright IBM
IBM Labs in Haifa
Limitations of Deterministic Methods: Another example
a, b, c
0,..., N , N
264
1. a * b c
2. a, b, c each have five 1' s in their binary representation
Already a single reduction of domains is hard
5
Simulation Based Methods, Systems and Modeling
© Copyright IBM
IBM Labs in Haifa
Stochastic approaches: defining the metrics
State: a tuple representing a single assignment to each variable
+
Cost: A function from the set of states to {0} U R
Cost = 0 iff all constraints are satisfied by the state.
a *b c
a
6
0
Cost (c a * b) 2
b 0 Cost
Simulation Based Methods, Systems and Modeling
b a
0 a
0
0
© Copyright IBM
ERROR: undefined
OFFENDING COMMAND: w
STACK:
1.2