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.

翻译：功能验证在确保现代集成电路设计正确性方面发挥着核心作用，其中受约束随机验证被广泛采用，以在高层次约束下生成多样化的激励。在工业验证环境中，约束求解越来越多地涉及动态数据结构，这些数据结构的形状和内容在运行时确定，导致变量集和约束实例随求解器调用而演化。当嵌套和高维结构在多次求解中反复扩展时，这进而导致大量开销。我们将此类问题形式化为动态数据结构约束满足问题（D2SCSP），该问题捕捉了动态数据结构扩展与约束评估之间的交互。我们提出了一种依赖引导的问题划分框架，结合增量编码和约束激活机制，使得求解器状态和编码能够在多次求解间复用。该框架集成到工业级SystemVerilog验证流程中，并在商业仿真器VeriSim中实现。在工业基准测试上的实验结果表明，性能显著提升，相比基线实现了平均24.80倍的加速，相比最先进的商业仿真器实现了1.72倍的加速，突显了该方法在实际验证工作流程中的实用性。