Lemma Pattern Matching for SMT-based Verification of Analog Mixed-Signal Hardware

Abstract

While bounded model checking (BMC) is now standard practice for digital designs, analog/mixed-signal (AMS) hardware remains largely outside the reach of automated formal analysis. This class of problems requires heavyweight theory solvers that support nonlinear real arithmetic and ordinary differential equations (ODEs) to analyze circuit behavior and contains much more complex SAT constraints than classic hybrid systems problems as a result of digital control logic. SMT solvers supporting this theory, such as dReal, face a structural bottleneck when targeting AMS BMC problems: repetitive constraints arise across digital clock cycles and reused instantiations of modular hardware blocks. This causes the solver to frequently rediscover nearly the same theory lemmas with only the names of constants changed. We present DRPM, a domain-specific optimization that intercepts theory-solver explanations and, via free constant renaming (α-equivalence), injects a larger set of valid theory lemmas without additional theory-solver calls. The optimization is formalized within the Abstract DPLL⟨T ⟩ framework and proven sound and complete. DRPM is implemented in dReal via an efficient one-to-many pattern matching algorithm using structural hashing and discrimination trees. We evaluate DRPM on 6,562 nonlinear AMS and hybrid systems BMC benchmarks. With pattern matching enabled, DRPM achieves a 2.1×–7.4× PAR-2 speedup, with no increase in memory footprint. DRPM is available via open-source repository, and provides a drop-in 7.5×–11.4× end-to-end speedup on BMC problems over dReal3, the current state-of-the-art QF_NRA_ODE solver.