International Journal of Intelligent Systems and Applications (IJISA)
IJISA Vol. 7, No. 12, 8 Nov. 2015
Cover page and Table of Contents: PDF (size: 772KB)
Formal and Informal Modeling of Fault Tolerant Noc Architectures
Full Text (PDF, 772KB), PP.32-42
Views: 0 Downloads: 0
Author(s)
Mostefa BELARBI
1,*
Index Terms
Self-Organized Network-On-Chip NoC, Testability, Formal proof, Event-B, Code generation, VHSIC Hardware Description Language VHDL
Abstract
The suggested new approach based on B-Event formal technics consists of suggesting aspects and constraints related to the reliability of NoC (Network-On-chip) and the over-cost related to the solutions of tolerances on the faults: a design of NoC tolerating on the faults for SoC (System-on-Chip) containing configurable technology FPGA (Field Programmable Gates Array), by extracting the properties of the NoC architecture. We illustrate our methodology by developing several refinements which produce QNoC (Quality of Service of Network on chip) switch architecture from specification to test. We will show how B-event formalism can follow life cycle of NoC design and test: for example the code VHDL (VHSIC Hardware Description Language) simulation established of certain kind of architecture can help us to optimize the architecture and produce new architecture; we can inject the new properties related to the new QNoC architecture into formal B-event specification. B-event is associated to Rodin tool environment. As case study, the last stage of refinement used a wireless network in order to generate complete test environment of the studied application.
Cite This Paper
Mostefa BELARBI, "Formal and Informal Modeling of Fault Tolerant Noc Architectures", International Journal of Intelligent Systems and Applications(IJISA), vol.7, no.12, pp.32-42, 2015. DOI:10.5815/ijisa.2015.12.03
Reference
[1]M. Heil and C. Tanougast: “Fault-tolerant self-organized mechanism for networked reconfigurable MPSoC” Codit’14. Metz.
[2]Killian, C. Tanougast, F. Monterio, and A. Dandache, “A new efficient and reliable dynamically Reconfigurable Network-on-Chip", Journal of Electrical and Computer Engineering, special issue Design and Automation for Integrated Circuits and Systems, Volume 2012, Article ID 843239, 16 pages, Hiwdawi, 2012.
[3]E. Bolotin, I. Cidon, R. Ginosar, A. Kolodny, “QNoC: QoS architecture and design process for network on chip” Journal of Systems architecture. 2003.
[4]Project RODIN. Rigorous open development environment for complex systems. http://www.eventb.org/, 2004-2010.
[5]M. Kamali, Luigia Petre, K. Sere, M. Daneshtalab Refinement-Based Modeling of 3D NoCs 2011 14th Euromicro Conference on Digital System Design.
[6]M Belarbi: Formal Modelling of Real-Time Embedded Automotive Architecture. Society of Design and Process Science Journal. JIDP, Volume 13, Number 2, 2009.
[7]H. Daoud, C. Tanougast, M. Belarbi and D. Mery, "Formal verification properties for Rapid Prototyping Using Fault Tolerant NoC-based Architecture", First International Workshop on Mathematics and Computer Science, Dec. 2012, University Ibn Khaldoun of Tiaret.
[8]Butler MJ (2009) Decomposition structures for Event-B. In: Leuschel M, Wehrheim H (eds) Proceedings of 7th international conference on integrated formal methods, IFM2009, Dusseldorf, Germany, February 16–19, 2009. Lecture notes in computer science, vol 5423. Springer, Berlin, pp 20–38.
[9]M. B. Andriamiarina, D. Méry, and N. K. Singh. Revisiting Snapshot Algorithms by Re?nement-based Techniques. In PDCAT. IEEE Computer Society, 2012.
[10]A. Hariche. M. Belarbi. and H. Daoud(2013), new Operators-Based Approach for the Event-B Refinement: QNoC Case Study IEEE ICM’2013, Beirut 15-18 Dec. 2013.
[11]A. Hariche. M. Belarbi. and H. Daoud(2012), Based B Extraction of QNoC architecture properties IWMCS’2012, Tiaret 16-17 Dec. 2012. Published by MomaJournal, Vol 1, Issue 2 (2012). ISSN N° 2253-0665.
[12]Abrial J.-R., The B book: assigning programs to meanings, Cambridge University Press, 1996.
[13]Abrial, J-R, Butler MJ, Hallerstede S, Hoang TS, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6):447–466.
[14]Bjerregaard and S. Mahadevan. A Survey of Research and Practices of Network-on-Chip. ACM Computer Surveys, 38(1), 2006.
[15]K. Goossens. Formal Methods for Networks on Chips. In Proceedings of the Fifth International Conference on Application of Concurrency to System Design, ACSD’05, pages 188–189. IEEE Computer Society, 200.
[16]Killian, C. Tanougast, F. Monterio, and A. Dandache, “Online routing fault detection for reconfigurable noc,” in International Conference on Field Programmable Logic and Applications, 2010.
[17]Killian, C. Tanougast, F. Monterio, and A. Dandache. Online routing fault detection for recon?gurable noc. In International Conference on Field Programmable Logic and Applications, 2010.
[18]J.S. Chenard, S. Bourduas, N. Azuelos, M. Boul′e, and Z. Zilic. Hardware Assertion Checkers in On-line Detection of Network-on-Chip Faults. In Proceedings of the Workshop on Diagnostic Services in Networks.
[19]Zhu, Q. and Matsuda, A. and Kuwamura, S. and Nakata, T. (2002) An Object-Oriented Design Process for System-on-Chip using UML Proceedings of 15th International Symposium on System Synthesis, New York, 2-4 October 2002, pp. 249-254. doi:10.1145/581199.58125.
[20]H.Daoud, C.Tanougast, M.Belarbi_, M. Heil_ “Formal Specification and Verification of wireless networked self-organized Systems on Chip” Cofid’14. Metz.
[21]X.-T. Tran, J. Durupt, Y. Thonnart, F. Bertrand, V. Beroulle, and C. Robach. Implementation of a Design-for-Test Architecture for Asynchronous Networks-on-Chip. In Proceeding of the 1st ACM/IEEE International Symposium on Networks-on-Chips, NOCS 2007, pp. 216{216, New Jersey, USA, May 2007.
[22]Morin-Allory, K. and Fesquet, L. and Borroine, D slopp(2006) Asynchronous Assertion Monitors For Multi-clock domain system veri?cation, 14-16 June. Seventeenth IEEE International Workshop on Rapid System Prototyping.
[23]R. Allur, D.L. Dill, “A theory of timed automata”, Theoretical Computer Science. 1994, Vol. 126, pp. 183-235.
[24]M. Butler and I. Maamria “Mathematical Extension in Event-B through the Rodin Theory Component” Research report 8 June 2010.
[25]Mentor Graphics www.mentorgraphics.com.
[26]M. Hosseinabady, A. Banaiyan, M.-N. Bojnordi, Z. Navabi ?A Concurrent Testing Method for NoC Switches”. in Proceedings of the conference on Design, automation and test in Europe: Proceedings, ser. DATE ’06. European Design and Automation Association, 2006, pp. 1171–1176.