Title
Verification of digitally-intensive analog circuits via kernel ridge regression and hybrid reachability analysis
Abstract
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.
Year
DOI
Venue
2013
10.1145/2463209.2488814
DAC
Keywords
Field
DocType
nonideal digital effects,large linear portion,overflow,kernel ridge regression,analogue-digital conversion,locked time verification,approximation theory,increased digital design content,learning (artificial intelligence),regression analysis,analog approximation,conservative analog approximation,digitally-intensive analog circuit verification,digital signals,digitally intensive phase locked loop,satisfiability modulo theories technique,digital block,phase locked loops,round-off error,digitally-intensive analog circuit,digital block conversion,digital design content,hybrid reachability analysis,hybrid formal reachability analysis,non-ideal digital effect,analog signals,machine learning approach,hybrid formal reachability analysis framework,remaining nonlinear portion,finite resolution,electronic engineering computing,formal verification,reachability analysis,learning artificial intelligence,soft error,redundancy
Phase-locked loop,Analogue electronics,Soft error,Computer science,Algorithm,Approximation theory,Electronic engineering,Real-time computing,Reachability,Redundancy (engineering),Satisfiability modulo theories,Formal verification
Conference
ISSN
Citations 
PageRank 
0738-100X
7
0.58
References 
Authors
10
3
Name
Order
Citations
PageRank
Honghuang Lin1293.83
Peng Li21912152.85
Chris J. Myers360775.73