Proving transaction and system-level properties of untimed SystemC TLM designs

Electronic System Level (ESL) design manages the complexity of todays systems by using abstract models. In this context Transaction Level Modeling (TLM) is state-of-theart for describing complex communication without all the details. As ESL language, SystemC has become the de facto standard. Since the SystemC TLM models are used for early software development and as reference for hardware implementation their correct functional behavior is crucial. Admittedly, the best possible verification quality can be achieved with formal approaches. However, formal verification of TLM models is a hard task. Existing methods basically consider local properties or have extremely high run-time. In contrast, the approach proposed in this paper can verify "true" TLM properties, i.e. major TLM behavior like for instance the effect of a transaction and that the transaction is only started after a certain event can be proven. Our approach works as follows: After a fully automatic SystemC-to-C tr...

• Type: Journal
• Year: 2010
• Where: MEMOCODE
• Authors: Daniel Große, Hoang M. Le, Rolf Drechsler
• Keywords: Formal Methods, MEMOCODE 2010, SystemC TLM, SystemC TLM Models, TLM Models