Overview

Constraint solving in the cited literature is the task of finding values for variables that satisfy stated constraints over their domains. In the STCS work, the constraint system is drawn from a hardware-description-derived language that includes fixed-width typed variables, bit-level operations such as extraction and concatenation, signed values, and array manipulations; constraints may also involve casting operations that can lose information across bit widths. [C1]

Core solving model

In the classical finite-domain model described by the STCS work, solving proceeds in two main stages. First, a propagation phase reduces variable domains, typically using arc-consistency techniques. Second, a labeling phase grounds variables by iteratively fixing values and re-propagating the consequences through the same arc-consistency machinery. The labeling phase can be improved by heuristics on the order in which variables are considered and the order in which values are tried within a variable's domain. [C2]

Specialized hardware-oriented solving: STCS

A major use case in the evidence is hardware test generation. The cited authors note that the existing GNU Prolog solver, which they initially considered, was not sufficient for this setting. They list four categories of constraint that GNU Prolog handled poorly:

• fixed-width typed variables, where casting between widths can lose information (for example, with 8-bit unsigned Y, Z > 0 and 9-bit unsigned X, the constraint X = Y + Z forces X ≥ 2, but an 8-bit unsigned T equal to the cast of X can take value 0 or 1 because the ninth bit of X is dropped);
• signed integer variables, which GNU Prolog did not natively support (it handled naturals only);
• bit-manipulation constraints, such as bit extraction X = Y[5:3] and bit concatenation X = (Y : Z);
• array manipulations, where naively expanding an array into individual variables creates too many variables for memory-sized arrays.

The cited alternative of treating variables as bit vectors with constraints on individual bits could not be combined with arithmetic constraints on the same variable, preventing further domain reductions. [C3]

To address this, the authors developed a dedicated constraint solver named STCS, built with the experience of GNU Prolog but introducing new specific constraints: logical and (X Eq Y and Z), logical shift (X Eq Y slr C), bit concatenation (X Eq Y concat Z), and bit extraction (X Eq Y extract C), with X, Y, Z variables and C a constant. [C4]

STCS keeps two internal representations of each variable's domain:

• an interval representation (min value, max value) used for arithmetic constraints;
• a bit representation recording which bits of the variable's bit-vector are known, used for bit-based constraints.

Propagation is split into interval propagation and bit propagation, and the two representations are kept coherent by two rules:

• on every interval modification, the bit representation is updated by propagating the most significant bits — 1 from the min value and 0 from the max value;
• on every bit modification, a new min/max interval is recomputed from the known bits. [C5]

The paper also states that STCS was developed as a general library rather than something limited to microprocessor test generation, and is intended to be reusable in other domains or applications. The cited case study uses STCS through the STTVC test generation tool on a commercial ST STM7 micro-controller. [C5]

Use in Theo

Theo is a sophisticated code generator used in the functional verification of high-performance microprocessors. In the cited paper, it is described as one of a set of code generation methods — alongside heuristic algorithms, user-provided templates, and pseudo-random selection — used to produce interesting test cases for the RTL model. [C6]

In Theo, the verification engineer writes templates that define sequences of instructions representing "constraints" on the microprocessor, using symbolic notation for instruction classes, registers, and operands. Theo's engine then uses a constraint solving engine to produce an Intermediate Code Representation (ICR) by repeatedly applying these templates. After the ICR is built, Theo performs instruction assignment, global resource allocation, and condition setup, consulting managers such as the register allocation manager, the address manager, the branch manager, the operand manager, and the external event manager, before translating the ICR into assembly code ready for simulation. [C7]

Theo's template placement algorithm explicitly uses constraint solving. Rather than placing templates one after the other, it tries to achieve overlap between templates while maintaining each template's requirements. To check whether an overlap is possible, the algorithm checks subset properties, runs constraint solving, and applies temporary unification; if all resource requirements are met, the unification is made permanent. Successive application of templates to the ICR refines and grows the code. The paper notes that this approach can create new test sequences from previously independent blocks, activating multiple units of the microprocessor simultaneously while still maintaining the sequence and conditions represented by each template. [C8]

The use of symbolic notation in templates allows Theo to select the actual assembly instructions and operands using sophisticated heuristic algorithms, and lets the verification engineer express conditions of interest in the most generic way. A typical hand-written diagnostic stresses a particular unit while leaving the rest idle; Theo instead combines templates so that all units of the microprocessor are active simultaneously. [C7]