A functional formalization of on chip communications

J. Schmaltz, D. Borrione

    Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

    16 Citaten (Scopus)


    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.
    Originele taal-2Engels
    Pagina's (van-tot)241-258
    Aantal pagina's18
    TijdschriftFormal Aspects of Computing
    Nummer van het tijdschrift3
    StatusGepubliceerd - 2008

    Vingerafdruk Duik in de onderzoeksthema's van 'A functional formalization of on chip communications'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit