For more Computer Science projects click here


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.


Table of contents
List of Figures

Chapter 1- Introduction
1.1       OVERVIEW
1.2       RELATED WORK

Chapter 2– Network on Chip
2.1       TOPOLOGY
2.1.1    Regular topologies
2.1.2    Irregular topologies
2.2       ROUTING
2.3       SWITCHING
2.4       FLOW CONTROL
2.5       BUFFERING
2.6       OASIS NOC
2.6.1    Topology
2.6.2    Switching and Routing
2.6.3    Flow control

Chapter 3– Formal Verification
3.2.1    Modelling a system
3.2.2    Specification of system Properties
3.2.3    Temporal Model checking problem
3.2.4    State Space Explosion

Chapter 4– Refinement Model Checking
4.1       CSP
4.1.1    The CSP Language
4.1.2    Observing Process behaviour – Failure, Divergence and Refinement
4.1.3    Operational Semantics
4.2       FDR
4.2.1    Verification with FDR
4.3       ProBe

Chapter 5 – Probabilistic Model Checking
5.1       Introduction
5.1.1    Probabilistic model checking
5.1.2    Overview of PCTL
5.2       PRISM language
5.3       PRISM Properties specification
5.3.1    The P operator
5.3.2    The S operator
5.3.3    Rewards-based properties - R operator
5.3.4    Quantitative properties

Chapter 6 - Model Checking OASIS with FDR
6.1       Modeling OASIS in CSP
6.1.1    Model Parameters and channels
6.1.2    Input Buffer model
6.1.3    Route model
6.1.4    Router model
6.1.5    Network model
6.2       Verification in FDR
6.3       FDR Verification Results and Analysis

Chapter 7– Model Checking OASIS with PRISM
7.1       Prism model of OASIS
7.2       PRISM Verification of OASIS – Results and Analysis
7.2.1    Verification of deadlock-freedom
7.2.2    Buffer property verification

Chapter 8- Conclusion
Appendix A – PRISM Verification Results


Chapter 1


“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].

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.

1.1  Overview

As the number of modules integrated on a single die multiplies and VLSI technology scales toward deep sub-micron level, on-chip inter-module communication becomes a performance bottleneck. The state of art in on-chip module interconnection is a shared bus with a central arbiter. But as the number of modules increase, this common shared bus approach poses serious scalability problems which results in low performance and energy inefficiencies. Network on Chip (NoC) has being proposed as a viable solution to address the problem of on chip communication scalability issues.....

For more Computer Science projects click here
This is a Postgraduate Thesis and the complete research material plus questionnaire and references can be obtained at an affordable price of N3,000 within Nigeria or its equivalent in other currencies.


Kindly pay/transfer a total sum of N3,000 into any of our Bank Accounts listed below:
·         Diamond Bank Account:
A/C Name:      Haastrup Francis
A/C No.:         0096144450

·         GTBank Account:
A/C Name:      Haastrup Francis
A/C No.:         0029938679

After payment, send your desired Project Topic, Depositor’s Name, and your Active E-Mail Address to which the material would be sent for downloading (you can request for a downloading link if you don’t have an active email address) to +2348074521866 or +2348066484965. You can as well give us a direct phone call if you wish to. Projects materials are sent in Microsoft format to your mail within 30 Minutes once payment is confirmed. 

N/B:    By ordering for our material means you have read and accepted our Terms and Conditions

Terms of Use: This is an academic paper. Students should NOT copy our materials word to word, as we DO NOT encourage Plagiarism. Only use as guide in developing your original research work.

Delivery Assurance
We are trustworthy and can never SCAM you. Our success story is based on the love and fear for God plus constant referrals from our clients who have benefited from our site. We deliver project materials to your Email address within 15-30 Minutes depending on how fast your payment is acknowledged by us.

Quality Assurance
All research projects, Research Term Papers and Essays on this site are well researched, supervised and approved by lecturers who are intellectuals in their various fields of study.

No comments:

Post a Comment

Note: Only a member of this blog may post a comment.