ABCD-NL: Approximating Continuous non-linear dynamical systems using purely Boolean models for analog/mixed-signal verification
Design Automation Conference(2014)
摘要
We present ABCD-NL, a technique that approximates non-linear analog circuits using purely Boolean models, to high accuracy. Given an analog/mixed-signal (AMS) system (e.g., a SPICE netlist), ABCD-NL produces a Boolean circuit representation (e.g., an And Inverter Graph, Finite State Machine, or Binary Decision Diagram) that captures the I/O behaviour of the given system, to near SPICE-level accuracy, without making any apriori simplifications. The Boolean models produced by ABCD-NL can be used for high-speed simulation and formal verification of AMS designs, by leveraging existing tools developed for Boolean/hybrid systems analysis (e.g., ABC [1]). We apply ABCD-NL to a number of SPICE-level AMS circuits, including data converters, charge pumps, comparators, non-linear signaling/communications sub-systems, etc. Also, we formally verify the throughput of an AMS signaling system - modelled in SPICE using 22nm BSIM4 transistors, Booleanized with high accuracy using ABCD-NL, and property-checked using ABC.
更多查看译文
关键词
Boolean functions,SPICE,charge pump circuits,comparators (circuits),formal verification,integrated circuit design,integrated circuit modelling,mixed analogue-digital integrated circuits,ABCD-NL,AMS designs,BSIM4 transistors,Boolean circuit representation,SPICE-level accuracy,analog-mixed-signal verification,charge pumps,comparators,continuous nonlinear dynamical systems,data converters,formal verification,nonlinear signaling,purely Boolean models,size 22 nm
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络