Constraint Solving

Technique

Constraint solving is a foundational technique in program analysis, verification, and test generation, in which a solver is given a set of logical or arithmetic constraints over variables and asked to find concrete values that satisfy them, or to determine that no such values exist. The evidence shows constraint solving being used as the key supporting technology for symbolic execution, for template-driven architecture verification test generation in AVPGEN, for SMT-based mutation-driven compliance testing of RISC-V, for ARM instruction-stream synthesis in Examiner, and for hardware-description-driven test generation with the dedicated STCS solver. Solver strategies range from domain-reduction constraint logic programming over bit-vectors, to BDD-based methods, to SMT solvers such as Z3, Boolector, and CMSGen, and more recently to deep-learning-augmented satisfiability classifiers.

First seen 5/25/2026

Last seen 7/13/2026

Evidence 15 chunks

Wiki v2

WIKI

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

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

8 connections

Examiner ← uses 100% 2e

Examiner uses constraint solving to find concrete values of encoding symbols that satisfy or negate ASL constraints.

semantics-aware test case generation ← uses 100% 2e

Semantics-aware test case generation uses constraint solving to find values that satisfy or negate ASL conditions.

STCS ← implements 100% 2e

STCS implements the constraint solving approach with hardware-specific constraints.

Code-based Test Generation for Validation of Functional Processor Descriptions ← uses 100% 2e

The paper uses constraint solving techniques to generate test vectors.

Constraint-based Random Simulation ← uses 98% 1e

Constraint solving is the mechanism used to generate stimuli in constraint-based random simulation.

Towards specification and testing of RISC-V ISA compliance ← uses 95% 1e

This paper leverages constraint solving techniques to generate a CT.

AVPGEN ← uses 100% 1e

AVPGEN uses constraint solving as a novel concept to generate effective tests.

riscv-dv ← uses 100% 1e

Most of the RISCV-DV generation time is spent on constraint solving.

LINKED ENTITIES

1 links

AVPGEN USES Extracted graph relationship

CITATIONS

16 sources

16 citations — click to expand

[1] AVPGEN uses symbolic execution and constraint solving along with biasing techniques to generate architecture verification programs for processor designs, choosing intermediate or final values and solving for initial values. AVPGEN—A Test Generator for Architecture Verification for IEEE Transactions on VLSI Systems - IBM Research

[2] AVPGEN uses a language called SIGL (symbolic instruction graph language) for the user to specify templates with symbolic constraints, and the combination of user-specified constraints and biasing functions focuses tests on conditions likely to activate bugs. AVPGEN—A Test Generator for Architecture Verification for IEEE Transactions on VLSI Systems - IBM Research

[3] AVPGEN has been used to debug many S/390 processors and is an integral part of the design process for these processors. AVPGEN—A Test Generator for Architecture Verification for IEEE Transactions on VLSI Systems - IBM Research

[4] A specification-based RISC-V compliance test approach leverages constraint solving techniques to generate a compliance test according to specification rules, focused on positive testing and reasoning about register and immediate values. Mutation-based Compliance Testing for RISC-V

[5] Examiner parses the encoding diagram and the ASL decoding/execution code for an ARM instruction, extracts constraints from the ASL, and feeds them to an SMT solver to find concrete values of encoding symbols that satisfy the constraints and their negations. Examiner: Automatically Locating Inconsistent Instructions between Real Devices and CPU Emulators for ARM

[6] Examiner converts a high-level constraint such as d4 > 31 into a constraint over the ultimately underlying symbols via backward symbolic execution through the ASL statements that define the symbols. Examiner: Automatically Locating Inconsistent Instructions between Real Devices and CPU Emulators for ARM

[7] Examiner models utility functions such as UInt so that symbols are not propagated into them, avoiding path explosion and allowing all test cases to be generated within minutes. Examiner: Automatically Locating Inconsistent Instructions between Real Devices and CPU Emulators for ARM

[8] The STCS solver introduces hardware-specific constraints — logical AND, logical shift, bit concatenation, and bit extraction — and maintains two coherent domain representations per variable: an interval (min, max) for arithmetic and a known-bit representation for bit-level constraints. STCS: A Dedicated Constraint Solver for Hardware Test Generation

[9] STCS was developed as a general library and is not limited to microprocessor test generation problems. STCS: A Dedicated Constraint Solver for Hardware Test Generation

[10] Constraint solving is the key supporting technology that affects the effectiveness of symbolic execution, and prior solution-reuse techniques such as Green and GreenTrie require syntactic/semantic equivalence or implication between constraints. Constraint Solving with Deep Learning for Symbolic Execution

[11] DeepSover trains a deep neural network on the collective knowledge of a set of constraint solutions and uses it to classify path conditions for satisfiability, reporting higher accuracy and better efficiency than state-of-the-art constraint solving and reuse techniques. Constraint Solving with Deep Learning for Symbolic Execution

[12] The Urban–Pitts–Gabbay nominal unification algorithm is the most commonly used constraint solving algorithm over nominal abstract syntax, and Cheney's equivariant unification respects the equivariance property of nominal logic at higher computational cost. Constraint solving in non-permutative nominal abstract syntax

[13] Constraint solving for non-permutative nominal abstract syntax has similar complexity to equivariant unification without many of the additional complications of the equivariant term language, with an explicit translation from name–name equivariant unification into non-permutative constraints. Constraint solving in non-permutative nominal abstract syntax

[14] In RISCV-DV profiling, directed instruction stream generation and non-directed instruction stream dumping spent most of their time executing constraint solvers or solving constraints, and both bottlenecks were characterized as linear in algorithmic complexity and as scaling well with multicore parallelization. Previous wiki article (Constraint Solving, v1)

[15] eUVM uses a native constraint solver for elementary single-domain constraints, BDD-based solvers for medium-complexity multi-domain constraints, and SMT/SAT solvers (Z3, Boolector, CMSGen) for the most complex constraints, with a high-performance constraint processor implemented using D metaprogramming (UDAs, CTFE, introspection, generative programming). Previous wiki article (Constraint Solving, v1)

[16] Pygen uses PyVSC for constraint solving, which lacks a BDD solver and relies entirely on SAT for multi-variable constraints, reportedly producing fewer than 100 random RISC-V instructions per second; the SystemC UVM port relies on CRAVE, which the cited evidence reports could not handle complex RISCV-DV constraints and lacked multicore parallelism at the time. Previous wiki article (Constraint Solving, v1)