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 ………………………………………………………………………………………………….. i
Acknowledgements ………………………………………………………………………………….. ii
Table of contents ……………………………………………………………………………………. iii
List of Figures …………………………………………………………………………………………. vi
Chapter 1 – Introduction ……………………………………………………………………………. 1
1.1 OVERVIEW ………………………………………………………………………………………………. 2
1.2 RELATED WORK …………………………………………………………………………………………. 3
1.3 REPORT STRUCTURE ……………………………………………………………………………………. 4
Chapter 2 – Network on Chip ……………………………………………………………………… 5
2.1 TOPOLOGY ………………………………………………………………………………………………. 6
2.1.1 Regular topologies …………………………………………………………………………. 8
2.1.2 Irregular topologies ………………………………………………………………………. 10
2.2 ROUTING ………………………………………………………………………………………………. 11
2.3 SWITCHING ……………………………………………………………………………………………. 13
2.4 FLOW CONTROL ………………………………………………………………………………………. 15
2.5 BUFFERING ……………………………………………………………………………………………. 17
2.6 OASIS NOC ………………………………………………………………………………………….. 18
2.6.1 Topology……………………………………………………………………………………… 18
2.6.2 Switching and Routing ………………………………………………………………….. 19
2.6.3 Flow control ………………………………………………………………………………… 22
Chapter 3 – Formal Verification ……………………………………………………………….. 24
3.1 INTRODUCTION ……………………………………………………………………………………….. 24
3.2 MODEL CHECKING ……………………………………………………………………………………. 26
3.2.1 Modelling a system ………………………………………………………………………. 28
iv
3.2.2 Specification of system Properties …………………………………………………. 29
3.2.3 Temporal Model checking problem ………………………………………………… 31
3.2.4 State Space Explosion …………………………………………………………………… 32
Chapter 4 – Refinement Model Checking ………………………………………………….. 35
4.1 CSP ……………………………………………………………………………………………………. 35
4.1.1 The CSP Language ………………………………………………………………………… 36
4.1.2 Observing Process behaviour – Failure, Divergence and Refinement….. 45
4.1.3 Operational Semantics ………………………………………………………………….. 49
4.2 FDR ……………………………………………………………………………………………………. 52
4.2.1 Verification with FDR ……………………………………………………………………. 53
4.3 ProBe …………………………………………………………………………………………………. 56
Chapter 5 – Probabilistic Model Checking ………………………………………………….. 58
5.1 Introduction ……………………………………………………………………………………….. 58
5.1.1 Probabilistic model checking …………………………………………………………. 58
5.1.2 Overview of PCTL …………………………………………………………………………. 59
5.2 PRISM language ………………………………………………………………………………….. 60
5.3 PRISM Properties specification ……………………………………………………………… 63
5.3.1 The P operator …………………………………………………………………………….. 64
5.3.2 The S operator …………………………………………………………………………….. 65
5.3.3 Rewards-based properties – R operator ………………………………………….. 65
5.3.4 Quantitative properties ………………………………………………………………… 66
Chapter 6 – Model Checking OASIS with FDR ……………………………………………….. 68
6.1 Modeling OASIS in CSP …………………………………………………………………………. 68
6.1.1 Model Parameters and channels ……………………………………………………. 69
6.1.2 Input Buffer model ……………………………………………………………………….. 70
6.1.3 Route model ………………………………………………………………………………… 71
6.1.4 Router model ………………………………………………………………………………. 73
v
6.1.5 Network model ……………………………………………………………………………. 73
6.2 Verification in FDR ………………………………………………………………………………. 74
6.3 FDR Verification Results and Analysis …………………………………………………….. 74
Chapter 7 – Model Checking OASIS with PRISM …………………………………………… 76
7.1 Prism model of OASIS ………………………………………………………………………….. 76
7.2 PRISM Verification of OASIS – Results and Analysis …………………………………. 79
7.2.1 Verification of deadlock-freedom …………………………………………………… 79
7.2.2 Buffer property verification …………………………………………………………… 81
Chapter 8 – Conclusion …………………………………………………………………………….. 84
Appendix A – PRISM Verification Results …………………………………………………… 86
References ……………………………………………………………………………………………
CHAPTER ONE
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 2
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. NoC has gained a lot of attention in the SoC community and even among traditional data network communities. Already a lot of papers have been written on their design and implementations; some of which have been synthesized on FPGAs and on ASICs. Examples of such NoCs include the Æthereal, Nostrum, Spidergon, Octagon, XPipes and FAUST.
The NoC paradigm brings along it new research challenges. Due to their nature, NoC is restricted by low latency, area, power and heat dissipation. To reduce communication latency, various switching and routing techniques are employed some of which makes the NoC prone to deadlocks. Again, restriction on area puts a limit on router buffer capacity which overloads the network and thereby increases the possibility of deadlock. Livelocks can also cause serious consequences with respect to power consumption and heat dissipation. While conventional data networks, like the internet, can accept packet losses and resending of packets, this is unacceptable in a NoC environment. Because of these reasons it becomes extremely
Introduction 3
necessary to verify their design. The size and complexity of SoCs is growing at a faster rate that traditional based techniques of simulation and testing are being stretched passed their limits. The only viable alternative is the use of formal verification methods whereby properties are proved to be true in a system by using mathematical techniques. The goal of this project therefore is to push forward the range of applicability of formal methods by formally verifying a NoC using model checking techniques. The OASIS NoC which is a realization in FPGA of an earlier proposed Basic Network on Chip (BANC) by Abderazak and Sowa [AS06], will be used as a case study. Properties to be verified will be deadlock-freedom and whether the network behaves as a buffer without any flit losses. The FDR model checker will be used to verify the NoC for deadlock freedom. We also show how the PRISM model checker which is designed for verifying probabilistic properties can be used to very non-probabilistic properties by verifying OASIS NoC for deadlock freedom and also buffer property.
1.2 Related work
NoC is a more recent design paradigm and therefore little work has been done on their formal verification. One of the most notable works in this area is the work by Gebremichael et al.[GVZ+05] who verified the Philips Æthereal Protocol[GDR05] in PVS logic. Schmaltz and Borrione also proposed a Generic Network on Chip framework (GeNoC)[SD05]. GeNoC is a metamodel of NoC which was developed and implemented in the ACL2 theorem prover. In a latter work Schmaltz et al. used their earlier work, GeNoC, to verify the Spidergon NoC from STMicroelectronics [SB07]. Also in [BHPS07], the Hermes [DHPS07] NoC was formalised in the GeNoC framework and was formally verified.
Introduction 4
In [SSTV07], the CADP toolbox [GLM01] was used to perform a formal verification of an Asynchronous Network on Chip (ANoC) specified in the Communication Hardware Process(CHP).
1.3 Report structure
The rest of this report is organized as follows. The first part of Chapter 2 introduces the concept of Network on Chip describing properties of NoCs such as the topology, switching, routing and flow control techniques. The second part of Chapter 2 presents the OASIS NoC which is used as a case study for this work. In Chapter 3 we give an introduction to formal verification techniques with emphasis on the type of technique used in this work, namely model checking. In this chapter we provide a way of modelling a system and how to specify its properties. The chapter ends with a discussion on one of the main shortcomings of the model checking technique, the state space explosion. Chapter 4 presents a background on how to model a system and its properties using the CSP approach and then present the FDR tool which can be used to verify a system specified in CSP. Chapter 5 presents a different approach to model checking, called probabilistic model checking and presents the PRISM language and tool. The OASIS NoC is formalized in CSP and PRISM language and then verified for deadlock freedom using FDR and PRISM tool in Chapter 6 and Chapter 7 respectively.
Finally, Chapter 8 concludes this report, with a summary of this work and provides a discussion of possible future directions for this work.
IF YOU CAN'T FIND YOUR TOPIC, CLICK HERE TO HIRE A WRITER»
