Abstract
TLM (Transaction-Level Modeling) was introduced to cope with the increasing complexity of Systems-on-Chip designs by raising the modeling level. Currently, TLM is primarily used for system-level functional testing and simulation using the SystemC C++ API widely accepted in industry. Nevertheless, TLM requires a careful handling of asynchronous concurrency. In this paper, we give a semantics to TLM models written in SystemC via a translation into the process algebra LOTOS, enabling the verification of the models with the CADP toolbox dedicated to asynchronous systems. Contrary to other works on formal verification of TLM models written in SystemC, our approach targets fully asynchronous TLM without the restrictions imposed by the SystemC simulation semantics. We argue that this approach leads to more dependable models.
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
Bolognesi, T., Brinksma, E.: Introduction to the ISO Specification Language Lotos. Computer Networks and ISDN Systems 14(1), 25–59 (1988)
Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. EATCS Monographs on Theoretical Computer Science, vol. 6 (1985)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158–163. Springer, Heidelberg (2007)
Ghenassia, F. (ed.): Transaction-Level Modeling with SystemC: TLM Concepts and Applications for Embedded Systems. Springer, Heidelberg (2005)
Große, D., Drechsler, R.: CheckSyC: An Efficient Property Checker for RTL SystemC Designs. ISCAS 4, 4167–4170 (2005)
Habibi, A., Tahar, S.: Design and Verification of SystemC Transaction-Level Models. IEEE Transactions on VLSI Systems 14(1), 57–68 (2006)
Helmstetter, C., Maraninchi, F., Maillet-Contoz, L., Moy, M.: Automatic Generation of Schedulings for Improving the Test Coverage of Systems-on-a-Chip. In: FMCAD, 171–178 (2006)
ISO/IEC. Lotos – A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, ISO, Genève (1989)
Karlsson, D., Eles, P., Peng, Z.: Formal Verification of SystemC Designs Using a Petri-net Based Representation. In: DATE, pp. 1228–1233 (2006)
Kroening, D., Sharygina, N.: Formal Verification of SystemC by Automatic Hardware/Software Partitioning. In: MEMOCODE, pp. 101–110 (2005)
Magee, J., Kramer, J.: Concurrency: State Models and Java Programs, 2nd edn., April 2006. Wiley, Chichester (2006)
Man, K.L.: SystemCFL: A Formalism for Hardware/Software Codesign. European Conference on Circuit Theory and Design 1, 193–196 (2005)
Moy, M., Maraninchi, F., Maillet-Contoz, L.: LusSy: A Toolbox for the Analysis of Systems-on-a-Chip at the Transactional Level. In: ACSD, June 2005, pp. 26–35 (2005)
Müller, W., Ruf, J., Hoffmann, D., Gerlach, J., Kropf, T., Rosenstiel, W.: The Simulation Semantics of SystemC. In: DATE, March 2001, pp. 64–70 (2001)
Niemann, B., Haubelt, C.: Towards a Unified Execution Model for Transactions in TLM. In: MEMOCODE, pp. 103–112 (2007)
Open SystemC Initiative. IEEE Standard SystemC Language Reference Manual. IEEE Computer Society. IEEE Std 1666-2005 (2006)
Rose, A., Swan, S., Pierce, J., Fernandez, J.-M.: Transaction Level Modeling in SystemC. In: Open SystemC Initiative (2005), http://www.systemc.org
Salem, A.: Formal Semantics of Synchronous SystemC. In: DATE, pp. 376–381 (2003)
Talpin, J.-P., Guernic, P.L., Shukla, S.K., Gupta, R.: A Compositional Behavioral Modeling Framework for Embedded System Design and Conformance Checking. International Journal of Parallel Programming 33(6), 613–643 (2005)
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)
Wodey, P., Camarroque, G., Baray, F., Hersemeule, R., Cousin, J.-P.: LOTOS Code Generation for Model Checking of STBus Based SoC: The STBus Interconnect. In: MEMOCODE, June 2003, pp. 204–213 (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ponsini, O., Serwe, W. (2008). A Schedulerless Semantics of TLM Models Written in SystemC Via Translation into LOTOS. In: Cuellar, J., Maibaum, T., Sere, K. (eds) FM 2008: Formal Methods. FM 2008. Lecture Notes in Computer Science, vol 5014. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68237-0_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-68237-0_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68235-6
Online ISBN: 978-3-540-68237-0
eBook Packages: Computer ScienceComputer Science (R0)