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. W. Dally and B. Towles. Principles and Practices of Interconnection Networks. Morgan-Kaufmann Publisher, 2004.
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. K. Karim, A. Nguyen, and S. Dey. An Interconnect Architecture for Networking Systems On Chip. IEEE Micro, pages 36--45, September-October 2002.
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. J. Rowson and A. Sangiovanni-Vincentelli. Interface-Based Design. In 34th Design Automation Conference (DAC'96), pages 178--183, 1997.
7. A. Roychoudhury, T. Mitra, and S. Karri. Using Formal Techniques to Debug the AMBA System-on-Chip Bus Protocol. In Design Automation and Test Europe (DATE'03), pages 828--833, 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

• Hardware

  • Electronic design automation

    • Physical design (EDA)

• Theory of computation