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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
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–1543
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–52
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).
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).
Holzmann G.J. (May 1997). The Model Checker Spin. IEEE Trans. Software Eng. 23(5):279–258
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).
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).
Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag (1992).
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–1255
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).
G. Kahn, The Semantics of a Simple Language for Parallel Programming, Proceedings of IFIP Congress, North Holland Publishing Company pp. 471–475 (1974).
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).
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).
C. Eisner and D. Fisman, Sugar 2.0 Proposal Presented to the Accellera Formal Verification Technical Committee (March 2002).
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, Israel
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Chen, X., Hsieh, H. & Balarin, F. Verification Approach of Metropolis Design Framework for Embedded Systems. Int J Parallel Prog 34, 3–27 (2006). https://doi.org/10.1007/s10766-005-0002-x
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10766-005-0002-x