Towards a formal theory of on chip communications in the ACL2 logic

ABSTRACT

This paper is devoted to the expression for a formal theory of communication networks in the ACL2 logic. More precisely, we have developed a generic model called GeNoC, in a general mathematical notation, with the use of quantification over variables as well as over functions. We present here its expression in the first order quantifier free logic of the ACL2 theorem prover. We describe our systematic approach to cast it into ACL2, especially how we use the encapsulation principle to obtain a systematic methodology to specify and validate on chip communications architectures. We summarize the different instances of GeNoC developed so far in ACL2, some come from industrial designs. We illustrate our approach on an XY routing algorithm.

REFERENCES

• 1: H. Amjad. Model Checking the AMBA Protocol in HOL. Technical report, University of Cambridge, Computer Laboratory, September 2004.
• 2: William Dally , Brian Towles, Principles and Practices of Interconnection Networks, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2003
• 3: B. Gebremichael, F. Vaandrager, M. Zhang, K. Goossens, E. Rijpkema, and A. Rădulescu. Deadlock Prevention in the Æthereal protocol. In D. Borrione and W. Paul, editors, Correct Hardware Design and Verification Methods (CHARME'05), volume 3725 of LNCS, pages 345--348, 2005.
• 4: Faraydon Karim , Anh Nguyen , Sujit Dey, An Interconnect Architecture for Networking Systems on Chips, IEEE Micro, v.22 n.5, p.36-45, September 2002 [doi>10.1109/MM.2002.1044298]
• 5: J. S. Moore. A Formal Model of Asynchronous Communications and Its Use in Mechanically Verifying a Biphase Mark Protocol. Formal Aspects of Computing, 6(1):60--91, 1993.
• 6: James A. Rowson , Alberto Sangiovanni-Vincentelli, Interface-based design, Proceedings of the 34th annual conference on Design automation, p.178-183, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266060]
• 7: Abhik Roychoudhury , Tulika Mitra , S. R. Karri, Using Formal Techniques to Debug the AMBA System-on-Chip Bus Protocol, Proceedings of the conference on Design, Automation and Test in Europe, p.10828, March 03-07, 2003
• 8: J. Schmaltz. Une formalisation fonctionnelle des communications sur la puce. PhD thesis, Joseph Fourier University, Grenoble, France, January 2006. In French. A partial translation is available upon request to the first author.
• 9: J. Schmaltz and D. Borrione. Verification of a Parameterized Bus Architecture Using ACL2. In Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and its Applications, April 2003.
• 10: J. Schmaltz and D. Borrione. A Functional Approach to the Formal Specification of Networks on Chip. In A. Hu and A. Martin, editors, Formal Methods in Computer-Aided Design (FMCAD'04), volume 3312 of LNCS, pages 52--66, Austin, Tx, USA, November 2004. Springer-Verlag.
• 11: J. Schmaltz and D. Borrione. A Generic Network on Chip Model. In T. Melham and J. Hurd, editors, Theorem Proving in Higher Order Logics (TPHOLs'05), volume 3603 of LNCS, pages 310--325, Oxford, UK, August 2005. Springer-Verlag.
• 12: G. Spirakis. Beyond Verification: Formal Methods in Design. In A. Hu and A. Martin, editors, Formal Methods in Computer-Aided Design (FMCAD'04), volume 3312 of LNCS, Austin, Texas, USA, November 2004. Springer-Verlag. Invited Speaker.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.0 GENERAL

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids

General Terms:
Design, Verification

Keywords:
communication theory, formal theory, network on a chip, theorem proving