Verification of digitally-intensive analog circuits via kernel ridge regression and hybrid reachability analysis

The emergence of digitally-intensive analog circuits introduces new challenges to formal verification due to increased digital design content, and non-ideal digital effects such as finite resolution, round-off error and overflow. We propose a machine learning approach to convert digital blocks to conservative analog approximations via the use of kernel ridge regression. These learned models are then adopted in a hybrid formal reachability analysis framework where the support function based manipulations are developed to efficiently handle the large linear portion of the design and the more general satisfiability modulo theories technique is applied to the remaining nonlinear portion. The efficiency of the proposed method is demonstrated for the locked time verification of a digitally intensive phase locked loop.