A functional approach to the formal specification of networks on chip

J. Schmaltz, D. Borrione

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

    12 Citations (Scopus)

    Abstract

    We present a functional approach, based on the ACL2 logic, for the specification of system on a chip communication architectures. Our decomposition of the communications allows the method to be modular for both system definition and validation. When performed in the context of the ACL2 logic, all the definitions and theorems are not only reusable, but also constitute an executable and proven valid specification for the system. We illustrate the approach on a state of the art network on chip: the Octagon. We prove that messages travel over this network without being modified and eventually reach their expected destination.
    Original languageEnglish
    Title of host publicationFormal Methods in Computer-Aided Design (5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004. Proceedings)
    EditorsA.J. Hu, A.K. Martin
    Pages53-66
    DOIs
    Publication statusPublished - 2004

    Publication series

    NameLecture Notes in Computer Science
    Volume3312
    ISSN (Print)0302-9743

    Fingerprint Dive into the research topics of 'A functional approach to the formal specification of networks on chip'. Together they form a unique fingerprint.

    Cite this