Formalizing on chip communications in a functional style

J. Schmaltz, D. Borrione

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    Samenvatting

    This paper presents a formal model for representing {it any} on-chip communication architecture. This model is described mathematically by a function, named $mathit{GeNoC}$. The correctness of $mathit{GeNoC}$ is expressed as a theorem, which states that messages emitted on the architecture reach their expected destination without modification of their content. The model identifies the key constituents common to {it all} communication architectures and their essential properties, from which the proof of the $GeNoC$ theorem is deduced. Each constituent is represented by a function which has no {it explicit} definition but is constrained to satisfy the essential properties. Thus, the validation of a {it 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 define a methodology that yields a systematic approach to the validation of communication architectures at a high level of abstraction. To validate our approach, we exhibit several architectures that constitute concrete instances of the generic model $GeNoC$. Some of these applications come from industrial designs, such as the AMBA AHB bus or the Octagon network from ST Microelectronics.
    Originele taal-2Engels
    TitelWorkshop Trustworthy Software 2006 (Saarbrücken, Germany, May 18-19, 2006)
    RedacteurenS. Autexier, S. Merz, L.W.N. Torre, van der, R. Wilhelm, P. Wolper
    Plaats van productieSchloss Dagstuhl
    UitgeverijInternationales Begegnungs- und Forschungszentrum für Informatik (IBFI)
    Pagina's1-25
    ISBN van geprinte versie978-3-939897-02-6
    DOI's
    StatusGepubliceerd - 2006

    Vingerafdruk Duik in de onderzoeksthema's van 'Formalizing on chip communications in a functional style'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit