Using Graph-Based CSP to Solve the Address Translation Problem

The hardware address translation mechanism is an essential part of modern microprocessor memory management. The ever-growing demand for performance and low power of integrated circuits makes this mechanism exceptionally complex, and its verification requires sophisticated test generation tools. This paper presents a solution, based on constraint satisfaction, to generate stimuli for testing address translation.

The address translation process passes through a sequence of steps and can therefore be naturally described as a directed acyclic graph. We developed a framework that we call graph-based constraint satisfaction problems (GCSP). These problems consist of a directed graph, combined with a CSP, where each variable and constraint of the CSP is linked to a particular node or edge of the graph. A solution to the problem is a path in the graph, such that all constraints defined along this path must be satisfied. We base our algorithm for solving GCSPs on conditional CSP. We successfully used this technology to verify the memory management units of several industrial microprocessors.