Instrumenting AMS assertion verification on commercial platforms

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: R. Alur , C. Courcoubetis , N. Halbwachs , T. A. Henzinger , P.-H. Ho , X. Nicollin , A. Olivero , J. Sifakis , S. Yovine, The algorithmic analysis of hybrid systems, Theoretical Computer Science, v.138 n.1, p.3-34, Feb. 6, 1995 [doi>10.1016/0304-3975(94)00202-T]
• 2: Rajeev Alur , Tomás Feder , Thomas A. Henzinger, The benefits of relaxing punctuality, Journal of the ACM (JACM), v.43 n.1, p.116-146, Jan. 1996 [doi>10.1145/227595.227602]
• 3: AMS-User-Guide. Virtuoso AMS Environment User Guide. www.ece.osu.edu/~bibyk/ee894z/\\amsenvug.pdf.
• 4: A. Balivada , Y. Hoskote , J. A. Abraham, Verification of transient response of linear analog circuits, Proceedings of the 13th IEEE VLSI Test Symposium, p.42, April 30-May 03, 1995
• 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: Tathagato Rai Dastidar , P. P. Chakrabarti, A Verification System for Transient Response of Analog Circuits Using Model Checking, Proceedings of the 18th International Conference on VLSI Design held jointly with 4th International Conference on Embedded Systems Design, p.195-200, January 03-07, 2005 [doi>10.1109/ICVD.2005.38]
• 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.
• 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.
• 10: Goran Frehse , Bruce H. Krogh , Rob A. Rutenbar, Verifying analog oscillator circuits using forward/backward abstraction refinement, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
• 11: Formal Verification of Synthesized Analog Designs, Proceedings of the 1999 IEEE International Conference on Computer Design, p.40, October 10-13, 1999
• 12: S. Gupta , B. H. Krogh , R. A. Rutenbar, Towards formal verification of analog designs, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.210-217, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382573]
• 13: Keith Hanna, Reasoning about Real Circuits, Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and Its Applications, p.235-253, September 19-22, 1994
• 14: Keith Hanna, Reasoning About Analog-Level Implementationsof Digital Systems, Formal Methods in System Design, v.16 n.2, p.127-158, March 2000 [doi>10.1023/A:1008791128550]
• 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: Lars Hedrich , Erich Barke, A formal approach to nonlinear analog circuit verification, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.123-127, November 05-09, 1995, San Jose, California, United States
• 17: L. Hedrich , E. Barke, A formal approach to verification of linear analog circuits wth parameter tolerances, Proceedings of the conference on Design, automation and test in Europe, p.649-655, February 23-26, 1998, Le Palais des Congrés de Paris, France
• 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.
• 19: Alexander Jesser , Lars Hedrich, A symbolic approach for mixed-signal model checking, Proceedings of the 2008 conference on Asia and South Pacific design automation, January 21-24, 2008, Seoul, Korea
• 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.
• 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.
• 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.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Verification

Additional Classification:
  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.4 Model Validation and Analysis

General Terms:
Design, Experimentation, Verification

Keywords:
Assertion, OVL, SVA, integrated mixed signal design, simulation, verification library