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.
TABLE OF CONTENTS
Abstract
Table of contents
List of Figures
Chapter 1- Introduction
1.1 OVERVIEW
1.2 RELATED WORK
1.3 REPORT STRUCTURE
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.1 INTRODUCTION
3.2 MODEL CHECKING
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
References
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].
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.....
================================================================
Item Type: Project Material | Size: 98 pages | Chapters: 1-5
Format: MS Word | Delivery: Within 30Mins.
================================================================
No comments:
Post a Comment
Note: Only a member of this blog may post a comment.