Towards a formally verified network-on-chip

T. Broek, van den; J. Schmaltz

doi:10.1109/FMCAD.2009.5351124

Towards a formally verified network-on-chip

T. Broek, van den, J. Schmaltz

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

6 Citations (Scopus)

Abstract

Multi-Processor Systems-on-Chip (MPSoC) designs are constructed by assembling pre-designed parameterized components. Communications are crucial to their overall functionality and performance. Formal verification methods have been intensively applied to processing elements, e.g., microprocessors. Very little work has been done with respect to communication modules. We present the formal specification of a packet switched NoC and its proven refinement. At the specification level, routing decisions are computed at once before packets get injected in the network. In the implementation, routing decisions are distributed over each individual node. We prove that the implementation behaves according to its specification for a 2D-mesh NoC. All models and proofs have been checked using the ACL2 theorem proving system. To the best of our knowledge, this work constitutes the first cross-layer verification of on-chip communication networks.

Original language	English
Title of host publication	Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD '09, Austin TX, USA, November 15-18, 2009)
Place of Publication	Piscataway
Publisher	Institute of Electrical and Electronics Engineers
Pages	184-187
ISBN (Print)	978-1-4244-4966-8
DOIs	https://doi.org/10.1109/FMCAD.2009.5351124
Publication status	Published - 2009
Externally published	Yes

Access to Document

10.1109/FMCAD.2009.5351124

Cite this

@inproceedings{c8c3df78407a4dae8b919fe5700789e3,

title = "Towards a formally verified network-on-chip",

abstract = "Multi-Processor Systems-on-Chip (MPSoC) designs are constructed by assembling pre-designed parameterized components. Communications are crucial to their overall functionality and performance. Formal verification methods have been intensively applied to processing elements, e.g., microprocessors. Very little work has been done with respect to communication modules. We present the formal specification of a packet switched NoC and its proven refinement. At the specification level, routing decisions are computed at once before packets get injected in the network. In the implementation, routing decisions are distributed over each individual node. We prove that the implementation behaves according to its specification for a 2D-mesh NoC. All models and proofs have been checked using the ACL2 theorem proving system. To the best of our knowledge, this work constitutes the first cross-layer verification of on-chip communication networks.",

author = "{Broek, van den}, T. and J. Schmaltz",

year = "2009",

doi = "10.1109/FMCAD.2009.5351124",

language = "English",

isbn = "978-1-4244-4966-8",

pages = "184--187",

booktitle = "Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD '09, Austin TX, USA, November 15-18, 2009)",

publisher = "Institute of Electrical and Electronics Engineers",

address = "United States",

}

Towards a formally verified network-on-chip. / Broek, van den, T.; Schmaltz, J.
Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD '09, Austin TX, USA, November 15-18, 2009). Piscataway: Institute of Electrical and Electronics Engineers, 2009. p. 184-187.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Towards a formally verified network-on-chip

AU - Broek, van den, T.

AU - Schmaltz, J.

PY - 2009

Y1 - 2009

N2 - Multi-Processor Systems-on-Chip (MPSoC) designs are constructed by assembling pre-designed parameterized components. Communications are crucial to their overall functionality and performance. Formal verification methods have been intensively applied to processing elements, e.g., microprocessors. Very little work has been done with respect to communication modules. We present the formal specification of a packet switched NoC and its proven refinement. At the specification level, routing decisions are computed at once before packets get injected in the network. In the implementation, routing decisions are distributed over each individual node. We prove that the implementation behaves according to its specification for a 2D-mesh NoC. All models and proofs have been checked using the ACL2 theorem proving system. To the best of our knowledge, this work constitutes the first cross-layer verification of on-chip communication networks.

AB - Multi-Processor Systems-on-Chip (MPSoC) designs are constructed by assembling pre-designed parameterized components. Communications are crucial to their overall functionality and performance. Formal verification methods have been intensively applied to processing elements, e.g., microprocessors. Very little work has been done with respect to communication modules. We present the formal specification of a packet switched NoC and its proven refinement. At the specification level, routing decisions are computed at once before packets get injected in the network. In the implementation, routing decisions are distributed over each individual node. We prove that the implementation behaves according to its specification for a 2D-mesh NoC. All models and proofs have been checked using the ACL2 theorem proving system. To the best of our knowledge, this work constitutes the first cross-layer verification of on-chip communication networks.

U2 - 10.1109/FMCAD.2009.5351124

DO - 10.1109/FMCAD.2009.5351124

M3 - Conference contribution

SN - 978-1-4244-4966-8

SP - 184

EP - 187

BT - Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD '09, Austin TX, USA, November 15-18, 2009)

PB - Institute of Electrical and Electronics Engineers

CY - Piscataway

ER -

Towards a formally verified network-on-chip

Abstract

Access to Document

Fingerprint

Cite this