### 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 language | English |
---|---|

Pages (from-to) | 241-258 |

Number of pages | 18 |

Journal | Formal Aspects of Computing |

Volume | 20 |

Issue number | 3 |

DOIs | |

Publication status | Published - 2008 |

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

## Cite this

Schmaltz, J., & Borrione, D. (2008). A functional formalization of on chip communications.

*Formal Aspects of Computing*,*20*(3), 241-258. https://doi.org/10.1007/s00165-007-0049-0