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

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

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    26 Citaten (Scopus)

    Samenvatting

    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.
    Originele taal-2Engels
    TitelFirst International Symposium on Networks-on-Chips (NOCS '07, Princeton NJ, USA, May 7-9, 2007. Proceedings)
    UitgeverijIEEE Computer Society
    Pagina's127-136
    ISBN van geprinte versie978-0-7695-2773-4
    DOI's
    StatusGepubliceerd - 2007

    Vingerafdruk

    Duik in de onderzoeksthema's van 'A generic model for formally verifying NoC communication architectures: A case study'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit