Formal Verification Of Fault Tolerant Noc-base Architecture

Approaches to design fault tolerant Network-on- Chip (NoC) for System-on-Chip(SoC)-based reconfigurable Field- Programmable Gate Array (FPGA) technology are challenges on the conceptualisation of the Multiprocessor System-on-Chip (MPSoC) design. For this purpose, the use of rigorous formal approaches, based on incremental design and proof theory, has become an essential step in a validation architecture. The Event- B formal method is a promising formal approach that can be used to develop, model and prove accurately the domain of SoCs and MPSoCs. This paper gives a formal verification of a NoC architecture, using the Event-B methodology. The formalisation process is based on an incremental and validated correct-by- construction development of the NoC architecture.