| Title | Analog Circuit Verification by Statistical Model Checking |
| Author | *Ying-Chih Wang, Anvesh Komuravelli, Paolo Zuliani, Edmund M. Clarke (Carnegie Mellon University, U.S.A.) |
| Page | pp. 1 - 6 |
| Keyword | Analog Circuits, Verification, Statistical Model Checking |
| Abstract | We show how statistical Model Checking can be used for verifying properties of analog circuits. As integrated circuit technologies scale down constantly, manufacturing variations in devices make analog designs behave like stochastic systems. In this paper, we use statistical model checking, an efficient verification technique for stochastic systems, for verifying properties of analog circuits in both the temporal and the frequency domain. In particular, randomly sampled traces are sequentially generated by SPICE and model checked to determine whether they satisfy a given specification, until the desired statistical strength is achieved. |
| Slides |
| Title | FSM Model Abstraction for Analog/Mixed-Signal Circuits by Learning from I/O Trajectories |
| Author | *Chenjie Gu, Jaijeet Roychowdhury (University of California, Berkeley, U.S.A.) |
| Page | pp. 7 - 12 |
| Keyword | model abstraction, finite state machine, analog/mixed-signal |
| Abstract | Abstraction of circuits is desirable for faster simulation and high-level system verification. In this paper, we present an algorithm that derives a Mealy machine from differential equations of a circuit by learning input-output trajectories. The key idea is adapted from Angluin's DFA (deterministic finite automata) learning algorithm that learns a DFA from another DFA. Several key components of Angluin's algorithm are modified so that it fits in our problem setting, and the modified algorithm also provides a reasonable partitioning of the continuous state space as a by-product. We validate our algorithm on a latch circuit and an integrator circuit, and demonstrate that the resulting FSMs inherit important behaviors of original circuits. |
| Title | A Structured Parallel Periodic Arnoldi Shooting Algorithm for RF-PSS Analysis based on GPU Platforms |
| Author | Xue-Xin Liu (University of California, Riverside, U.S.A.), Hao Yu (Nanyang Technological University, Singapore), Jacob Relles, *Sheldon X.-D. Tan (University of California, Riverside, U.S.A.) |
| Page | pp. 13 - 18 |
| Keyword | shooting-Newton, periodic steady state analysis, GPU, RF, Krylov |
| Abstract | The recent multi/many-core CPUs or GPUs have provided an ideal
parallel computing platform to accelerate the time-consuming
analysis of radio-frequency/millimeter-wave (RF/ MM) integrated
circuit (IC). This paper develops a structured shooting algorithm
that can fully take advantage of parallelism in periodic steady
state (PSS) analysis. Utilizing periodic structure of the state
matrix of RF/ MM-IC simulation, a cyclic-block-structured
shooting-Newton method has been parallelized and mapped onto
recent GPU platforms. We first present the formulation of the
parallel cyclic-block-structured shooting-Newton algorithm, called
{\em periodic Arnoldi shooting} method. Then we will present its
parallel implementation details on GPU. Results from several
industrial examples show that the structured parallel
shooting-Newton method on Tesla's GPU can lead to speedups of more
than 20$\times$ compared to the state-of-the-art implicit GMRES
methods under the same accuracy on the CPU. |
| Title | Hierarchical Exact Symbolic Analysis of Large Analog Integrated Circuits By Symbolic Stamps |
| Author | *Hui Xu, Guoyong Shi, Xiaopeng Li (Shanghai Jiao Tong University, China) |
| Page | pp. 19 - 24 |
| Keyword | analog integrated circuits, binary decision diagram, determinant expansion, graph reduction, symbolic analysis |
| Abstract | Linearized small-signal transistor models share the common circuit structure but may
take different parameter values in the ac analysis of an analog circuit simulator.
This property can be utilized in symbolic circuit analysis. This paper proposes
to use a symbolic stamp for all device models in the same circuit for hierarchical
symbolic analysis.
Two levels of binary decision diagrams (BDDs) are used for maximum data sharing,
one for the symbolic device stamp and the other for modified nodal analysis.
The symbolic transadmittances of the device stamp share one BDD for storage saving.
The modified nodal analysis (MNA) matrix formulated using symbolic stamp is of greatly lower
dimension, hence its solving complexity by using a determinant decision diagram (DDD)
is greatly reduced.
A circuit simulator is implemented based on the proposed scheme. It is able to analyze
an op-amp circuit containing 44 MOS transistors \emph{exactly} for the first time. |
| Slides |