Abstract
Transaction level modeling allows exploring several SoC design architectures leading to better performance and easier verification of the final product. In this paper, we present an approach for design and verification of transaction level models. Verification is integrated as part of the design-flow. In the proposed method, we first model the design in UML. Then, we translate it into the Reactive Objects Language, Rebeca [5], which is an actor-based language with formal foundation. A model in Rebeca is a set of concurrently executed reactive objects (called rebecs) interacted by asynchronous message passing. After mapping UML to Rebeca, Rebeca code will be translated into Promela which is a language for formal verification. Checking the correctness of the design is performed on-the-fly with the LTL properties using the SPIN model checker. Finally, we translate the verified design to SystemC and map the properties to a set of assertions that can be re-used to validate the design at lower levels through simulation.
Original language | English (US) |
---|---|
Article number | 4253499 |
Pages (from-to) | 3760-3763 |
Number of pages | 4 |
Journal | Proceedings - IEEE International Symposium on Circuits and Systems |
DOIs | |
State | Published - 2007 |
Externally published | Yes |
Event | 2007 IEEE International Symposium on Circuits and Systems, ISCAS 2007 - New Orleans, LA, United States Duration: May 27 2007 → May 30 2007 |
ASJC Scopus subject areas
- Electrical and Electronic Engineering