Overview
Constraint solving is the task of determining values for the variables of a constraint system that satisfy all stated constraints, or proving that no such assignment exists. The evidence describes constraint solving as a key supporting technology for symbolic execution (DeepSover, 2020), a central mechanism inside template-driven architecture verification generators (AVPGEN, 1995; STCS, 2003), the engine used by compliance test generation tools to instantiate symbolic specifications (Herdt et al., 2020), and the back-end that turns a symbolic ASL encoding into a concrete ARM instruction stream (Examiner, 2022).
Constraint solving in symbolic execution
In symbolic execution, constraint solving is identified as the key supporting technology that determines the effectiveness of the analysis, because every explored path requires solving the accumulated path condition to determine feasibility and to produce concrete inputs. Prior work has tried to speed this up by reusing previously computed constraint solutions, but reuse techniques such as Green and GreenTrie require syntactic/semantic equivalence or implication relationships between constraints, limiting their applicability. The DeepSover approach trains a deep neural network on the collective knowledge of a set of constraint solutions and uses it to classify the satisfiability of path conditions during symbolic execution; the authors report high classification accuracy and better efficiency than state-of-the-art constraint solving and constraint-solution-reuse techniques.
Constraint solving in template-driven architecture verification (AVPGEN)
AVPGEN is a test generator for verifying that processor designs conform to their specified architecture. Rather than making biased random choices and propagating them forward, AVPGEN frequently chooses intermediate or final values first and then solves for the initial values that lead to the desired values. The user specifies instruction templates and symbolic constraints in a language called SIGL (Symbolic Instruction Graph Language), and the combination of user-specified constraints and biasing functions is then used to focus the generated tests on conditions that are likely to activate bugs. AVPGEN has been used to debug many S/390 processors and is described as an integral part of the design process for these processors.
Constraint solving in RISC-V compliance test generation
Mutation-based RISC-V compliance testing relies on a symbolic execution framework that emits constraint-solving queries to drive the test generator. Specifically, the cited approach uses constraint solving to instantiate symbolic expressions so that mutated values are concretely realized in generated test programs, extending an earlier test-suite specification mechanism that itself leverages constraint solving to generate a compliance test suite from specification rules covering register and immediate value ranges. The symbolic execution framework is also proposed as a vehicle for difference-based testing between RISC-V simulators.
Constraint solving in ARM instruction generation (Examiner)
Examiner generates ARM instruction streams by combining a syntax-aware mutation step with a semantics-aware constraint-solving step. After producing syntactically correct instruction encodings by mutating non-constant fields (register indices, immediates, condition codes), the tool parses the ARM Architecture Specification Language (ASL) code for each instruction, extracts the constraints that influence the execution path, and feeds them to an SMT solver to find concrete values of the encoding symbols that satisfy each constraint and its negation. For example, when an immediate-field constraint such as d4 > 31 is encountered, Examiner performs backward symbolic execution through the ASL statements that define d4 (e.g., d4 = d3 + inc) and converts the constraint into one over the ultimately underlying symbols (UInt(D:Vd) + 3 × inc > 31). Because the decoding and execution ASL code has limited constraints and utility functions are modelled, path explosion is not a practical issue, and all test cases can be generated within minutes.
Dedicated hardware-aware constraint solving (STCS)
When general-purpose constraint solvers such as GNU Prolog are applied to hardware-description-level test generation, several shortcomings appear: bit-typed variables require casting that loses information, bit-manipulation constraints such as extraction (X = Y[5:3]) and concatenation (X = (Y:Z)) cannot be combined with arithmetic constraints on the same variable, and natural-only variable domains exclude signed values. To address these, the STCS solver introduces new specific constraints — logical AND, logical shift, bit concatenation, and bit extraction — and maintains two internal domain representations per variable: an interval (min, max) for arithmetic constraints and a known-bit representation for bit-based constraints. Interval changes propagate into the bit representation (high bits from min/max), and bit changes recompute the interval, keeping the two views coherent. STCS is described as a general library that, while developed for microprocessor test generation, is not limited to that domain.
Constraint solving in instruction-generation performance
Constraint solving is one of the largest runtime consumers in randomized instruction generation. In RISCV-DV profiling, two of the four largest runtime bottlenecks — directed instruction stream generation and non-directed instruction stream dumping — spent most of their time executing constraint solvers or solving constraints. Both of these bottlenecks were classified as linear in algorithmic complexity and as scaling well with multicore parallelization. Separate bottlenecks of O(n²) directed-stream insertion complexity and string formatting dominated by repeated memory allocation were not themselves characterized as constraint-solving bottlenecks.
Solver strategies in eUVM
eUVM, an open-source, multicore-enabled implementation of UVM in the D programming language, deploys a hierarchy of solver strategies depending on constraint complexity: a native constraint solver for elementary single-domain constraints, BDD-based solvers for multi-domain constraints of medium complexity, and SMT/SAT solvers (including Z3, Boolector, and CMSGen) for the most complex constraints that BDD cannot handle. D language metaprogramming features (User-Defined Attributes, Compile-Time Function Evaluation, code introspection, and generative programming) are used to implement a high-performance constraint processor, with compile-time parsing and analysis of constraints enabled by code introspection and CTFE.
Other constrained-randomization environments
Pygen, the Python port of RISCV-DV, uses PyVSC for solving constraints. PyVSC does not deploy a BDD solver and relies completely on SAT solvers for multi-variable constraints; the cited report indicates poor runtime performance, generating fewer than one hundred random RISC-V instructions per second. The SystemC UVM port instead relies on the CRAVE library for constrained randomization, which provides an integrated BDD/SAT interface; the cited evidence states that CRAVE could not handle complex RISCV-DV constraints at the time described and did not support multicore parallelism.
Constraint solving over nominal abstract syntax
Outside hardware verification, constraint solving is also the standard algorithmic tool for nominal unification and related problems over nominal abstract syntax. The Urban–Pitts–Gabbay nominal unification algorithm handles the most common cases, while Cheney's equivariant unification algorithm respects the equivariance property of nominal logic and is more powerful but more complicated and computationally hard. A subsequent line of work presents a constraint-solving algorithm for non-permutative nominal abstract syntax that attains similar complexity to equivariant unification while avoiding many of the additional complications of the equivariant term language, including an explicit translation from name–name equivariant unification problems into non-permutative constraints.