A generic model for formally verifying NoC communication architectures: A case study

D. Borrione, A. Helmy, L. Pierre, J. Schmaltz

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    21 Citations (Scopus)

    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.
    Original languageEnglish
    Title of host publicationFirst International Symposium on Networks-on-Chips (NOCS '07, Princeton NJ, USA, May 7-9, 2007. Proceedings)
    PublisherIEEE Computer Society
    Pages127-136
    ISBN (Print)978-0-7695-2773-4
    DOIs
    Publication statusPublished - 2007

    Fingerprint Dive into the research topics of 'A generic model for formally verifying NoC communication architectures: A case study'. Together they form a unique fingerprint.

  • Cite this

    Borrione, D., Helmy, A., Pierre, L., & Schmaltz, J. (2007). A generic model for formally verifying NoC communication architectures: A case study. In First International Symposium on Networks-on-Chips (NOCS '07, Princeton NJ, USA, May 7-9, 2007. Proceedings) (pp. 127-136). IEEE Computer Society. https://doi.org/10.1109/NOCS.2007.1