Where academic tradition
meets the exciting future

Formal Analysis of a Local Segmented Bus Arbiter

Tomi Westerlund, Tiberiu Seceleanu, Formal Analysis of a Local Segmented Bus Arbiter. In: Proceedings of the 21st NORCHIP Conference, 268-271, 2003.

Abstract:

In this paper we show the derivation of a local segmented bus
arbiter from a single segment bus arbiter. The arbiter is extended
to cater for requests coming from and going to external segment. The
derivation demonstrates the capability of preserving correctness
when considering an important hardware design decision. The
operations are performed in the formal framework of Action Systems.
Action Systems is a predicate transformer based method for modelling
reactive systems. It has also been successfully applied to
both asynchronous and synchronous hardware designs.

Files:

Abstract in PDF-format

BibTeX entry:

@INPROCEEDINGS{inpWeSe03a,
  title = {Formal Analysis of a Local Segmented Bus Arbiter},
  booktitle = {Proceedings of the 21st NORCHIP Conference},
  author = {Westerlund, Tomi and Seceleanu, Tiberiu},
  pages = {268-271},
  year = {2003},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Edit publication