Formal Verification of a Network on Chip

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.

TABLE OF CONTENTS

Abstract …………………. i
Acknowledgements ………….. ii
Table of contents ……….. iii
List of Figures ………. vi

Chapter 1 – Introduction

1.1 OVERVIEW …………………. 2
1.2 RELATED WORK ……….. 3
1.3 REPORT STRUCTURE ……………… 4

Chapter 2 – Network on Chip

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

3.1 INTRODUCTION ……………….. 24
3.2 MODEL CHECKING ….. 26
3.2.1 Modelling a system …………………… 28
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

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

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

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
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 

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

Appendix A – PRISM Verification Results …… 86
References ………….. 89

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.

REFERENCES

Ahmad, A. Erdogan, and S. Khawam, “Architecture of a dynamically reconfigurable NoC for adaptive reconfigurable MPSoC,” in AHS, Jun. 2006,pp. 405–411.

Alur and T. Henzinger. Reactive modules. In Proc. 11^th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 207–218,1996.

A. Abderazek and M. Sowa, “Basic Network-on-Chip Interconnection for Future Gigascale MCSoCs Applications: Communication and Computation Orthogonalization”, proceedings of the TJASSST ’06 symposium on science, society and technology, Sousse, Dec. 4-6, 2006.

E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactionson Computers, 35(8):677–691, 1986.

Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Proc. FST & TCS, 1995.

Bertozzi and L. Benini. Xpipes: a network-on-chip architecture for gigascale systems-on-chip. IEEE Circuits and Systems Magazine, 4(2):18– 31,April 2004.