Models & Optimisation and Mathematical Analysis Journal
Volume 1, Numéro 2, Pages 8-13

Based B Extraction Of Qnoc Architecture Properties

Authors : Hariche Abdelhamid . Belarbi Mostefa . Daoud Hayat .


Embedded systems become more and more present in our daily life. The validation of this kind of systems with time their evolution became fast and complex we focus on multiprocessor systems on chip (MPSoC) and exactly Qaulity of Service of Network on chip architecture (QNoC). The interconnection of communication modules (IP - Intellectual Property) constitutes a fundamental part during the design of such systems expressed in terms on band-width, latency, power consumption and reliability. The validation currently for MPSoC (with QNoC’s basis) based on the logical simulation which it can’t allow a global validation for this system even it is not adapted for the design of high level integration complex systems (Handicaps with respect to the concept time to market). The new validation approach using the formal technics using B event method consists of suggesting aspects and constraints related to the reliability of NoC and the over-cost related to the solutions of tolerances on the faults (a design of NoC tolerating on the faults for SoC containing configurable technology FPGA) by extracting the properties of the QNoC architecture existed in the VHDL code associated and prove these last using the prover that used in B event method. This approach makes it possible to exploit.


MPSoC, Formal Technics, Generating Model, QNOC, VHDL, B Event, incrementale