FORMAL VERIFICATION OF A NETWORK ON CHIP
Need help with a related project topic or New topic? Send Us Your Topic
DOWNLOAD THE COMPLETE PROJECT MATERIAL
FORMAL VERIFICATION OF A NETWORK ON CHIP
Chapter one
Introduction
“Therefore, there is an ongoing need to strive for balance, conciseness, and even grace. The strategy we take, therefore, can be summarised as follows: Use theory to provide insight; use common sense and intuition where appropriate, but rely on formal theory when obstacles and complexities develop. David Gries (The Balance of Formality and Common Sense, 1981).
Computers are becoming increasingly omnipresent, and society’s reliance on them cannot be overstated. Imagine you’re in a futuristic car that uses x-by-wire (where x stands for steer, break, gear, and so on) technology and you hit the brakes, but the car refuses to stop because the chip responsible for the breaking system isn’t responding.
This failure could be the result of the computerised breaking system, which is most likely a System on Chip (SoC), becoming blocked, preventing communication between the chip’s internal modules.
But, luckily, this will never happen, not because the existing traditional simulation-based verification approaches are insufficient to verify these chips, but because more robust formal procedures will be used to assure that such a circumstance cannot occur by design.
The good news is that, while the communication structure of SoCs typically includes sophisticated state machines, flow control circuitry, and handshaking protocols, the design blocks that comprise such networking chips are well-suited to formal verification.
Specifying attributes that define appropriate operation of these chips, while not easy, is a process that designers and verification engineers can complete with little training [Nar04].
Introduction 2
In summary, the impetus for this effort is that society is becoming more reliant on computers. Computers are growing increasingly complicated, so we need to secure their dependability and boost people’s confidence in utilising them.
1.1 BACKGROUND OF THE STUDY.
As the number of modules integrated on a single die increases and VLSI technology advances to the deep submicron level, on-chip inter-module communication becomes a performance constraint. The current status of on-chip module interconnection is a shared bus with a central arbiter.
However, when the number of modules grows, this common shared bus method presents significant scalability issues, resulting in poor performance and energy inefficiencies.
Network on Chip (NoC) is being offered as a feasible solution to the challenge of on-chip communication scalability. NoC has received a lot of attention from the SoC community and even traditional data network sectors.
Many papers have already been written about their design and implementation, with some being synthesised on FPGAs and ASICs. Examples of NoCs are the Æthereal, Nostrum, Spidergon, Octagon, XPipes, and FAUST.
The NoC paradigm brings with it new research problems. Because of their nature, NoC are limited by low latency, area, power, and heat dissipation. To reduce communication latency, various switching and routing strategies are used, some of which leave the NoC susceptible to deadlocks.
Again, the restriction on region limits router buffer capacity, overloading the network and increasing the probability of deadlock. Livelocks can have major repercussions in terms of power consumption and heat dissipation.
While traditional data networks, such as the internet, may tolerate packet losses and resending of packets, this is not acceptable in a NoC environment. Verifying their design is crucial for a variety of reasons, as discussed in Introduction 3.
The size and complexity of SoCs are increasing at such a rapid pace that standard modelling and testing methodologies are reaching their limits. The only realistic option is to employ formal verification methods, which use mathematical approaches to prove the truth of properties in a system.
The purpose of this project is to broaden the application of formal methods by formally proving a NoC with model checking approaches. The OASIS NoC, which is an FPGA implementation of an earlier suggested Basic Network on Chip (BANC) by Abderazak and Sowa [AS06], would be utilised as a case study.
Deadlock-freedom and the network’s ability to function as a buffer without flit losses will be tested. The FDR model checker will be used to validate the NoC’s deadlock freedom.
We also demonstrate how the PRISM model checker, which is intended to test probabilistic features, can be applied to very non-probabilistic qualities by verifying OASIS NoC for deadlock freedom and buffer quality.
Need help with a related project topic or New topic? Send Us Your Topic