https://scholars.lib.ntu.edu.tw/handle/123456789/358074
標題: | Formal modeling and verification for Network-on-chip | 作者: | Chen, Y.-R. Su, W.-T. Hsiung, P.-A. Lan, Y.-C. Hu, Y.-H. Chen, S.-J. SAO-JIE CHEN |
公開日期: | 2010 | 起(迄)頁: | 299-304 | 來源出版物: | 1st International Conference on Green Circuits and Systems, ICGCS 2010 | 摘要: | 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. © 2010 IEEE. |
URI: | http://www.scopus.com/inward/record.url?eid=2-s2.0-77956591737&partnerID=MN8TOARS http://scholars.lib.ntu.edu.tw/handle/123456789/358074 |
DOI: | 10.1109/ICGCS.2010.5543050 | SDG/關鍵字: | Bi-directional channels; Communication infrastructure; Deadlock freedom; Formal model; Formal modeling and verification; Formal verification procedures; Formal verifications; Micro architectures; Mutual exclusions; Network on chip; Protocol design; Starvation-freedom; State graphs; Verification task; Model checking; Servers; Traffic congestion; VLSI circuits; Routers |
顯示於: | 電機工程學系 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。