CSP at Haifa Research Lab

All four major testcase generators developed at Haifa utilize advanced CSP techniques as their basic technology. They differ in the domain for which they create tests, and hence in the number and types of constraints they are required to satisfy:

• FPGen creates tests for the verification of the floating-point unit of processors. Typically, it solves problems consisting of a small number of variables and constraints, but performing projection by some of the constraints is computationally hard. The constraints fall into two main categories:
  1. Some floating-point operation between operands and result
  2. Range, mask, or count-ones unary constraints on either an operand or a result
  
  Example Problem Structure
  After specifying all values of the constants below, this is a complete real problem:
  
  

  Variables and domains
  a, b, c are each 128-bit IEEE floating point numbers.
  Note: a, b, c may be thought of as 128-bit integers, and this would not significantly change the essence of the problem.
  
  Constraints

  1. a is in the range [A, B] where A, B are given constants.
  2. b is constrained by a given constant mask M (M is a vector of length 128, with elements '1', '0', or 'X'. Element '1', '0', or 'X' in position p of M implies that bit p in the binary representation of b is 1, 0, or unconstrained, respectively).
  3. c has between Nmin and Nmax 1's in its binary representation, where Nmin and Nmax are given constants.
  4. c = a X b, where X signifies floating-point multiplication.

  
  
• Piparazzi is a generator used to create tests that lead to specific micro-architectural events at a processor. In order to enforce the cycle-accuracy necessary for tests at this level, a large number of constraints are used to model the micro-architectural states, and the transitions between them. Typical problems consist of 10^4 variables and 10^5 constraints. The latter can usually be expressed as a combination of simple arithmetic, logic, and bitwise operators.
  
  Example Problem Structure
  Only a small number of typical variables and constraints are considered:
  
  

  Variables and Domains
  a, b: 64-bit integers
  c: [0, 15]
  d: {0, 1}
  
  Constraints
  (d = 1) -> ((a > 3 * b + 5) || (a[4, 5] = c & 0x2)),
  where the mathematical and logical operators take their usual meaning, p[A, B] means the integer value equal to the bit-interval defined by positions A and B in the bit representation of p, and & signifies bitwise-and.

  
  
• Genesys-Pro is used to create tests at the processor architectural level. A typical problem here involves a large number of constraints that span a wide range of complexity, starting from simple bitwise constraints between two 64-bit integer variables, and ranging to semantically-complex relations between a number of variables. (For example, as a means to enforce the address translation requirements of the underlying hardware architecture).
  
  
  
• X-Gen is a test generator aimed at the system-level. Here, the problems are reminiscent of the problems solved by Genesys-Pro, except that several different types of components are involved, and each presents its own sub-CSP to the problem. In addition, the identity of components being tested by a given test are themselves part of the CSP. Thus, if we view the hardware system as a graph, with specific components represented by nodes and connections between components by edges, X-Gen solves a graph-based CSP. By this we mean that paths in the graph are themselves represented as CSP variables, and in addition to explicit constraints on the paths, a solution with a specific path requires that all constraints related to components at the nodes forming this path are also satisfied.