Abstract
We propose a new methodology for formally specifying on-chip bus protocols and for verifying protocol compliance of communication blocks in System-on-Chip (SoC) designs. In this methodology, the bus protocol is specified in a design-independent way by a set of protocol compliance properties based on a generic recorder finite state transition system. The properties are verified by combining local reachability analysis with a SAT-based property checking approach. This approach is called interval property checking and is based on a bounded circuit model generated from the design and the recorder. The proposed methodology clearly differentiates between design-specific and protocol-specific aspects of the overall verification task and exploits the nature of typical SoC protocol specifications and implementations. In this way, the proposed methodology contributes to reaching two important goals: making the computational complexity of formal verification algorithms tractable for large designs and reducing the manual effort of applying formal methods in industrial practice. Our approach has been applied successfully on several industrial designs.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
F. Aglietti, AHB System Generator. http://www.opencores.org/projects.cgi/web/ahb_system_generator/overview, 2004
ARM Limited, AMBA specification (rev 2.0). http://www.arm.com, 1999
A.Biere, A.Cimatti, E.Clarke, Y.Zhu, Symbolic model checking without BDDs, in Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 1999
R.K. Brayton, G.D. Hachtel, A.Sangiovanni-Vincentelli, F.Somenzi, A.Aziz, S.-T. Cheng, S.Edwards, S.Khatri, Y.Kukimoto, A.Pardo, S.Qadeer, R.K. Ranjan, S.Sarwary, T.R. Shiple, G.Swamy, T.Villa, VIS: a system for verification and synthesis, in Proceedings of the International Conference on Computer-Aided Verification (CAV), volume 1102, ed. by R.Alur, T.Henzinger (New Brunswick, NJ, 1996), pp. 428–432
G. Cabodi, S. Nocco, S. Quer, Improving SAT-based bounded model checking by means of BDD-based approximate traversals. J. Univ. Comput. Sci. 10, 1693–1730 (2004)
E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)
R.P. Kurshan, Computer-Aided Verification of Coordinating Processes – The Automata-Theoretic Approach (Princeton University Press, Princeton, NJ, 1994)
M.D. Nguyen, M. Thalmaier, M. Wedler, J. Bormann, D. Stoffel, W.Kunz, Unbounded protocol compliance verification using interval property checking with invariants. IEEE Trans. Comput. Aided Design 27(11), 2068–2082 (2008)
Onespin Solutions GmbH, Germany. OneSpin 360MV, www onespin-solutions.com
M.Sheeran, S.Singh, G.Stalmarck, Checking safety properties using induction and a SAT-solver, in Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2000
K.Shimizu, L.Dill, A.J. Hu, Monitor-based formal specification of PCI, in Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2000
M. Thalmaier, M.D. Nguyen, M. Wedler, D. Stoffel, W. Kunz, Formale Verifikation von SoC Protokollimplementierungen, in Tagungsband 1.GMM/GI/ITG-Fachtagung Zuverlaessigkeit und Entwurf, 2007
C.Wang, B.Li, H.Jin, G.Hachtel, F.Somenzi, Improving Ariadne’s bundle by following multiple threads in abstraction refinement. IEEE Trans. Comput. Aided Design 25, 2297–2316 (2006)
Y.-C. Yang, J.-D. Huang, C.-C. Yen, C.-H. Shih, J.-Y. Jou, Formal compliance verification of interface protocols, in Proceedings of the IEEE International Symposium on VLSI, 2005
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer Science+Business Media B.V.
About this chapter
Cite this chapter
Nguyen, M.D., Thalmaier, M., Wedler, M., Stoffel, D., Kunz, W., Bormann, J. (2010). A Re-Use Methodology for Formal SoC Protocol Compliance Verification. In: Borrione, D. (eds) Advances in Design Methods from Modeling Languages for Embedded Systems and SoC’s. Lecture Notes in Electrical Engineering, vol 63. Springer, Dordrecht. https://doi.org/10.1007/978-90-481-9304-2_12
Download citation
DOI: https://doi.org/10.1007/978-90-481-9304-2_12
Published:
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-9303-5
Online ISBN: 978-90-481-9304-2
eBook Packages: EngineeringEngineering (R0)