Abstract
SystemC is a popular language used in modeling system-on-chip implementations. To support this task at a high level of abstraction, transaction-level modeling (TLM) libraries have been recently developped. While TLM libraries are useful, it is difficult to capture the reactive nature of certain transactions with the constructs currently available in the SystemC and TLM libraries. In this paper, we propose an approach to specify and verify reactive transactions in SystemC designs. Reactive transactions are different from TLM transactions in the sense that a transaction can be killed or reset. Our approach consists of: (1) a language to describe reactive transactions that can be translated to verification monitors, (2) an architectural pattern to implement reactive transactions, and (3) the verification support to verify that the design does not deadlock, allows only legal behaviors and is always responsive. We illustrate our approach through an example of a transactional memory system where a transaction can be killed or reset before its completion. We identify the architectural patterns for reactive transactions. Our results demonstrate the feasibility of our approach as well as support for a comprehensive verification using RuleBase/NuSMV tools.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Groetker, T., Liao, S., Martin, G., Swan, S.: System Design with SystemC. Kluwer Academic Publishers, Dordrecht (2002)
Berry, G.: The Foundations of Esterel. MIT Press, Cambridge (2000)
Liao, S., Tjiang, S., Gupta, R.: An Efficient Implementation of Reactivity for Modeling Hardware in the Scenic Design Environment. In: Proc. of the Design Automation Conf. (1997)
Marschner, E., Deadman, B., Martin, G.: IP Reuse Hardening via Embedded Sugar Assertions. In: Proc. of the Int. Workshop on IP SOC Design (2002)
Balarin, F., Passerone, R.: Functional Verification Methodology Based on Formal Interface Specification and Transactor Generation. In: Proc. Design Automation and Test in Europe Conf. (2006)
Berry, G., Ramesh, S., Shyamasundar, R.K.: Communicating Reactive Processes. In: Proc. of the Symposium on Principles of Programming Languages (1993)
Seawright, A., Brewer, F.: Clairvoyant: A Synthesis System for Production-based Specifications. IEEE Trans. on Very Large Scale Integration (VLSI) Systems 2, 172–185 (1994)
Siegmund, R., Muller, D.: Automatic Synthesis of Communication Controller Hardware from Protocol Specification. IEEE Design and Test of Computer 19, 84–95 (2002)
Oliveira, M., Hu, A.: High-level Specification and Automatic Generation of IP Interface Monitors. In: Proc. of the Design Automation Conf. (2002)
Shimizu, K.: Writing, Verifying, and Exploiting Formal Specifications for Hardware Designs. PhD thesis, Stanford University (2002)
Zhu, Q., Oishi, R., Hasegawa, T., Nakata, T.: System-on-Chip Validation using UML and CWL. In: Proc. of the Int. Conf. on Hardware-Software Codesign and System Synthesis (2004)
Abarbanel, Y., Beer, I., Glushovsky, L., Keidar, S., Wolfsthal, Y.: FoCs: Automatic Generation of Simulation Checkers from Formal Specifications. In: Proc. of the Int. Conf. on Computer Aided Verification. pp. 538–542 (2000)
Cai, L., Gajski, D.: Transaction-level Modeling: an Overview. In: Proc. of the Int. Conf. on Hardware/Software Codesign and System Synthesis, pp. 19–24. ACM Press, New York (2003)
Habibi, A., Tahar, S.: Design and Verification of SystemC Transaction-level Models. IEEE Transactions on Very Large Scale Integration Systems 14, 57–68 (2006)
Moy, M., Maraninchi, F., Maillet-Contoz, L.: LusSy: A Toolbox for the Analysis of System-on-a-Chip at the Transactional Level. In: Proc. of the Int. Conf. on Application of Concurrency to System Design (2005)
Kroening, D., Sharygina, N.: Formal Verification of SystemC by Automatic Hardware/Software Partitioning. In: Proc. of the Int. Conf. on Formal Methods and Models for Codesign (2007)
Hoare, C.A.R.: Communicating Sequential Processes. Series in Computer Science. Prentice-Hall International, Englewood Cliffs (1985)
Shyamasundar, R., Doucet, F., Gupta, R., Krüger, I.H.: Compositional Reactive Semantics of SystemC and Verification in RuleBase. In: Proc. of the Workshop on Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Doucet, F., Shyamasundar, R.K., Krüger, I.H., Joshi, S., Gupta, R.K. (2008). Reactivity in SystemC Transaction-Level Models. In: Yorav, K. (eds) Hardware and Software: Verification and Testing. HVC 2007. Lecture Notes in Computer Science, vol 4899. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77966-7_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-77966-7_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77964-3
Online ISBN: 978-3-540-77966-7
eBook Packages: Computer ScienceComputer Science (R0)