Reachability in Analog and AMS. Innovation in Verification

Can a combination of learning-based surrogate models plus reachability analysis provide first pass insight into extrema in circuit behavior more quickly than would be practical through Monte-Carlo analysis? Paul Cunningham (GM, Verification at Cadence), Raúl Camposano (Silicon Catalyst, entrepreneur, former Synopsys CTO and lecturer at Stanford, EE292A) and I continue our series on research ideas. As always, feedback welcome.

The Innovation

This month’s pick, HFMV: Hybridizing Formal Methods and Machine Learning for

Verification of Analog and Mixed-Signal Circuits, was published in the 2018 DAC and has 2 citations. The authors are from Texas A&M University.

While in this series we usually look at innovations around digital circuitry, the growing importance of mixed signal in modern designs cannot be overlooked. This month’s pick considers machine learning together with formal methods in AMS to explore reachability for out-of-spec behaviors. The goal is to find out-of-spec performance behavior, normally addressed through Monte Carlo analysis but very expensive across a high-dimensional parameter space. Instead an ML-based surrogate model plus reachability analysis could be an effective aid in quick turnaround design exploration, while still turning back to standard methods for full/signoff validation.

My interest in this paper was triggered by a question in a DVCon keynote a couple of years ago, looking for a better way to check CDC (clock domain crossings) in mixed signal designs. Might this approach be relevant? Reachability in that case would be finding a case where a register data input doesn’t settle until inside the setup window.

Paul’s view

Great paper on combining machine learning with formal methods for high sigma verification of small analog circuits. The authors test their method, hybrid formal / machine-learning verification (HFMV), on a differential amplifier, LDO, and DC2DC converter across a range of performance specifications (e.g. gain, GBW, CMRR, …). Comparing to scaled sigma sampling (SSS), a relatively state-of-the-art importance sampling method, HFMV, finds multiple failures with less than 1k samples across all three circuits, whereas SSS is unable to find any failure after 4-9k samples. Impressive.

HFMV works by first building a predictor for a sample being a failure with some given probability using Bayesian machine learning methods. An SMT problem (a Boolean expression which can include numerical expressions and inequalities within it, e.g. a>b AND x+a<y) is constructed using this predictor. This expression is satisfied by any sample point that is predicted to have a probability of being a failure greater than some threshold, P. An existing state of the art SMT solver, Z3, is then used to try and satisfy the expression with a value of P close to 1.0, i.e. to find a sample point that has a probability of being a failure. Neat trick! After a batch of 350 samples has been generated from the SAT solver, real simulations are run to determine the ground truth results for these samples. The Bayesian model is updated with the new results, and the process repeated. If the SMT solver fails to converge on a solution, then P is decreased in small steps until the converges.

The other key innovation in this paper is some clever math tricks that modify the Bayesian model to make it more amenable to SMT solvers. The first is to apply a mapping function to the input parameters to make the model behave more linearly. The second removes a quadratic term in the model, again to make it more linear. This paper is a wonderful example of how disruptive innovation often happens at the intersection of different perspectives. Blending Bayesian with SMT, as the authors do here, is a brilliant idea, and the results speak for themselves.

Raúl’s view

Verifying that an analog circuit meets its specifications as design parameters vary (transistor channel length and width, temperature, supply voltage, …) requires simulating the circuit at numerous points within a defined parameter space. This is essentially the same problem addressed by commercial tools such as Siemens’ Solido, Cadence’s Spectre FMC analysis, Synopsys’ WiCkeD, Silvaco’s Varman, etc. all of which are crucial for applications such as library characterization and analog design. A common metric is the probability of identifying rare failures, presuming a Gaussian distribution with a specified width of σ; for instance, 6σ refers to approximately 2 parts per billion (2×10⁻⁹) being undetected. Employing “brute force” Monte Carlo simulations could require around 1.5 billion samples to identify at least one 6σ failure with 95% confidence which is infeasible. Commercial tools address this in different ways, e.g., statistical learning, functional margin computation, worst-case distance estimation (WCD) and scaled-sigma sampling (SSS). The paper in this blog introduced a novel technique, not yet commercialized, called “Hybrid Formal/Machine learning Verification” (HFMV). This verification framework integrates the scalability of machine learning with the precision of formal methods to detect extremely rare failures in analog/mixed-signal (AMS) circuits.

The paper focuses heavily on mathematics and may be challenging to read, but the main ideas are as follows. HFMV exploits commonly used probabilistic ML models such as Bayesian additive regression trees, relevance vector machine (RVM) [12], and sparse relevance kernel machine (SRKM), trained on limited simulation or measurement data to probabilistically predict failure. Points in the parameter space can be characterized as strong failure, weak failure, weak good, or strong good, depending on prediction confidence. Formal verification using Satisfiability Modulo Theories (SMT) is applied to identify high probability failure points (confirmed as true failures by a single simulation), and to prove that all points within a space have a very low probability of being failure points. Since rare failures might not appear in the initial training set, active learning refines the model iteratively. SMT solving is accelerated by several orders of magnitude by input space remapping and linear approximation.

HFMV is tested on a Differential amplifier, a Low-Dropout Regulator (LDO) and a DC-DC converter, tested on specs like GBW, gain, CMRR, overshoot, quiescent current, etc. and compared to Monte Carlo and SSS. HFMV hits the first true failure point using 600-1,500 samples, which are about 10x and up to 1,000x lower than used by SSS and MC respectively. Yet, neither MC and SSS can find any true failure in the bounded parameter space.

Despite being published in 2018, our blog paper shows that HFMV outperforms techniques used in current commercial tools for high σ rare failure detection, effectively bridging the gap between accuracy and scalability (ML models) and rigor and completeness (formal methods). In addition, given the significant advancements in machine learning since its publication, implementing such capabilities today could be very interesting.