Simulation-Assisted Formal Verification of Nonlinear Mixed-Signal Circuits With Bayesian Inference Guidance

The pressing need for the verification of analog and mixed-signal (AMS) designs is driven by increased design complexity and the integration of such circuits into SoCs. However, verification of AMS circuits remains a significant challenge. This paper proposes a simulation-assisted formal verification methodology that leverages SMT-based satisfiability techniques to tackle the challenges arising from the inherent analog and/or hybrid nature of AMS systems. Although state-of-the-art SMT solvers, in the worst-case scenario, still have exponential complexity in the number of constraints, the main focus of this paper is to first formally formulate the verification task into an SMT problem, then accelerate the verification by using simulation assistance. To verify the nonlinear dynamics, randomly sampled simulations are first applied to quickly explore the reachable state space, and then a nonlinear SMT solver is invoked to ensure the conservativeness. To achieve optimal efficiency, the tradeoff between the runtime costs of simulation and SMT solving is analyzed by means of a Bayesian inference-based technique that dynamically learns from the simulation history. This paper demonstrates the feasibility and efficacy of the proposed methodology on conservative verification of dynamic properties of nonlinear AMS circuits.