Title :
A Generic Model for Formally Verifying NoC Communication Architectures: A Case Study
Author :
Borrione, Dominique ; Helmy, Amr ; Pierre, Laurence ; Schmaltz, Julien
Author_Institution :
TIMA Lab., Inst. Nat. Polytech. de Grenoble
Abstract :
Networks on chip are emerging as a promising solution for the design of complex systems on a chip, to interconnect manufactured IP cores, and the need to formally guarantee their correctness is crucial. In a NoC centered design, the individual IP´s are considered already validated. This paper addresses the validation of the communication infrastructure. A generic formal model for NoC´s has been developed and implemented in the ACL2 theorem prover. As an application, the HERMES network has been formalized in this model, and we show that both formal proofs and simulation experiments can be performed in ACL2
Keywords :
integrated circuit interconnections; logic design; logic testing; microprocessor chips; network-on-chip; ACL2 theorem prover; HERMES network; NoC communication architectures; complex system design; network-on-chip design; Binary trees; Computer architecture; Fabrics; Formal specifications; Formal verification; Laboratories; Logic; Network-on-a-chip; Protocols; Routing;
Conference_Titel :
Networks-on-Chip, 2007. NOCS 2007. First International Symposium on
Conference_Location :
Princeton, NJ
Print_ISBN :
0-7695-2773-6
DOI :
10.1109/NOCS.2007.1
