A functional formalization of on chip communications

J. Schmaltz, D. Borrione

    Research output: Contribution to journalArticleAcademicpeer-review

    16 Citations (Scopus)

    Abstract

    This paper presents a formal model and a systematic approach to the validation of communication architectures at a high level of abstraction. This model is described mathematically by a function, named GeNoC. The correctness of GeNoC is expressed as a theorem, which states that messages emitted on the architecture reach their expected destination without any modification of their content. The model identifies the key constituents common to all on chip communication architectures, and their essential properties from which the correctness theorem is deduced. Each constituent is represented by a function that has no explicit definition but is constrained to satisfy the essential properties. Thus, the validation of a particular architecture is reduced to the proof that its concrete definition satisfies the essential properties. In practice, the model has been defined in the logic of the ACL2 theorem proving system. We illustrate our approach on several architectures that constitute concrete instances of the generic GeNoC model. Some of these applications come from industrial designs, such as the AMBA AHB bus or the Octagon network from ST Microelectronics.
    Original languageEnglish
    Pages (from-to)241-258
    Number of pages18
    JournalFormal Aspects of Computing
    Volume20
    Issue number3
    DOIs
    Publication statusPublished - 2008

    Fingerprint Dive into the research topics of 'A functional formalization of on chip communications'. Together they form a unique fingerprint.

  • Cite this