Efficient Solving for Dynamic Data Structure Constraint Satisfaction Problem

TL;DR

This paper introduces a new approach to efficiently solve dynamic data structure constraint satisfaction problems in industrial circuit verification, significantly reducing runtime overhead.

Contribution

It formalizes D2SCSP and proposes a dependency-guided partitioning framework with incremental encoding, enabling reuse of solver states across multiple solves.

Findings

Achieves an average speedup of 24.80x over baseline methods.

Outperforms a state-of-the-art commercial simulator by 1.72x.

Successfully integrated into an industrial verification flow.

Abstract

Functional verification plays a central role in ensuring the correctness of modern integrated circuit designs, where constrained-random verification is widely adopted to generate diverse stimuli under high-level constraints. In industrial verification environments, constraint solving increasingly involves dynamic data structures whose shape and content are determined at runtime, causing the sets of variables and constraint instances to evolve across solver invocations, which in turn leads to substantial overhead when nested and high-dimensional structures repeatedly expand across solves. We formalize this class of problems as the Dynamic Data Structure Constraint Satisfaction Problem (D2SCSP),which captures the interaction between dynamic data structure expansion and constraint evaluation. We propose a dependency-guided problem partitioning framework combined with an incremental encoding and constraint activation mechanism, enabling reuse of solver state and encodings across multiple solves. The framework is integrated into an industrial SystemVerilog verification flow and implemented in the commercial simulator VeriSim. Experimental results on industrial benchmarks demonstrate significant performance improvements, achieving an average speedup of 24.80x over a baseline and 1.72x over a state-of-the-art commercial simulator, highlighting the practicality of the approach for real-world verification workflows.