The Community for Technology Leaders
RSS Icon
Issue No.12 - December (2011 vol.60)
pp: 1730-1743
Nicola Bombieri , University of Verona, Verona
Franco Fummi , University of Verona, Verona
Graziano Pravadelli , University of Verona, Verona
Transaction-level modeling (TLM) is the most promising technique to deal with the increasing complexity of modern embedded systems. However, modeling a complex system completely at transaction level could be inconvenient when IP cores are available on the market, since they are usually modeled at register transfer level (RTL). In this context, modeling and verification methodologies based on transactors allow designers to reuse RTL IPs into TLM-RTL mixed designs, thus guaranteeing a considerable saving of time. Practical advantages of such an approach are evident, but mixed TLM-RTL designs cannot completely provide the well-known effectiveness in terms of simulation speed provided by TLM. This paper presents a methodology to automatically abstract RTL IPs into equivalent TLM descriptions. To do that, the paper first proposes a formal definition of equivalence based on events, showing how such a definition can be applied to prove the correctness of a code manipulation methodology, such as code abstraction. Then, the paper proposes a technique to automatically abstract RTL IPs into TLM descriptions. Finally, the paper shows that the TLM descriptions obtained by applying the proposed technique are correct by construction, relying on the given definition of event-based equivalence. A set of experimental results is reported to confirm the effectiveness of the methodology.
Transaction-level modeling, embedded systems, TLM design.
Nicola Bombieri, Franco Fummi, Graziano Pravadelli, "Automatic Abstraction of RTL IPs into Equivalent TLM Descriptions", IEEE Transactions on Computers, vol.60, no. 12, pp. 1730-1743, December 2011, doi:10.1109/TC.2010.187
[1] L. Cai and D. Gajski, “Transaction Level Modeling: An Overview,” Proc. First IEEE/ACM/IFIP Int'l Conf. Hardware/Software Codesign and System Synthesis (CODES+ISSS), pp. 19-24, 2003.
[2] F. Balarin and R. Passerone, “Specification, Synthesis, and Simulation of Transactor Processes,” IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 26, no. 10, pp. 1749-1762, Oct. 2007.
[3] N. Bombieri, N. Deganello, and F. Fummi, “Integrating RTL IPs into TLM Designs through Automatic Transactor Generation,” Proc. Conf. Design, Automation and Test in Europe (DATE), pp. 15-20, 2008.
[4] M. Fujita, “Equivalence Checking between Behavioral and RTL Descriptions with Virtual Controllers and Datapaths,” ACM Trans. Design Automation of Electronic Systems , vol. 10, no. 4, pp. 610-626, 2005.
[5] R. Drechsler and D. Grosse, “System Level Validation Using Formal Techniques,” IEE Proc.-Computer and Digital Techniques, vol. 152, no. 3, pp. 393-406, 2005.
[6] C.-J. Seger, R. Jones, J. O'Leary, T. Melham, M. Aagaard, C. Barrett, and D. Syme, “An Industrially Effective Environment for Formal Hardware Verification,” IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 24, no. 9, pp. 1381-1405, Sept. 2005.
[7] R. Drechsler and S. Höreth, “Gatecomp: Equivalence Checking of Digital Circuits in an Industrial Environment,” Proc. Fifth Int'l Workshop Boolean Problems, 2002.
[8] A. Mishchenko, M. Case, R. Brayton, and S. Jang, “Scalable and Scalably-Verifiable Sequential Synthesis,” Proc. ACM/IEEE Int'l Conf. Computer-Aided Design (ICCAD), pp. 234-241, 2008.
[9] H. Savoj, D. Berthelot, A. Mishchenko, and R. Brayton, “Combinational Techniques for Sequential Equivalence Checking,” Proc. 19th ACM/IEEE Int'l Workshop Logic and Synthesis (IWLS), 2010.
[10] D. Anastasakis, R. Damiano, H.-K. Mah, and T. Stanion, “A Practical and Efficient Method for Compare-Point Matching,” Proc. 39th ACM/IEEE Ann. Design Automation Conf. (DAC), pp. 305-310, 2002.
[11] J.R. Burch and V. Singhal, “Robust Latch Mapping for Combinational Equivalence Checking,” Proc. IEEE/ACM Int'l Conf. Computer-Aided Design (ICCAD), pp. 563-569, 1998.
[12] S. Vasudevan, V. Viswanath, J. Abraham, and J. Tu, “Automatic Decomposition for Sequential Equivalence Checking of System Level and RTL Descriptions,” Proc. Fourth ACM and IEEE Int'l Conf. Formal Methods and Models Co-Design (MEMOCODE), pp. 71-80, 2006.
[13] D. Kroening and E. Clarke, “Checking Consistency of C and Verilog Using Predicate Abstraction and Induction,” Proc. IEEE/ACM Int'l Conf. Computer-Aided Design (ICCAD), pp. 66-72, 2004.
[14] A. Koelbl, Y. Lu, and A. Mathur, “Embedded Tutorial: Formal Equivalence Checking between System-Level Models and RTL,” Proc. IEEE/ACM Int'l Conf. Computer-Aided Design (ICCAD), pp. 965-971, 2005.
[15] P. Chauhan, D. Goyal, G. Hasteer, A. Mathur, and N. Sharma, “Non-Cycle-Accurate Sequential Equivalence Checking,” Proc. 46th ACM/IEEE Design Automation Conf. (DAC), pp. 460-465, 2009.
[16] N. Bombieri, F. Fummi, G. Pravadelli, and J. Marques-Silva, “Towards Equivalence Checking between TLM and RTL Models,” Proc. Fifth IEEE/ACM Int'l Conf. Formal Methods and Models for Codesign (MEMOCODE), pp. 113-122, 2007.
[17] G. Di. Guglielmo, F. Fummi, C. Marconcini, and G. Pravadelli, “EFSM Manipulation to Increase High-Level ATPG Efficiency,” Proc. Seventh Int'l Symp. Quality Electronic Design (ISQED), 2006.
[18] D. Gajski, J. Zhu, and R. Domer, “Essential Issue in Codesign,” Technical Report ICS-97-26, Univ. of California, Irvine, 1997.
[19] K.-T. Cheng and A.S. Krishnakumar, “Automatic Generation of Functional Vectors Using the Extended Finite State Machine Model,” ACM Trans. Design Automation of Electronic Systems, vol. 1, no. 1, pp. 57-79, 1996.
[20] OSCI, http:/, 2009.
[21] TLM-2.0, OSCI TLM-2.0 Language Reference Manual, Open SystemC Organization Initiative, http:/, 2009.
[22] W. Ecker, V. Esen, and M. Hull, “Execution Semantics and Formalisms for Multi-Abstraction TLM Assertions,” Proc. Fourth ACM and IEEE Int'l Conf. on Formal Methods and Models for Co-Design (MEMOCODE), pp. 93-79, 2006.
[23] L. Lamport, “Time, Clocks, and the Ordering of Events in a Distributed System,” Comm. ACM, vol. 21, no. 7, pp. 558-565, 1978.
[24] ESD Group, Univ. of Verona, EDALab s.r.l. “A$^2$ T.” http:/, 2010.
[25] M. Borgatti, A. Capello, U. Rossi, J.-L. Lambert, I. Moussa, F. Fummi, and G. Pravadelli, “An Integrated Design and Verification Methodology for Reconfigurable Multimedia System,” Proc. Conf. Design, Automation and Test in Europe (DATE), pp. 266-271, 2005.
[26] Politecnico di Torino “ITC-99 Benchmarks,” http://www.cad. , 1999.
[27] Coconut Project: Final Report, , 2010.
6 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool