FORMAL VERIFICATION OF A NETWORK ON CHIP

Abstract

Current advancement in VLSI technology allows more circuit to be integrated on a single chip forming a System on Chip (SoC). The state of art in on-chip intermodule connection of using a shared bus with a common arbiter poses scalability problems and become a performance bottleneck as the number of modules increase. Network on Chip (NoC) has been proposed as a viable solution to this problem. The possibility of occurrence of deadlocks and livelocks in a NoC requires that their design be validated since these can cause serious consequences such as power consumption and heat dissipation. The traditional ways of validating chips by simulation-based techniques are been stretched passed their limits and the only alternative left is formal verification. This project pushes forward the range of applicability of formal verification by formally verifying the OASIS NoC using the model checking technique. Both refinement model checking and probabilistic model checking techniques are used to verify OASIS NoC for properties of the System. The OASIS NoC is first formalised in CSP and then verified with the FDR model checker for deadlock freedom. It is also shown that PRISM model checker which is designed for verifying probabilistic properties can be used to verify non probabilistic properties by using PRISM to also verify the OASIS NoC for deadlock freedom. The verification result of both FDR and PRISM shows that the OASIS NoC is free from deadlock. It was also shown using PRISM that the OASIS NoC behaves as a message buffer as expected of NoCs.

Chapter 1

Introduction

“Thus, there is a continual need to strive for balance, conciseness, and even elegance. The approach we take, then, can be summarized in the following: Use theory to provide insight; use common sense and intutition where it is suitable, but fall back upon the formal theory when difficulties and complexities arise.” David Gries (The balance between formality and common sense, 1981) Computers are increasingly becoming ubiquitous and the society’s dependence on computers cannot be overemphasized. Imagine being in a future car which uses x-by-wire (where x is steer, break, gear, etc) technology and you apply the brakes but the car refuses to stop because the chip responsible for the breaking system is not responding. This failure may be due to the fact that the computerized breaking system which is likely to be a System on Chip (SoC), deadlocked and therefore no communication between the chips internal modules were possible. But fortunately, this is never going to hapen not because the current traditional simulation-based verification techiniques are enough to verify these chips but rather more robust formal techniques will be applied to ensure that such a situation is not possible by design. The good news is that, although the communication structure of SoCs tend to have complex state machines, flow control logic and handshaking protocols, the design blocks that make up such networking chips are well-suited for formal verification. Specifying properties that describe proper operation of these chips, while not trivial, is a task that designers and verification engineers can accomplish with little training[Nar04].

Introduction

In short the motivation for this work is: the society is increasingly becoming dependent on computers. Computers are becoming more and more complex and therefore we need to ensure these systems are dependable and increase people’s confidence in using them.

Department: Computer Science (M.Sc Thesis)

Format: MS Word

Chapters: 1 - 5, Preliminary Pages, Abstract, References, Appendix.

No. of Pages: 101

Price: 20,000 NGN

In Stock

Buy Now

Our Customers are Happy!!!

See What Some of Our Customers are Saying About Us