Functional verification methodology based on formal interface specification and transactor generation

ABSTRACT

Transaction level models promise to be the basis of the verification environment for the whole design process. Realizing this promise requires connecting transaction level and RTL blocks through an object called a transactor, which translates back and forth between RTL signal-based communication, and transaction level function-call based communication. Each transactor is associated with a pair of interfaces, one at RTL and one at transaction level. Typically, however, a pair of interfaces is associated to more than one transactor, each assuming a different role in the verification process. In this paper we propose a methodology in which both the interfaces and their relation are captured by a single formal specification. By using the specification, we show how the code for all the transactors associated with a pair of interfaces can be automatically generated.

REFERENCES

• 1: Janaki Akella , Kenneth L. McMillan, Synthesizing Converters Between Finite State Protocols, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.410-413, October 14-16, 1991
• 2: AMBA Home Page. http://www.arm.com/products/-solutions/AMBAHomePage.html.
• 3: F. Balarin, M. Chiodo, P. Giusto, H. Hsieh, A. Jurecska, L. Lavagno, A. Sangiovanni-Vincentelli, E. M. Sentovich, and K. Suzuki. Synthesis of software programs for embedded control applications. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 18(6):834--49, June 1999.
• 4: G. Borriello and R. H. Katz. Synthesis and optimization of interface transducer logic. In Proceedings of the International Conference on Conputer Aided Design, November 1987.
• 5: Cohesive. http://www.spiratech.com.
• 6: Robert W. Floyd , Jeffrey D. Ullman, The Compilation of Regular Expressions into Integrated Circuits, Journal of the ACM (JACM), v.29 n.3, p.603-622, July 1982 [doi>10.1145/322326.322327]
• 7: Thorsten Grotker, System Design with SystemC, Kluwer Academic Publishers, Norwell, MA, 2002
• 8: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 9: IBM. On-chip peripheral bus. available at http://www-306.ibm.com/chips/techlib/techlib.nsf/-productfamilies/CoreConnect_Bus_Architecture.
• 10: T. Michiels. Generating TLM bus models from formal protocol specifications, Feb. 2004. presented at 9thEuropean SystemC Users Group Meeting, slides available at http://www-ti.informatik.uni-tuebingen.de/systemc/ninth_escugm.html.
• 11: Sanjiv Narayan , Daniel D. Gajski, Interfacing incompatible protocols using interface process generation, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.468-473, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217572]
• 12: Marcio T. Oliveira , Alan J. Hu, High-Level specification and automatic generation of IP interface monitors, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.513952]
• 13: Roberto Passerone , Luca de Alfaro , Thomas A. Henzinger , Alberto L. Sangiovanni-Vincentelli, Convertibility verification and converter synthesis: two faces of the same coin, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.132-139, November 10-14, 2002, San Jose, California [doi>10.1145/774572.774592]
• 14: Roberto Passerone , James A. Rowson , Alberto Sangiovanni-Vincentelli, Automatic synthesis of interfaces between incompatible protocols, Proceedings of the 35th annual conference on Design automation, p.8-13, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277047]
• 15: A. Pnueli. The temporal logic of programs. In 18th IEEE Symposium on Foundations of Computer Science, pages 46--57, Oct. 1977.
• 16: Property Specification Language: Reference Manual. available at http://www.accellera.org/pslv101.pdf.
• 17: A. Seawright and F. Brewer. Clairvoyant: a synthesis system for production-based specification. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 2(2):172--185, June 1994.
• 18: Standard Co-Emulation Modelling Interface (SCE-MI): Reference Manual (DRAFT), May 2003. available at http://www.eda.org/itc/scemi.pdf.
• 19: System Verilog 3.1: Accellera's Extensions to Verilog. http://www.eda.org/sv/SystemVerilog_3.1_final.pdf.
• 20: TestBuilder. http://www.testbuilder.net.
• 21: The ATM Forum Techncal Committee. Utopia Level 2, Version 1.0, June 1995. available at http://www.atmforum.com/standards/approved.html.
• 22: TransactorWizard. http://www.sdvinc.com.