Verification Approach of Metropolis Design Framework for Embedded Systems

  • Xi Chen
  • Harry Hsieh
  • Felice Balarin

In this paper, we focus on the verification approach of Metropolis, an integrated design framework for heterogeneous embedded systems. The verification approach is based on the formal properties specified in Linear Temporal Logic (LTL) or Logic of Constraints (LOC). Designs may be refined due to synthesis or be abstracted for verification. An automatic abstraction propagation algorithm is used to simplify the design for specific properties. A user-defined starting point may also be used with automatic propagation. Two main verification techniques are implemented in Metropolis the formal verification utilizing the model checker Spin and the simulation trace checking with automatic generated checkers. Translation algorithms from specification models to verification models, as well as algorithms of generated checkers are discussed. We use several case studies to demonstrate our approach for verification of system level designs at multiple levels of abstraction.


LTL LOC metropolis meta-model spin property simulation formal verification 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Keutzer K., Malik S., Newton A.R., Rabaey J., Sangiovanni-Vincentelli A. (December 2000). System Level Design: Orthogonalization of Concerns and Platform-based Design. IEEE Trans, Computer-Aided Design. 19(12):1523–1543CrossRefGoogle Scholar
  2. 2.
    Balarin F., Watanabe Y., Hsieh H., Lavagno L., Passerone C., Sangiovanni-Vincentelli A. (April 2003). Metropolis: An Integrated Electronic System Design Environment. IEEE Comput 36(4):45–52Google Scholar
  3. 3.
    P. Godefroid and G. J. Holzmann, On the Verification of Temporal Properties, Proceedings of IFIP/WG6.1 Symposium on Protocols Specification, Testing, and Verification (June 1993).Google Scholar
  4. 4.
    F. Balarin, Y. Watanabe, J. Burch, L. Lavagno, R. Passerone, and A. Sangiovanni-Vincentelli, Constraints Specification at Higher Levels of Abstraction, Proceedings of International Workshop on High Level Design Validation and Test (November 2001).Google Scholar
  5. 5.
    Holzmann G.J. (May 1997). The Model Checker Spin. IEEE Trans. Software Eng. 23(5):279–258CrossRefGoogle Scholar
  6. 6.
    F. Balarin, L. Lavagno, C. Passerone, A. Sangiovanni-Vincentelli, M. Sgroi, and Y. Watanabe, Modeling and Designing Heterogeneous Systems, Technical Report 2001/01 Cadence Berkeley Laboratories (November 2001).Google Scholar
  7. 7.
    X. Chen, H. Hsieh, F. Balarin, and Y. Watanabe, Verifying LOC BasedFunctional and Performance Constraints, Proceedings of International Workshop on High Level Design Validation and Test (November 2003).Google Scholar
  8. 8.
    Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag (1992).Google Scholar
  9. 9.
    Chen X., Hsieh H., Balarin F., Watanabe Y. (August 2004). Logic of Constraints: A Quantitative Performance and Functional Constraint Formalism. IEEE Trans Computer-Aided Design Integrated Circuits. 23(8):1243–1255CrossRefGoogle Scholar
  10. 10.
    E. d. Kock, G. Essink, W. Smits, P. v. d. Wolf, J. Brunel, W. Kruijtzer, P. Lieverse, and K. Vissers, YAPI: Application Modeling for Signal Processing Systems, Proceedings of the 37 th Design Automation Conference, (June 2000).Google Scholar
  11. 11.
    G. Kahn, The Semantics of a Simple Language for Parallel Programming, Proceedings of IFIP Congress, North Holland Publishing Company pp. 471–475 (1974).Google Scholar
  12. 12.
    J. Brunel, E. A. de Kock, W. M. Kruijtzer, H. J. H. N. Kenter, and W. J. M. Smits, Communication Refinement In Video Systems on Chip, Proceedings of the 7th International Workshop on Hardware/Software Codesign, pp. 142–146 (1999).Google Scholar
  13. 13.
    O. Gangwal, A. Nieuwland, and P. Lippens, A Scalable and Flexible Data Synchronization Scheme for Embedded HW-SW Shared-Memory Systems, Proceedings of International Symposium on System Synthesis (October 2001).Google Scholar
  14. 14.
    C. Eisner and D. Fisman, Sugar 2.0 Proposal Presented to the Accellera Formal Verification Technical Committee (March 2002).Google Scholar
  15. 15.
    Abarbanel Y., Beer I., Gluhovsky L., Keidar S., Wolfsthal Y. (2003). FoCs-Automatic Generation of Simulation Checkers from Formal Specifications, Technical Report, IBM Haifa Research Laboratory, IsraelGoogle Scholar

Copyright information

© Springer Science+Business Media, Inc. 2006

Authors and Affiliations

  1. 1.University of CaliforniaRiversideUSA
  2. 2.Novas Software, Inc.San JoseUSA
  3. 3.Cadence Berkeley LaboratoriesBerkeleyUSA

Personalised recommendations