Abstract
SystemC is a de-facto standard language for high-level modeling of systems on chip. We investigate the feasibility of explicit state model checking of SystemC programs, proposing several ways to convert SystemC into Promela. We analyze the expressiveness of the various encoding styles, and we experimentally evaluate their impact on the search carried out by SPIN on a significant set of benchmarks. We also compare the results with recent approaches to symbolic verification of SystemC. Our approach never returns false positives, detects assertion violations much faster than recent formal approaches, and has the novel feature of pinpointing non-progressing delta cycles.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: QEST, pp. 125–126. IEEE, New York (2006)
Blanc, N., Kroening, D.: Race Analysis for SystemC using Model Checking. In: ICCAD, pp. 356–363. IEEE, New York (2008)
Blanc, N., Kroening, D., Sharygina, N.: Scoot: A Tool for the Analysis of SystemC Models. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 467–470. Springer, Heidelberg (2008)
Cimatti, A., Griggio, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos: A Software Model Checker for SystemC. In: CAV (to appear, 2011)
Cimatti, A., Micheli, A., Narasamdya, I., Roveri, M.: Verifying SystemC: a Software Model Checking Approach. In: FMCAD, pp. 51–59 (2010)
Cimatti, A., Narasamdya, I., Roveri, M.: Boosting lazy abstraction for systemC with partial order reduction. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 341–356. Springer, Heidelberg (2011)
Clarke, E., Kröning, D., Sharygina, N., Yorav, K.: SATABS: SAT-Based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005)
Große, D., Drechsler, R.: CheckSyC: An Efficient Property Checker for RTL SystemC Designs. In: ISCAS, vol. 4, pp. 4167–4170. IEEE, New York (2005)
Grosse, D., Le, H., Drechsler, R.: Proving Transaction and System-level Properties of Untimed SystemC TLM Designs. In: MEMOCODE, pp. 113–122 (2010)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: POPL, pp. 58–70 (2002)
Herber, P., Fellmuth, J., Glesner, S.: Model Checking SystemC Designs using Timed Automata. In: CODES+ISSS, pp. 131–136. ACM, New York (2008)
Holzmann, G.J.: Software Model Checking with SPIN. Adv. in Comp. 65, 78–109 (2005)
Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, pp. 197–211. Chapman & Hall, Ltd, London (1995)
Kroening, D., Sharygina, N.: Formal Verification of SystemC by Automatic Hardware/Software Partitioning. In: MEMOCODE, pp. 101–110. IEEE, New York (2005)
Kundu, S., Ganai, M.K., Gupta, R.: Partial Order Reduction for Scalable Testing of SystemC TLM Designs. In: DAC, pp. 936–941. ACM, New York (2008)
Marquet, K., Jeannet, B., Moy, M.: Efficient Encoding of SystemC/TLM in Promela. Technical report, Verimag, Verimag Research Report no TR-2010-7 (2010)
Moy, M., Maraninchi, F., Maillet-Contoz, L.: LusSy: A Toolbox for the Analysis of Systems-on-a-Chip at the Transactional Level. In: ACSD, pp. 26–35. IEEE, New York (2005)
Moy, M., Maraninchi, F., Maillet-Contoz, L.: Pinapa: An Extraction Tool for SystemC Descriptions of Systems-on-a-Chip. In: EMSOFT, pp. 317–324. ACM, New York (2005)
Tabakov, D., Kamhi, G., Vardi, M.Y., Singerman, E.: A Temporal Language for SystemC. In: FMCAD, pp. 1–9. IEEE, New York (2008)
Tabakov, D., Vardi, M.: Monitoring Temporal SystemC Properties. In: MEMOCODE, pp. 123–132 (2010)
Traulsen, C., Cornet, J., Moy, M., Maraninchi, F.: A SystemC/TLM Semantics in Promela and Its Possible Applications. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 204–222. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Campana, D., Cimatti, A., Narasamdya, I., Roveri, M. (2011). An Analytic Evaluation of SystemC Encodings in Promela. In: Groce, A., Musuvathi, M. (eds) Model Checking Software. SPIN 2011. Lecture Notes in Computer Science, vol 6823. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22306-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-22306-8_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22305-1
Online ISBN: 978-3-642-22306-8
eBook Packages: Computer ScienceComputer Science (R0)