Sciweavers

Share
MEMOCODE
2010
IEEE

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

8 years 3 months ago
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...
Daniel Große, Hoang M. Le, Rolf Drechsler
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where MEMOCODE
Authors Daniel Große, Hoang M. Le, Rolf Drechsler
Comments (0)
books