Formal modeling and verification for Network-on-chip

Yean-Ru Chen, Wan Ting Su, Pao Ann Hsiung, Ying Chemg Lan, Yu Hen Hu, Sao Jie Chen

Research output: Chapter in Book/Report/Conference proceedingConference contribution

12 Citations (Scopus)

Abstract

A model checking based formal verification procedure is developed to verify and validate the routing microarchitecture in a Network-on-chip (NoC) communication infrastructure. Specifically, four crucial properties of an NoC router, namely, mutual exclusion, starvation freedom, deadlock freedom, and conditions for traffic congestions are investigated. Given a recently proposed bi-directional channel direction control protocol, guidelines for constructing formal models of an NoC router are proposed, and minimal formal models essential for verifying these four properties are analyzed. A popular formal verification model checking tool State Graph Manipulators (SGM) is applied to perform the verification task. Results obtained through formal verification of these four properties provide useful insights to refine the protocol design.

Original languageEnglish
Title of host publication1st International Conference on Green Circuits and Systems, ICGCS 2010
Pages299-304
Number of pages6
DOIs
Publication statusPublished - 2010 Sep 20
Event1st International Conference on Green Circuits and Systems, ICGCS 2010 - Shanghai, China
Duration: 2010 Jun 212010 Jun 23

Publication series

Name1st International Conference on Green Circuits and Systems, ICGCS 2010

Other

Other1st International Conference on Green Circuits and Systems, ICGCS 2010
CountryChina
CityShanghai
Period10-06-2110-06-23

Fingerprint

Model checking
Routers
Network protocols
Traffic congestion
Manipulators
Communication
Network-on-chip
Formal verification

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Electrical and Electronic Engineering

Cite this

Chen, Y-R., Su, W. T., Hsiung, P. A., Lan, Y. C., Hu, Y. H., & Chen, S. J. (2010). Formal modeling and verification for Network-on-chip. In 1st International Conference on Green Circuits and Systems, ICGCS 2010 (pp. 299-304). [5543050] (1st International Conference on Green Circuits and Systems, ICGCS 2010). https://doi.org/10.1109/ICGCS.2010.5543050
Chen, Yean-Ru ; Su, Wan Ting ; Hsiung, Pao Ann ; Lan, Ying Chemg ; Hu, Yu Hen ; Chen, Sao Jie. / Formal modeling and verification for Network-on-chip. 1st International Conference on Green Circuits and Systems, ICGCS 2010. 2010. pp. 299-304 (1st International Conference on Green Circuits and Systems, ICGCS 2010).
@inproceedings{fffebbe4daba4e0a8705aa656c165361,
title = "Formal modeling and verification for Network-on-chip",
abstract = "A model checking based formal verification procedure is developed to verify and validate the routing microarchitecture in a Network-on-chip (NoC) communication infrastructure. Specifically, four crucial properties of an NoC router, namely, mutual exclusion, starvation freedom, deadlock freedom, and conditions for traffic congestions are investigated. Given a recently proposed bi-directional channel direction control protocol, guidelines for constructing formal models of an NoC router are proposed, and minimal formal models essential for verifying these four properties are analyzed. A popular formal verification model checking tool State Graph Manipulators (SGM) is applied to perform the verification task. Results obtained through formal verification of these four properties provide useful insights to refine the protocol design.",
author = "Yean-Ru Chen and Su, {Wan Ting} and Hsiung, {Pao Ann} and Lan, {Ying Chemg} and Hu, {Yu Hen} and Chen, {Sao Jie}",
year = "2010",
month = "9",
day = "20",
doi = "10.1109/ICGCS.2010.5543050",
language = "English",
isbn = "9781424468775",
series = "1st International Conference on Green Circuits and Systems, ICGCS 2010",
pages = "299--304",
booktitle = "1st International Conference on Green Circuits and Systems, ICGCS 2010",

}

Chen, Y-R, Su, WT, Hsiung, PA, Lan, YC, Hu, YH & Chen, SJ 2010, Formal modeling and verification for Network-on-chip. in 1st International Conference on Green Circuits and Systems, ICGCS 2010., 5543050, 1st International Conference on Green Circuits and Systems, ICGCS 2010, pp. 299-304, 1st International Conference on Green Circuits and Systems, ICGCS 2010, Shanghai, China, 10-06-21. https://doi.org/10.1109/ICGCS.2010.5543050

Formal modeling and verification for Network-on-chip. / Chen, Yean-Ru; Su, Wan Ting; Hsiung, Pao Ann; Lan, Ying Chemg; Hu, Yu Hen; Chen, Sao Jie.

1st International Conference on Green Circuits and Systems, ICGCS 2010. 2010. p. 299-304 5543050 (1st International Conference on Green Circuits and Systems, ICGCS 2010).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Formal modeling and verification for Network-on-chip

AU - Chen, Yean-Ru

AU - Su, Wan Ting

AU - Hsiung, Pao Ann

AU - Lan, Ying Chemg

AU - Hu, Yu Hen

AU - Chen, Sao Jie

PY - 2010/9/20

Y1 - 2010/9/20

N2 - A model checking based formal verification procedure is developed to verify and validate the routing microarchitecture in a Network-on-chip (NoC) communication infrastructure. Specifically, four crucial properties of an NoC router, namely, mutual exclusion, starvation freedom, deadlock freedom, and conditions for traffic congestions are investigated. Given a recently proposed bi-directional channel direction control protocol, guidelines for constructing formal models of an NoC router are proposed, and minimal formal models essential for verifying these four properties are analyzed. A popular formal verification model checking tool State Graph Manipulators (SGM) is applied to perform the verification task. Results obtained through formal verification of these four properties provide useful insights to refine the protocol design.

AB - A model checking based formal verification procedure is developed to verify and validate the routing microarchitecture in a Network-on-chip (NoC) communication infrastructure. Specifically, four crucial properties of an NoC router, namely, mutual exclusion, starvation freedom, deadlock freedom, and conditions for traffic congestions are investigated. Given a recently proposed bi-directional channel direction control protocol, guidelines for constructing formal models of an NoC router are proposed, and minimal formal models essential for verifying these four properties are analyzed. A popular formal verification model checking tool State Graph Manipulators (SGM) is applied to perform the verification task. Results obtained through formal verification of these four properties provide useful insights to refine the protocol design.

UR - http://www.scopus.com/inward/record.url?scp=77956591737&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=77956591737&partnerID=8YFLogxK

U2 - 10.1109/ICGCS.2010.5543050

DO - 10.1109/ICGCS.2010.5543050

M3 - Conference contribution

SN - 9781424468775

T3 - 1st International Conference on Green Circuits and Systems, ICGCS 2010

SP - 299

EP - 304

BT - 1st International Conference on Green Circuits and Systems, ICGCS 2010

ER -

Chen Y-R, Su WT, Hsiung PA, Lan YC, Hu YH, Chen SJ. Formal modeling and verification for Network-on-chip. In 1st International Conference on Green Circuits and Systems, ICGCS 2010. 2010. p. 299-304. 5543050. (1st International Conference on Green Circuits and Systems, ICGCS 2010). https://doi.org/10.1109/ICGCS.2010.5543050