ABCD-NL: Approximating Continuous non-linear dynamical systems using purely Boolean models for analog/mixed-signal verification
ABCD-NL: Approximating Continuous non-linear dynamical systems using purely Boolean models for analog/mixed-signal verification
复制标题
ABCD-NL：使用纯布尔模型进行模拟/混合信号验证来逼近连续非线性动力系统
DOI：
10.1109/aspdac.2014.6742898
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
J. Roychowdhury
中科院分区：
文献类型：
--
作者：
Aadithya V. Karthik;Sayak Ray;P. Nuzzo;A. Mishchenko;R. Brayton;J. Roychowdhury
我们提出了 ABCD-NL，一种使用纯布尔模型以高精度逼近非线性模拟电路的技术。给定一个模拟/混合信号 (AMS) 系统（例如 SPICE 网表），ABCD-NL 生成布尔电路表示（例如与逆变器图、有限状态机或二元决策图），捕获给定系统的 I/O 行为，达到接近 SPICE 级别的精度，而无需进行任何先验简化。通过利用为布尔/混合系统分析开发的现有工具（例如 ABC [1]），ABCD-NL 生成的布尔模型可用于 AMS 设计的高速仿真和形式验证。我们将 ABCD-NL 应用于许多 SPICE 级 AMS 电路，包括数据转换器、电荷泵、比较器、非线性信号/通信子系统等。此外，我们正式验证了 AMS 信号系统的吞吐量 - 使用 22nm BSIM4 晶体管在 SPICE 中建模，使用 ABCD-NL 进行高精度布尔运算，并使用 ABC 进行属性检查。
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.