A formal approach to the protocol converter problem

ABSTRACT

In the absence of a single module interface standard, integration of pre-designed modules in System-on-Chip design often requires the use of protocol converters. Existing approaches to automatic synthesis of protocol converters mostly lack formal foundations and either employ abstractions that ignore crucial low level behaviors, or grossly simplify the structure of the protocols considered. We present a state-machine based formal model for bus based communication protocols, and precisely define protocol compatibility, and correct protocol conversion. Our model is expressive enough to capture features of commercial protocols such as bursts, pipelined transfers, wait state insertion, and data persistence, in cycle accurate detail. We show that the most general, correct converter for a pair of protocols, can be described as the greatest fixed point of a function for updating buffer states. This characterization yields a natural algorithm for automatic synthesis of a provably correct converter by iterative computation of the fixed point. We report our experience with automatic converter synthesis between widely used commercial bus protocols, such as AMBA AHB, ASB, APB, and OCP, considering features which are beyond the scope of current techniques.

REFERENCES

• 1: Open core protocol international partnership, http://www.ocpip.org.
• 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: V. Androutsopoulos, D. Brookes, and T. Clarke. Protocol converter synthesis. Computers and Digital Techniques, 151(6):391--401, 2004.
• 4: ARM. Amba specification, http://www.arm.com/.
• 5: K. Avnit, V. D'Silva, A. Sowmya, S. Ramesh, and S. Parameswaran. Protocol compatibility and automatic converter synthesis. Technical Report 0718, UNSW, Australia, August 2007.
• 6: 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
• 7: Vijay D'silva , S. Ramesh , Arcot Sowmya, Synchronous Protocol Automata: A Framework for Modelling and Verification of SoC Communication Architectures, Proceedings of the conference on Design, automation and test in Europe, p.10390, February 16-20, 2004
• 8: D. Gajski, H. Cho, and S. Abdi. General transducer architecture. Technical Report TR 05--08, CECS Center for Embedded Computer Systems University of California, Irvine, August 2005.
• 9: 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]
• 10: 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]
• 11: 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]
• 12: 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]
• 13: 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

Primary Classification:
  B. Hardware
  B.4 INPUT/OUTPUT AND DATA COMMUNICATIONS
      B.4.3 Interconnections (subsystems)

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.1 Types and Design Styles
  B.8 Performance and Reliability
      B.8.2 Performance Analysis and Design Aids

General Terms:
Design, Performance