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

13 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

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Formal modeling and verification for Network-on-chip'. Together they form a unique fingerprint.

Cite this