Fixed-point characterizations of constraint satisfaction problems and their use in performance verification of VLSI systems

Current methods for solving a constraint satisfaction problem (CSP) are insufficient when a number of difficult conditions all hold true. CSPs are unsolvable in general, so this leaves little hope for solving CSPs where these methods do not work. This thesis presents an unsolvable class of CSPs, along with a method for determining if individual CSPs in this class may or may not be satisfiable, and ultimately for reducing the domain space to a subdomain where all solutions (if any) must lie.; This method is based upon fixed-point theory. Given a CSP, its constraints are characterized as a functional [Y] which maps a domain space to a subset of itself. Any set of points which maps to itself (a fixed point) cannot be reduced by any constraint; the greatest of these sets (the greatest fixed point) is a superset of the solution space to the CSP. Through this, fixed-point characterizations of CSPs are used to comment on CSP satisfiability. If the greatest fixed point is empty, it follows that the solution space is empty, and that the CSP is unsatisfiable. If the greatest fixed point is not empty, then the solution space may or may not be empty.; The domain space is represented using interval notation, and the constraint propagation methods are implemented using interval mathematics. Problems involving the nontransitivity of extended interval mathematics are avoided through the introduction of “colored” intervals. Although other problems with interval mathematics prevent the calculation of the greatest fixed point itself, these methods can calculate a superset of it; the emptiness or non-emptiness of the greatest fixed point can be determined from this superset. This is sufficient to comment on the satisfiability of the original CSP. A number of satisfiability algorithms are presented, along with corresponding proofs of correctness.; Given a CSP which may be satisfiable, an iterative variant of these methods can be used in hopes of producing a solution. Thus, these methods can solve some CSPs in a class which would be considered impossible to solve using other methods.; The performance verification problem is presented as an application of these methods. This problem can be stated as: “Given a VLSI design and desired performance goals, can the design satisfy all the goals simultaneously?” The use of performance description languages allows a VLSI designer to specify rules to evaluate the performance (nonfunctional attributes) of a VLSI design; these attributes and rules can be represented as a CSP, upon which the performance goals can be asserted. If the CSP is unsatisfiable, The performance model can meet all performance goals if and only if the resulting CSP is satisfiable.