License: 
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.TrustworthySW.2006.700
URN: urn:nbn:de:0030-drops-7000
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/700/
Schmaltz, Julien ;
Borrione, Dominique
Formalizing On Chip Communications in a Functional Style
Abstract
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.
BibTeX - Entry
@InProceedings{schmaltz_et_al:OASIcs:2006:700,
author = {Julien Schmaltz and Dominique Borrione},
title = {{Formalizing On Chip Communications in a Functional Style}},
booktitle = {Workshop on Trustworthy Software},
series = {OpenAccess Series in Informatics (OASIcs)},
ISBN = {978-3-939897-02-6},
ISSN = {2190-6807},
year = {2006},
volume = {3},
editor = {Serge Autexier and Stephan Merz and Leon van der Torre and Reinhard Wilhelm and Pierre Wolper},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2006/700},
URN = {urn:nbn:de:0030-drops-7000},
doi = {10.4230/OASIcs.TrustworthySW.2006.700},
annote = {Keywords: SoC's, communication architectures, formal methods, automated theorem proving}
}
|
Keywords: |
|
SoC's, communication architectures, formal methods, automated theorem proving |
|
Collection: |
|
Workshop on Trustworthy Software |
|
Issue Date: |
|
2006 |
|
Date of publication: |
|
26.09.2006 |
