Executable formal specification and validation of NoC communication infrastructures

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

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

    11 Citations (Scopus)


    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.
    Original languageEnglish
    Title of host publicationProceedings of the 21st Annual Symposium on Integrated Circuits and Systems Design (SBCCI '08, Gramado, Brazil, September 1-4, 2008)
    EditorsM. Lubaszewski, M. Renovell, R.K. Gupta
    Place of PublicationNew York NY
    PublisherAssociation for Computing Machinery, Inc
    ISBN (Print)978-1-60558-231-3
    Publication statusPublished - 2008


    Dive into the research topics of 'Executable formal specification and validation of NoC communication infrastructures'. Together they form a unique fingerprint.

    Cite this