Executable formal specification and validation of NoC communication infrastructures

ABSTRACT

We describe an enhanced generic model for Networks-on-Chip (NoCs), implemented in the executable logic of the ACL2 theorem prover. The model is meant for serving as a formal reference for the specification, validation, and simulation at the initial design phase. Instantiated on a specific NoC, the model may be used for formal proofs and for simulation. The methodology is illustrated on HERMES.

REFERENCES

• 1: H. Amjad. Model Checking the AMBA Protocol in HOL. Technical report, University of Cambridge, Computer Laboratory, September 2004.
• 2: Dominique Borrione , Amr Helmy , Laurence Pierre , Julien Schmaltz, A Generic Model for Formally Verifying NoC Communication Architectures: A Case Study, Proceedings of the First International Symposium on Networks-on-Chip, p.127-136, May 07-09, 2007 [doi>10.1109/NOCS.2007.1]
• 3: B. Gebremichael, F. Vaandrager, M. Zhang, K. Goossens, E. Rijpkema, and A. Radulescu. Deadlock Prevention in the AEthereal Protocol. In Proc. CHARME'05, October 2005.
• 4: N. Genko, D. Atienza, and G. De Micheli. NoC Emulation on FPGA: HW/SW Synergy for NoC Features Exploration. In Proc. ParCo'2005, 2005.
• 5: D. Herzberg , M. Broy, Modeling layered distributed communication systems, Formal Aspects of Computing, v.17 n.1, p.1-18, May 2005 [doi>10.1007/s00165-004-0051-8]
• 6: 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]
• 7: Matt Kaufmann , J. Strother Moore , Panagiotis Manolios, Computer-Aided Reasoning: An Approach, Kluwer Academic Publishers, Norwell, MA, 2000
• 8: 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.
• 9: Fernando Moraes , Ney Calazans , Aline Mello , Leandro Möller , Luciano Ost, HERMES: an infrastructure for low area overhead packet-switching networks on chip, Integration, the VLSI Journal, v.38 n.1, p.69-93, October 2004 [doi>10.1016/j.vlsi.2004.03.003]
• 10: J. Perez Ramas, D. Atienza, M. Peon, I. Magan, J. Mendias, and R. Hermida. Versatile FPGA--Based Functional Validation Framework for Networks-on-Chip Interconnections Designs. In Proc. ParCo'2005 (mini-symposium NoC), 2005.
• 11: 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
• 12: Julien Schmaltz , Dominique Borrione, Towards a formal theory of on chip communications in the ACL2 logic, Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications, August 15-16, 2006, Seattle, Washington [doi>10.1145/1217975.1217985]
• 13: Julien Schmaltz , Dominique Borrione, A functional formalization of on chip communications, Formal Aspects of Computing, v.20 n.3, p.241-258, May 2008 [doi>10.1007/s00165-007-0049-0]

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Verification

General Terms:
Verification

Keywords:
simulation, theorem proving, verification