GCSP (Graph-Based Constraint Satisfaction Problem)
GCSP is a framework for solving constraint satisfaction problems in which the assignment of constraints to variables depends on a path through a directed graph. It was developed to support constraint-based test generation for the complex address translation mechanisms that exist in modern microprocessor memory management units (MMUs).
Motivation
The hardware address translation mechanism is an essential part of modern microprocessor memory management. The demand for high performance and low power in integrated circuits makes this mechanism exceptionally complex, and its verification requires sophisticated test generation tools. Constraint satisfaction provides a natural way to generate stimuli for testing address translation, but the underlying process has structure (a sequence of translation steps) that plain CSP does not capture.
Model
The address translation process passes through a sequence of steps and can therefore be naturally described as a directed acyclic graph. A GCSP instance consists of two coupled components:
- a directed (acyclic) graph describing the structure of the process, and
- a CSP whose variables and constraints are each linked to a particular node or edge of the graph.
A solution to a GCSP is a path in the graph such that all constraints defined along that path are satisfied. This means that, in contrast to a flat CSP, the set of constraints that must hold is path-dependent: only the constraints attached to nodes and edges traversed by the selected path are activated.
Algorithm
The algorithm used to solve GCSP is based on conditional CSP. By reusing conditional-CSP machinery to selectively activate constraints conditioned on the chosen graph path, the solver avoids materialising the full Cartesian product of translation paths and constraint sets, and can focus propagation on the relevant subproblem for each candidate path.
Application: MMU verification
The framework has been used to verify the memory management units of several industrial microprocessors. In this setting, the graph encodes the possible sequences of address-translation steps exercised by the hardware, the CSP variables describe microarchitectural state and translation parameters, and the path-conditioned constraints encode the correctness conditions that must hold along the path. Solving the GCSP yields concrete stimuli for testing address translation.
RelatedEntities
- CSP — GCSP extends / is built on top of CSP; each node and edge of the GCSP graph carries CSP variables and constraints.
- Conditional CSP — the algorithmic basis onto which GCSP's path-conditioned constraint activation is mapped.
- MMU verification — the principal application domain in which GCSP has been deployed.