IBM Labs in Haifa Generation Core: IBM's Systematic Constraint Solver IBM Haifa Labs Outline Introduction to constraint satisfaction problems (CSP) Constraint satisfaction at IBM Haifa Solving approaches Generation Core (GEC): IBM’s systematic CSP solver Special features – Large domains – Specialized propagators – Random solutions – Hierarchical soft constraints – Conditional sub-problems 2 © 2008 IBM Corporation IBM Haifa Labs A CSP consists of: A set of Variables v1, v2, ..., vn A finite domain for each variable: for each vi, vi є Di Constraints A set of relations between the variables 3 © 2008 IBM Corporation IBM Haifa Labs The round-table problem King Arthur would like to seat all his knights around the round table Each knight must sit between two knights he knows Lancelot knows Galahad Ector knows Kay Percival knows Lancelot Gareth knows Gawain Gareth knows Lionel Galahad knows Percival Pellinore knows Kay ... 4 © 2008 IBM Corporation IBM Haifa Labs Solution for a CSP Every variable is assigned a value from its domain, such that all constraints are satisfied All solutions are created equal 5 © 2008 IBM Corporation IBM Haifa Labs Constraint satisfaction at IBM Haifa Research Labs Two state-of-the-art solving engines – systematic and stochastic Major application: test generation for hardware verification Other applications – Workforce management – Truck configuration – Floor planning 6 © 2008 IBM Corporation IBM Haifa Labs Generation Core (GEC) IBM’s systematic CSP engine On a par with leading tools in the industry (ILOG, SICStus) Generic Dozens of engineers involved in development, modeling, and applications of CSP 15 years of development experience Research activity 7 © 2008 IBM Corporation IBM Haifa Labs GEC solution algorithm Systematic approach Based on Maintain Arc Consistency (MAC) [Mackworth 1977] MAC Instantiation MAC Instantiation backtrack MAC Instantiation MAC 8 © 2008 IBM Corporation IBM Haifa Labs MAC Example R1: {(x,y,z): x=y+z} X: {1,2,3} Y: {1,2,3} Z: {1,2,3} X: {1,2,3} Y: {1,2,3} Z: {1,2,3} X: {1,2,3} Y: {1,2,3} Z: {1,2,3} instantiation X: {1,2,3} Y: {1,2,3} Z: {1,2,3} AC X: {1,2,3} Y: {1,2,3} Z: {1,2,3} AC AC R2: {(y,z): ygz} Don’t give up yet 9 © 2008 IBM Corporation IBM Haifa Labs MAC example - backtracking R1: {(x,y,z): x=y+z} R2: {(y,z): ygz} 10 X: {1,2,3} Y: {1,2,3} Z: {1,2,3} X: {1,2,3} Y: {1,2,3} Z: {1,2,3} X: {1,2,3} Y: {1,2,3} Z: {1,2,3} instantiation X: {1,2,3} Y: {1,2,3} Z: {1,2,3} instantiation X: {1,2,3} Y: {1,2,3} Z: {1,2,3} AC © 2008 IBM Corporation IBM Haifa Labs GEC algorithm summary Repeat until all variables are reduced to a single value or failure occurs Make all constraints locally consistent Through reducing the variable domains Iteratively until a fixed-point is achieved Backtrack if a domain is reduced to an empty set If backtracking is exhausted problem is unsolvable Choose a variable (which was not yet assigned) Choose a soft constraint and activate it Choose and assign a value for the selected variable 11 © 2008 IBM Corporation IBM Haifa Labs Main Application: Simulation-Based Functional Verification of Processors Stimuli Generator 12 Stimuli (test-cases) Functional Specification Design Simulator Expected Behavior Actual Behavior © 2008 IBM Corporation IBM Haifa Labs How GEC fits into the test generation process Expert knowledge defining corner cases Architecture specification Model Stimuli Generator Constraint solver GEC constraint solver Stimuli (test-cases) Used to verify all PowerPC designs in IBM over the last seven years : i/p series servers, Cell, Xbox™ 13 © 2008 IBM Corporation IBM Haifa Labs Example of constraints Quality: sum zero add R1 R2 , R3 load Rx 1000 (Ry) ???? ?? Rz mult Rz ?? , ?? Validity: x != y Input scenario: same register 14 © 2008 IBM Corporation IBM Haifa Labs Special features: Large number domains Represented as masks: 0X0X = {0000, 0100, 0001, 0101} Length of numbers often 64 or 128 bits long Domains can have sizes of 264 15 © 2008 IBM Corporation IBM Haifa Labs Special Features: Specialized propagators For arithmetic operations: +, *, /, ... For logical expressions: and, or, implies, ... For bit operations: shift, rotate, concatenate, ... Rich expression language to represent constraints But users also have the option of defining their own propagators in C++ code! 16 © 2008 IBM Corporation IBM Haifa Labs Special Features: Random Solutions Every operation of the solver on a given problem produces a different solution Strive toward uniformity of solutions (sometimes difficult) Guarantee not to ‘lose’ solutions Essential for testing because of unpredictability of bugs All solutions are created equal User preferences allowed by Allowing hierarchy of soft constraints Value ordering Variable ordering 17 © 2008 IBM Corporation IBM Haifa Labs Special Features: Conditional Sub-problems Existence variables control the existence of certain sub-problems {true,false} false 18 © 2008 IBM Corporation IBM Haifa Labs Summary CSP is a dynamic field used to solve ‘hard’ problems (non-polynomial, non-linear) Haifa Research Labs have a large group working on research and development in CSP Haifa CSP tools are already in usage as a critical link in the chain of processor development Also used in other applications within and outside of IBM 19 © 2008 IBM Corporation

1/--страниц