Formal verification of bond graph modelled analogue circuits

Author(s): W. Denman ; M.H. Zaki ; S. Tahar
DOI: 10.1049/iet-cds.2009.0221

For access to this article, please select a purchase option:

Buy article PDF

Buy Knowledge Pack

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership

Recommend Title Publication to library

IET Circuits, Devices & Systems — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

Author(s): W. Denman ¹ ; M.H. Zaki ² ; S. Tahar ¹
- Affiliations: 1: Department of Electrical & Computer Engineering, Concordia University, Montreal, Canada
  2: Department of Computer Science, University of British Columbia, Vancouver, Canada
Source: Volume 5, Issue 3, May 2011, p. 243 – 255
DOI: 10.1049/iet-cds.2009.0221 , Print ISSN 1751-858X, Online ISSN 1751-8598

Analogue circuits are an increasingly critical component in embedded system designs. Traditionally, simulation is used for verification, but owing to the infinite state space of analogue components, the 100% correctness of a design cannot be guaranteed. Formal methods, based around applying mathematical expressions and reasoning to prove correctness, have been developed to increase the verification confidence level. This study introduces and demonstrates a methodology for formally verifying safety properties of analogue circuits. In the proposed approach, system equations are automatically extracted from a SPICE netlist by means of energy-conservative bond graph models. Verification based on abstract model checking and constraint solving is then applied on the extracted equation models. The authors methodology avoids an exhaustive and time demanding simulation that is normally encountered during analogue circuit verification. To this end, the authors have used a set of tools to implement the proposed verification flow and applied it on tunnel diode, Chua and Colpitts oscillators as case studies.

References

1. 1)
  - H. Chang , K. Kundert . Verification of complex analog and RF IC designs. Proc. IEEE , 3 , 622 - 639
2. 2)
  - Gupta, S., Krogh, B.H., Rutenbar, R.A.: `Towards formal verification of analog designs', Proc. IEEE/ACM Int. Conf. Computer Aided Design, 2004, p. 210–217.
3. 3)
  - Graf, S., Saidi, H.: `Construction of abstract state graphs with PVS', Computer Aided Verification, 1997, p. 72–83, (LNCS, 1254).
4. 4)
  - Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: `Counterexample-guided abstraction refinement', Computer Aided Verification, 2000, p. 154–169, (LNCS, 1855).
5. 5)
  - E.M. Clarke , O. Grumberg . (1999) Model checking.
6. 6)
  - R.P. Kurshan , K.L. McMillan . Analysis of digital circuits through symbolic re-duction. IEEE Trans. Comput.-Aided Des , 11 , 1356 - 1371
7. 7)
  - Alur, R., Dang, T., Ivancic, F.: `Reachability analysis via predicate abstraction', Hybrid Systems: Computation and Control, 2002, p. 35–48, (LNCS, 2289).
8. 8)
  - Y.E. Fattah . Constraint logic programming for structure-based reasoning about dynamic physical systems. Artif. Intell. Eng , 253 - 264
9. 9)
  - Cellier, F.E., Clauss, C., Urquia, A.: `Electronic circuit modelling and simulation in modelica', Proc. Eurosim Congress on Modelling and Simuulation, 2007, 2, p. 1–10.
10. 10)
  - J.R. Abrial . Faultless systems: yes we can. Computer , 9 , 30 - 36
11. 11)
  - Denman, W.: `Towards the automated modelling and formal verification of analog designs', 2009, Master's, Concordia University, Montreal, Quebec, Canada.
12. 12)
  - D. Karnopp , R.C. Rosenberg . (1968) Analysis and simulation of multiport systems: the bond graph approach to physical system dynamics.
13. 13)
  - J. Vlach , K. Singhal . (1994) Computer methods for circuit analysis and design.
14. 14)
  - S. Ratschan , Z. She . Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Trans. Embedded Comput. Syst , 1 , 1 - 23
15. 15)
  - Hartong, W., Klausen, K., Hedrich, L.: `Formal verification for nonlinear analog systems: approaches to model and equivalence checking', Advanced Formal Verification, 2004, p. 205–245.
16. 16)
  - Clarke, E., Fehnker, A., Han, Z., Krogh, B.H., Stursberg, O., Theobald, M.: `Verification of hybrid systems based on counterexample-guided abstraction refinement', Tools and Algorithms for the Construction and Analysis of Systems, 2003, p. 192–207, (LNCS, 2619).
17. 17)
  - Ratschan, S.: `Continuous first-order constraint satisfaction', Artificial Intelligence, Automated Reasoning and Symbolic Computation, 2002, p. 181–195, (LNCS, 2385).
18. 18)
  - Greenstreet, M.R., Mitchell, I.: `Reachability analysis using polygonal projections', Hybrid System: Computation and Control, 1999, p. 103–116, (LNCS, 1569).
19. 19)
  - Dang, T., Donze, A., Maler, O.: `Verification of analog and mixed-signal circuits using hybrid system techniques', Formal Methods in Computer-Aided Design, 2004, p. 14–17, (LNCS, 3312).
20. 20)
  - Jirstrand, M., Gunnarsson, J., Fritzson, P.: `A new modeling and simulation environment for mathematica', Proc. Int. Mathematica Symp, 1999, Available at http://www.modelica.org.
21. 21)
  - Cellier, F.E., Nebot, A.: `The modelica bond graph library', Swiss Federal Institute of Technology, 2007.
22. 22)
  - Tiwary, S.K., Gupta, A., Phillips, J.R., Pinello, C., Zlatanovici, R.: `First Steps towards SAT-based formal analog verification', Proc. IEEE/ACM Int. Conf. Computer-Aided Design, 2009, p. 1–8.
23. 23)
  - T. Kropf . (1999) Introduction to formal hardware verification.
24. 24)
  - Frehse, G., Krogh, B.H., Rutenbar, R.A.: `Verifying analog oscillator circuits using forward/backward abstraction refinement', Proc. IEEE Design Automation and Test in Europe, 2006, p. 257–262.
25. 25)
  - Tiwari, A.: `Series of abstractions for hybrid automata', Hybrid Systems: Computation and Control, 2002, p. 465–478, (LNCS, 2289).
26. 26)
  - Mattsson, S.E., Olsson, H., Elmqvist, H.: `Dynamic selection of states in dymola', Modelica Workshop, 2000, p. 62–67.
27. 27)
  - M. Zaki , S. Tahar , G. Bois . Qualitative abstraction-based verification for analog circuits. Revue des Nouvelles Technologies de l'information , 147 - 158
28. 28)
  - L.O. Chua . Chua's circuit : an overview ten years later. J. Circuits Syst. Comput , 117 - 159
29. 29)
  - M. Zaki , S. Tahar , G. Bois . Formal verification of analog and mixed signal designs: a survey. Microelectron. J. , 12 , 1 - 10
30. 30)
  - W. Borutzky . Supporting the generation of a state space model by adding tearing information to the bond graph. Simul. Prac. Theory , 419 - 438
31. 31)
  - A.S. Sedra , K.C. Smith . (1998) Microelectronic circuits.
32. 32)
  - Maehne, T., Vachoux, A.: `Proposal for a bond graph-based model of computation in system C-AMS', Proc. Languages for Formal Specification and Verification, Forum on Specification and Design Languages, 2007, p. 25–31.
33. 33)
  - Broenink, F.: `Introduction to physical systems modelling with bond graphs', University of Twente, 1999.
34. 34)
  - de Moura, L.M., Owre, S., Rue, B.H.: `SAL 2', Computer Aided Verification, 2004, p. 496–500, (LNCS, 3114).
35. 35)
  - Dassault Systemes: ‘The Dymola modelling laboratory’. Available at http://www.dymola.com/index.htm.
36. 36)
  - M.P. Kennedy . Chaos in the Colpitts oscillator. IEEE Trans. Circuits Syst. I , 11 , 771 - 774
37. 37)
  - S. Wolfram . (1991) Mathematica: a system for doing mathematics.

Formal verification of bond graph modelled analogue circuits

Formal verification of bond graph modelled analogue circuits

Buy article PDF

Buy Knowledge Pack

Thank you

References

Related content