Provably correct on-chip communication: A formal approach to automatic protocol converter synthesis

ABSTRACT

Hardware module reuse is a standard solution to the problems of increasing complexity of chip architectures and pressure to reduce time to market. In the absence of a single module interface standard, predesigned modules for “plug-and-play” usually require a converter between incompatible interface protocols. Current approaches to automatic synthesis of protocol converters mostly lack formal foundations and either employ abstractions far removed from the HDL implementation level or grossly simplify the structure of the protocols considered. This work presents a state-machine-based formalism for modeling bus-based communication protocols and a notion of protocol compatibility and of correct conversion between incompatible protocols. This formalism is used to derive algorithms for checking protocol compatibility and for provably correct, automatic converter synthesis. Experiments with automatic converter synthesis between different configurations of widely used commercial bus protocols, such as AMBA AHB, ASB APB, and the Open Core Protocol (OCP) are discussed. The work here is unique in its combination of a completely formal approach and the use of a low abstraction level that enables precise modeling of protocol characteristics that is also close to HDL.

REFERENCES

• 1: Abdel-Hamid, A., Zaki, M., and Tahar, S. 2004. A tool converting finite state machine to VHDL. In Proceedings of the Canadian Conference on Electrical and Computer Engineering. Vol. 4, 1907--1910.
• 2: 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
• 3: Androutsopoulos, V., Brookes, D., and Clarke, T. 2004. Protocol converter synthesis. Comput. Digital Techniq. 151, 6, 391--401.
• 4: ARM. 1999. AMBA specification. http://www.arm.com/.
• 5: Karin Avnit , Vijay D'Silva , Arcot Sowmya , S. Ramesh , Sri Parameswaran, A formal approach to the protocol converter problem, Proceedings of the conference on Design, automation and test in Europe, March 10-14, 2008, Munich, Germany [doi>10.1145/1403375.1403447]
• 6: Davey, B. and Priestley, H. 2002. Introduction to Lattices and Order. Cambridge University Press.
• 7: Doucet, F., Shukla, S., Otsuka, M., and Gupta, R. 2003. BALBOA: A component-based design environment for system models. IEEE Trans. Comput.-Aid. Des. Integr. Circ. Syst. 22, 12, 1597--1612.
• 8: Vijay D'silva , S. Ramesh , Arcot Sowmya, Bridge Over Troubled Wrappers: Automated Interface Synthesis, Proceedings of the 17th International Conference on VLSI Design, p.189, January 05-09, 2004
• 9: D'Silva, V., Ramesh, S., and Sowmya, A. 2005. Synchronous protocol automata: A framework for modeling and verification of SoC communication architectures. In Proceedings of the Computers and Digital Techniques. 390--395.
• 10: Gansner, E. K. and North, S. C. 2002. Drawing graphs with dot. Tech. rep. AT&T Bell Laboratories, Murray Hill, NJ.
• 11: Gajski, D., Cho, H., and Abdi, S. 2005. General transducer architecture. Tech. rep. TR 05-08, CECS Center for Embedded Computer Systems, University of California, Irvine.
• 12: Lee, E. A. The Ptolemy project. http://ptolemy.eecs.berkeley.edu/.
• 13: Deepak Mathaikutty , Hiren Patel , Sandeep Shukla , Axel Jantsch, EWD: A metamodeling driven customizable multi-MoC system modeling framework, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.12 n.3, p.1-43, August 2007 [doi>10.1145/1255456.1255470]
• 14: Deepak A. Mathaikutty , Sandeep K. Shukla, MCF: a metamodeling-based component composition framework-composing SystemC IPs for executable system models, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.16 n.7, p.792-805, July 2008 [doi>10.1109/TVLSI.2008.2000344]
• 15: 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]
• 16: OCPIP. 2005. Open Core Protocol International Partnership. http://www.ocpip.org.
• 17: 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]
• 18: 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]
• 19: Sander, I. and Jantsch, A. 2004. System modeling and transformational design refinement in ForSyDe {formal system design}. IEEE Trans. Comput.-Aid. Des. Integr. Circ. Syst. 23, 1, 17--32.
• 20: Shin, D. and Gajski, D. 2002. Interface synthesis from protocol specification. Tech. rep. CECS-02-13, Center for Embedded Computer Systems, University of California, Irvine. dongwans,[e-mail].
• 21: James Smith , Giovanni De Micheli, Automated composition of hardware components, Proceedings of the 35th annual conference on Design automation, p.14-19, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277048]
• 22: Sonics. Smart interconnects. http://www.sonicsinc.com/.
• 23: S. Watanabe , K. Seto , Y. Ishikawa , S. Komatsu , M. Fujita, Protocol Transducer Synthesis using Divide and Conquer approach, Proceedings of the 2007 conference on Asia South Pacific design automation, p.280-285, January 23-26, 2007 [doi>10.1109/ASPDAC.2007.357999]

INDEX TERMS

General Terms:
Algorithms, Design, Reliability

Keywords:
System-on-chip, automatic design, converter synthesis, protocol compatibility