research-article

Instrumenting AMS assertion verification on commercial platforms

Authors:

Rajdeep Mukhopadhyay,

Pallab Dasgupta,

John GoughAuthors Info & Claims

ACM Transactions on Design Automation of Electronic Systems (TODAES), Volume 14, Issue 2

Article No.: 21, Pages 1 - 47

https://doi.org/10.1145/1497561.1497564

Published: 07 April 2009 Publication History

Abstract

The industry trend appears to be moving towards designs that integrate large digital circuits with multiple analog/RF (radio frequency) interfaces. In the verification of these large integrated circuits, the number of nets that need to be monitored has been growing rapidly. Consequently, the mixed-signal design community has been feeling the need for AMS (Analog and Mixed Signal) assertions that can automatically monitor conformance with expected time-domain behavior and help in debugging deviations from the design intent. The main challenges in providing this support are (a) developing AMS assertion languages or AMS verification libraries, and (b) instrumenting existing commercial simulators to support assertion verification during simulation. In this article, we report two approaches: the first extends the Open Verification Library (OVL) to the AMS domain by integrating a new collection of AMS verification libraries; while the second extends SystemVerilog Assertions (SVA) by augmenting analog predicates into SVA. We demonstrate the use of AMS-OVL on the Cadence Virtuoso environment while emphasizing that our libraries can work in any environment that supports Verilog and Verilog-A. We also report the development of tool support for AMS-SVA using a combination of Cadence NCSIM and Synopsys VCS. We demonstrate the utility of both approaches on the verification of LP3918, an integrated power management unit (PMU) from National Semiconductors. We believe that in the absence of existing EDA (Electronic Design Automation) tools for AMS assertion verification, the proposed approaches of integrating our libraries and our tool sets with existing commercial simulators will be of considerable and immediate practical value.

References

[1]

Alur, R., Courcoubetis, C., Halbwachs, N., and Henzinger, T. A. 1995. The algorithmic analysis of hybrid systems. Theore. Comput. Sci. 138, 1, 3--34.

Digital Library

[2]

Alur, R., Feder, T., and Henzinger, T. A. 1996. The benefits of relaxing punctuality. J. ACM 43, 1, 116--146.

Digital Library

[3]

AMS-User-Guide. Virtuoso AMS Environment User Guide. www.ece.osu.edu/~bibyk/ee894z/\\amsenvug.pdf.

[4]

Balivada, A., Chen, J., and Abraham, J. 1995. Verification of transient response of linear analog circuits. In Proceedings of the IEEE VLSI Test Symposium. 42--47.

Digital Library

[5]

Coram, G. 2004. How to (and how not to) write a compact model in Verilog-A. In Proceedings of the Behavioral Modeling and Simulation Conference. 97--106.

[6]

Dang, T., Donze, A., and Maler, O. 2004. Verification of analog and mixed-signal circuits using hybrid system techniques. In Proceedings of the Formal Methods In Computer-aided Design:5th International Conference (FMCAD).

[7]

Dastidar, T. and Chakrabarti, P. 2005. A verification system for transient response of analog circuits using model checking. In Proceedings of the 18th International Conference on VLSI Design.

Digital Library

[8]

Dutertre, B. and de Moura, L. 2006. A fast linear-arithmetic solver for DPLL (T). In Computer-Aided Verification. Lecture Notes in Computer Science, vol. 4144, Springer, Berlin, 81--94.

Digital Library

[9]

Frehse, G. 2005. PHAVer: Algorithmic verification of hybrid systems past HyTech. In Proceedings of the Hybrid Systems: Computation and Control Conference. Lecture Notes in Computer Science, vol. 3414, Springer, Berlin. 258--273.

Digital Library

[10]

Frehse, G., Krogh, B., and Rutenbar, R. 2006. Verifying analog oscillator circuits using forward/backward abstraction refinement. In Proceedings of the Conference on Design, Automation and Test in Europe. 257--262.

Digital Library

[11]

Ghosh, A. and Vemuri, R. 1999. Formal verification of synthesized analog designs. In Proceedings of the International Conference on Computer Design. 40--45.

Digital Library

[12]

Gupta, S., Krogh, B., and Rutenbar, R. 2004. Towards formal verification of analog designs. In Proceedings of the International Conference on Computer Aided Design (ICCAD). IEEE/ACM, 210--217.

Digital Library

[13]

Hanna, K. 1994. Reasoning about real circuits. In Proceedings of the 7th International Higher Order Logic Theorem Proving and Its Applications Conference. 235--253.

Digital Library

[14]

Hanna, K. 2000. Reasoning about analog-level implementations of digital systems. Formal Meth. Syst. Des. 16, 2, 127--158.

Digital Library

[15]

Hartong, W., Klausen, R., and Hedrich, L. 2004. Formal verification for nonlinear analog systems. In Approaches to Model and Equivalence Checking. Advanced Formal Verification, Kluwer, Amsterdam, 205--245.

[16]

Hedrich, L. and Barke, E. 1995. A formal approach to nonlinear analog circuit verification. In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design. 123--127.

Digital Library

[17]

Hedrich, L. and Barke, E. 1998. A formal approach to verification of linear analog circuits with parameter tolerances. In Proceedings of the Conference on Design, Automation and Test in Europe.

Digital Library

[18]

Henzinger, T., Ho, P., and Wong-Toi, H. 1997. HYTECH: A model checker for hybrid systems. Int. J. Softw. Tools Technol. Transfer 1, 1, 110--122.

Digital Library

[19]

Jesser, A. and Hedrich, L. 2008. A symbolic approach for mixed-signal model checking. In Proceedings of the Conference on Asia and South Pacific Design Automation. IEEE Computer Society Press, Los Alamitos, CA, 404--409.

Digital Library

[20]

Jesser, A. et al. 2007. Analog simulation meets digital verification—A formal assertion approach for mixed-signal verification. In Proceedings of the Workshop on Synthesis and System Integrating of Mixed Information Technologies (SASIMI). 507--514.

[21]

Kundert, K. 1995. The Designer's Guide to Verilog-AMS. Kluwer, Amsterdam.

[22]

LP3918. http://www.national.com/pf/LP/LP3918.html.

[23]

Maler, O. 2005. Extending PSL for analog circuits. Res. rep. PROSYD Deliverable D 1, 1.

[24]

Maler, O. and Nickovic, D. 2004. Monitoring temporal properties of continuous signals. In Proceedings of the Conference Formal Techniques, Modeling and Analysis of Timed and Fault-Tolerant Systems. Lecture Notes in Computer Science, vol. 3253, Springer, Berlin, 152--166.

[25]

Maler, O., Pnueli, A., and Nickovic, D. 2008. Checking temporal properties of discrete, timed and continuous behaviors. Trakhtenbrot Festschrift.

[26]

MLD. MLDesigner documentation version 2.5. http://www.mldesigner.com.

[27]

Nickovic, D. and Maler, O. 2007. AMT: A property-based monitoring tool for analog systems. In Proceedings of the 5th International Conference on Formats.

Digital Library

[28]

OVL. Open Verification Library. http://www.accellera.org/activities/ovl.

[29]

Peruzzi, R. O. 2006. Verification of digitally calibrated analog systems with Verilog-AMS behavioral models. In Proceedings of the Behavioral Modeling and Simulation Workshop. 7--16.

[30]

Salem, A. 2002. Semi-formal verification of VHDL-AMS descriptions. In Proceedings of the IEEE Symposium on Circuits and Systems (ISCAS 5).

[31]

Sammane, G. A. 2007. Towards assertion based verification of analog and mixed signal designs using PSL. In Proceedings of the Conference on Languages for Formal Specification and Verification (FDL).

[32]

SVA. System Verilog Assertions. http://www.systemverilog.org.

[33]

Verilog AMS LRM. www.verilog.org/verilogams/htmlpages/publicdocs/lrm/2.2/AMS-LRM-2-2.pdf.

[34]

Verilog-XL-Env-User-Guide. Virtuoso Verilog-XL Environment User Guide, Product Version 5.1.41. http://www.ece.uci.edu/eceware/cadence/compveruser/chap9.html.

[35]

Walter, D. 2007. Bounded model checking of analog and nixed-signal circuits using an SMT solver. In Proceedings of the Conference on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 4762, Springer, Berlin, 66--81.

Digital Library

[36]

Zaki, M., Tahar, S., and Bois, G. 2006. Formal verification of analog and mixed signal designs: Survey and comparison. In Proceedings of the IEEE Northeast Workshop on Circuits and Systems. 281--284.

Cited By

Sanyal SDasgupta PHazra ADas SMorrison SSurendran SBalasubramanian L(2022)The CoveRT Approach for Coverage Management in Analog and Mixed-Signal Integrated CircuitsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2022.315768641:12(5695-5708)Online publication date: Dec-2022
https://doi.org/10.1109/TCAD.2022.3157686
Mandal SDasgupta P(2022)Migrating Assertions From Dense to Discrete TimeIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2021.310171541:7(2362-2371)Online publication date: Jul-2022
https://doi.org/10.1109/TCAD.2021.3101715
Sanyal Sda Costa ADasgupta P(2021)Recurrence in Dense-Time AMS AssertionsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2020.304025940:11(2416-2420)Online publication date: 1-Nov-2021
https://dl.acm.org/doi/10.1109/TCAD.2020.3040259
Show More Cited By

Index Terms

Instrumenting AMS assertion verification on commercial platforms
1. Computing methodologies
  1. Modeling and simulation
    1. Model development and analysis
      1. Model verification and validation
2. Hardware
  1. Hardware validation
    1. Functional verification

Recommendations

Synchronizing AMS Assertions with AMS Simulation: From Theory to Practice

The verification community anticipates the adoption of assertions in the Analog and Mixed-Signal (AMS) domain in the near future. Several questions need to be answered before AMS assertions are brought into practice, such as: (a) How will the languages ...
Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial)
CAV '08: Proceedings of the 20th international conference on Computer Aided Verification

Debugging, on average, has grown to consume more than 60% of today's ASIC and SoC verification effort. Clearly, this is a topic the industry must address, and some organizations have done just that. Those that have adopted an assertion-based ...
Inline Assertions - Embedding Formal Properties in a Test Bench
VLSID '09: Proceedings of the 2009 22nd International Conference on VLSI Design

The scope of immediate assertions in SystemVerilog is restricted to Boolean properties, where as temporal properties are specified as concurrent assertions. Concurrent assertion statements can also be embedded in a procedural block - known as procedural ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Design Automation of Electronic Systems

ACM Transactions on Design Automation of Electronic Systems Volume 14, Issue 2

March 2009

384 pages

ISSN:1084-4309

EISSN:1557-7309

DOI:10.1145/1497561

Issue’s Table of Contents

Copyright © 2009 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 07 April 2009

Accepted: 01 October 2008

Revised: 01 August 2008

Received: 01 February 2008

Published in TODAES Volume 14, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
372
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)1

Reflects downloads up to 05 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Sanyal SDasgupta PHazra ADas SMorrison SSurendran SBalasubramanian L(2022)The CoveRT Approach for Coverage Management in Analog and Mixed-Signal Integrated CircuitsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2022.315768641:12(5695-5708)Online publication date: Dec-2022
https://doi.org/10.1109/TCAD.2022.3157686
Mandal SDasgupta P(2022)Migrating Assertions From Dense to Discrete TimeIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2021.310171541:7(2362-2371)Online publication date: Jul-2022
https://doi.org/10.1109/TCAD.2021.3101715
Sanyal Sda Costa ADasgupta P(2021)Recurrence in Dense-Time AMS AssertionsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2020.304025940:11(2416-2420)Online publication date: 1-Nov-2021
https://dl.acm.org/doi/10.1109/TCAD.2020.3040259
Ain ADasgupta P(2018)Interpreting Local Variables in AMS Assertions during SimulationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2018.2824288(1-1)Online publication date: 2018
https://doi.org/10.1109/TCAD.2018.2824288
Costa ADasgupta PFrehse GTalpin J(2016)Formal feature analysis of hybrid automataProceedings of the 14th ACM-IEEE International Conference on Formal Methods and Models for System Design10.5555/3343414.3343416(2-11)Online publication date: 18-Nov-2016
https://dl.acm.org/doi/10.5555/3343414.3343416
Ain ABruto da Costa ADasgupta P(2016)Feature Indented Assertions for Analog and Mixed-Signal ValidationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2016.252579835:11(1928-1941)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1109/TCAD.2016.2525798
da Costa ADasgupta PFrehse G(2016)Formal feature analysis of hybrid automata2016 ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)10.1109/MEMCOD.2016.7797740(2-11)Online publication date: Nov-2016
https://doi.org/10.1109/MEMCOD.2016.7797740
Ain ADasgupta P(2015)Monitoring AMS Simulation: From Assertions to Features2015 28th International Conference on VLSI Design10.1109/VLSID.2015.78(429-434)Online publication date: Jan-2015
https://doi.org/10.1109/VLSID.2015.78
Bruto da Costa ADasgupta P(2014)Formal Interpretation of Assertion Based Features on AMS DesignsIEEE Design & Test10.1109/MDAT.2014.2361720(1-1)Online publication date: 2014
https://doi.org/10.1109/MDAT.2014.2361720
Cerny EDudani SHavlicek JKorchemny DCerny EDudani SHavlicek JKorchemny D(2014)IntroductionSVA: The Power of Assertions in SystemVerilog10.1007/978-3-319-07139-8_1(3-29)Online publication date: 8-Jul-2014
https://doi.org/10.1007/978-3-319-07139-8_1
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents