Login | Register

Exploiting Bounds Optimization for the Semi-formal Verification of Analog Circuits

Title:

Exploiting Bounds Optimization for the Semi-formal Verification of Analog Circuits

Lahiouel, Ons, Aridhi, Henda, Zaki, Mohamed H. and Tahar, Sofiène (2017) Exploiting Bounds Optimization for the Semi-formal Verification of Analog Circuits. Integration, the VLSI Journal . ISSN 01679260 (In Press)

[thumbnail of Exploiting-Bounds-Optimization-for-the-Semi-formal-Verification-of-Analog-Circuits_2017_Integration-the-VLSI-Journal.pdf]
Preview
Text (application/pdf)
Exploiting-Bounds-Optimization-for-the-Semi-formal-Verification-of-Analog-Circuits_2017_Integration-the-VLSI-Journal.pdf - Accepted Version
Available under License Spectrum Terms of Access.
1MB

Official URL: http://dx.doi.org/10.1016/j.vlsi.2017.06.008

Abstract

This paper proposes a semi-formal methodology for modeling and verification of analog circuits behavioral properties using multivariate optimization techniques. Analog circuit differential models are automatically extracted and their qualitative behavior is computed for interval-valued parameters, inputs and initial conditions. The method has the advantage of guaranteeing the rough enclosure of any possible dynamical behavior of analog circuits. The circuit behavioral properties are then verified on the generated transient response bounds. Experimental results show that the resulting state variable envelopes can be effectively employed for a sound verification of analog circuit properties, in an acceptable run-time.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Refereed:Yes
Authors:Lahiouel, Ons and Aridhi, Henda and Zaki, Mohamed H. and Tahar, Sofiène
Journal or Publication:Integration, the VLSI Journal
Date:23 June 2017
Digital Object Identifier (DOI):10.1016/j.vlsi.2017.06.008
Keywords:Analog Circuits; Global Optimization; Verification; Qualitative Simulation
ID Code:982648
Deposited By: Danielle Dennie
Deposited On:28 Jun 2017 14:46
Last Modified:01 Jun 2018 00:00

References:

B. Liu, G. Gielen, F.V. Fernandez. Automated Design of Analog and High-frequency Circuits. Springer (2014) https://doi.org/10.1007/978-3-642-39162-0

M.H. Zaki, S. Tahar, G. Bois. Formal verification of analog and mixed signal designs: A survey. Microelectronics Journal, 39 (12) (2008), pp. 1395–1404 https://doi.org/10.1016/j.mejo.2008.05.013

SPICE, Spice, user's guide and manuals (April 2015).

S. Steinhorst, L. Hedrich, Improving verification coverage of analog circuit blocks by state space-guided transient simulation, in: International Symposium on Circuits and Systems, 2010, pp. 645-648. http://dx.doi.org/10.1109/ISCAS.2010.5537507.

G. Bontempi, Modeling with uncertainty in continuous dynamical systems: the probability and possibility approach, Tech. rep., Iridia, Universite Libre de Bruxelle, Brussels, Belgium (1995). http://www.ulb.ac.be/di/map/gbonte/ftp/bontempi_fpde.pdf.

O. Hasan, S. Tahar. Formal verification methods. encyclopedia of information science and technology. IGI Global (2015), pp. 7162–7170 https://doi.org/10.4018/978-1-4666-5888-2.ch705

A. Bonarini, G. Bontempi. A qualitative simulation approach for fuzzy dynamical models. ACM Transactions on Modeling and Computer Simulation, 4 (1994), pp. 285–313

L.A. Zadeh, Fuzzy sets, Information and Control, 1965. http://dx.doi.org/10.1016/S0019-9958(65)90241-X.

R.J. Baker. CMOS Circuit Design Layout, and Simulation. Wiley-IEEE Press (2010) http://doi.org/10.1002/9780470891179.ch21

K. Lata, H. Jamadagni, Formal verification of tunnel diode oscillator with temperature variations, in: Asia and South Pacific Design Automation Conference, 2010, pp. 217-222. http://dx.doi.org/10.1109/ASPDAC.2010.5419891.

M. Greenstreet, S. Yang, Verifying start-up conditions for a ring oscillator, in: ACM Great Lakes Symposium on VLSI, 2008, pp. 201–206 http://dx.doi.org/10.1145/1366110.1366160.

M. Miller, F. Brewer, Formal verification of analog circuit parameters across variation utilizing SAT, in: Design, Automation and Test in Europe, 2013, pp. 1442-1447 http://dx.doi.org/10.1109/43.273749.

Y. Zhang, S. Sankaranarayanan, F. Somenzi. Piecewise linear modeling of nonlinear devices for formal verification of analog circuits. Formal Methods in Computer Aided Design (2012), pp. 196–203 https://doi.org/10.1/1.362.8818

L. Yin, Y. Deng, P. Li, Verifying dynamic properties of nonlinear mixed-signal circuits via efficient SMT-based techniques, in: International Conference on Computer-Aided Design, 2012, pp. 436-442 http://dx.doi.org/10.1145/2429384.2429474.

X.-X. Liu, S.-D. Tan, Z. Hao, G. Shi, Time-domain performance bound analysis of analog circuits considering process variations, in: Asia and South Pacific Design Automation Conference, 2012, pp. 535-540 http://dx.doi.org/10.1109/ASPDAC.2012.6165011.

X.X. Liu, A. A. Palma-Rodriguez, S. Rodriguez-Chavez, S. X. D. Tan, E. Tlelo-Cuautle, Y. Cai, Performance bound and yield analysis for analog circuits under process variations, in: Design Automation Conference (ASP-DAC), 2013 18th Asia and South Pacific, 2013, pp. 761-766 http://dx.doi.org/10.1109/ASPDAC.2013.6509692.

Y. Song, H. Yu, S.M.P. DinakarRao. Reachability-based robustness verification and optimization of sram dynamic stability under process variations. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 33 (4) (2014), pp. 585–598 https://doi.org/10.1109/TCAD.2014.2304704

L. Ni, S.M.P.D.Y. Song, C. Gu, H. Yu. A zonotoped macromodeling for eye-diagram verification of high-speed i/o links with jitter and parameter variations. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 35 (6) (2016), pp. 1040–1051 https://doi.org/10.1109/TCAD.2015.2481873

L.T.J. Back, F. Nobile, R. Tempone, Spectral and high order methods for partial differential equations, Lecture Notes in Computational Science and Engineering 76 (3) (2011) 43-62 http://dx.doi.org/10.1007/978-3-642-15337-2.

P. Manfredi, I. Stievano, F. Canavero. Alternative spice implementation of circuit uncertainties based on orthogonal polynomials. Electrical Performance of Electronic Packaging and Systems (2011), pp. 41–44 https://doi.org/10.1109/EPEPS.2011.6100181

C. Yan, M. Greenstreet, Oscillator verification with probability one, in: Formal Methods in Computer-Aided Design, 2012, pp. 165–172.

M. Nikravesh, L.A. Zadeh, V. Korotkikh. Reservoir Characterization and Modeling Series: Studies in Fuzziness and Soft Computing. Springer Verlag (2004) https://doi.org/10.1007/978-3-540-39675-8

O. Lahiouel, H. Aridhi, M.H. Zaki, S. Tahar, A semi-formal approach for analog circuits behavioral properties verification, in: ACM Great Lakes Symposium on VLSI, 2014, pp. 247–248 http://dx.doi.org/10.1145/2591513.2591578.

O. Lahiouel, H. Aridhi, M.H. Zaki, S. Tahar, A tool for modeling and analysis of analog circuits, Tech. rep., Concordia University, Montreal, Quebec, Canada (2012) http://hvg.ece.concordia.ca/Publications/TECH_REP/TMAAC_TR1

R. Horst, P.M. Pardalos, N.V. Thoai. Introduction to Global Optimization. Kluwer Academic Publishers (2000)

MATLAB, Documentation center (September 2015) http://www.mathworks.com/products/matlab/.

J. Momoh, J. Zhu. Improved interior point method for OPF problems. IEEE Transactions on Power Systems, 14 (3) (1999), pp. 1114–1120 https://doi.org/10.1109/59.780938

W.M. Hartmann. Signals, Sound, and Sensation. American Institute of Physics (1998) https://doi.org/10.1063/1.882215

B. McCarthy, Sound Systems: Design and Optimization: Modern Techniques and Tools for Sound System Design and Alignment, Images of America, Focal, 2007.

M. Mingyu, L. Hedrich, C. Sporrer. A machine-readable specification of analog circuits for integration into a validation flow. Specification and Design Languages (2011), pp. 1–8

S. Steinhorst, L. Hedrich, Model checking of analog systems using an analog specification language, in: Design, Automation and Test in Europe, 2008, pp. 324-329. http://dx.doi.org/10.1109/DATE.2008.4484700.

H.E. Graeb. Analog Design Centering and Sizing. Springer (2007) https://doi.org/10.1007/978-1-4020-6004-5

S. Saibua, L. Qian, D. Zhou, Worst case analysis for evaluating vlsi circuit performance bounds using an optimization method, in: VLSI and System-on-Chip, 2011, pp. 102–105 http://dx.doi.org/10.1109/VLSISoC.2011.6081660.

T. Yu, S.-D. Tan, Y. Cai, P. Tang, Time-domain performance bound analysis for analog and interconnect circuits considering process variations, in: Asia and South Pacific Design Automation Conference, 2014, pp. 455-460. http://dx.doi.org/10.1109/ASPDAC.2014.6742933.
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top