Higher Order Logic and Hardware Verification

✍ Scribed by T. F. Melham

• Publisher: Cambridge University Press
• Year: 2009
• Tongue: English
• Leaves: 180
• Series: Cambridge Tracts in Theoretical Computer Science 31
• Category: Library

✦ Synopsis

Dr. Melham shows here how formal logic can be used to specify the behavior of hardware designs and reason about their correctness. A primary theme of the book is the use of abstraction in hardware specification and verification. The author describes how certain fundamental abstraction mechanisms for hardware verification can be formalized in logic and used to express assertions about design correctness and the relative accuracy of models of hardware behavior. His approach is pragmatic and driven by examples. He also includes an introduction to higher-order logic, which is a widely used formalism in this subject, and describes how that formalism is actually used for hardware verification. The book is based in part on the author's own research as well as on graduate teaching. Thus it can be used to accompany courses on hardware verification and as a resource for research workers.

✦ Table of Contents

Cover......Page 1
Frontmatter......Page 2
Contents......Page 6
List of Figures......Page 10
Preface......Page 12
1 - Hardware Verification......Page 16
1.1 The hardware verification method......Page 17
1.2 Limitations of hardware verification......Page 18
1.3 Abstraction......Page 19
1.4 Hardware verification using higher order logic......Page 21
2.1 Types......Page 24
2.2 Terms......Page 27
2.3 Sequents, theorems and inference rules......Page 31
2.4 Constant definitions......Page 33
2.5 The primitive constant [ELEMENT OF]......Page 34
2.6 Recursive definitions......Page 35
2.7 Type definitions......Page 36
2.8 The HOL system......Page 39
3.1 Specifying hardware behaviour......Page 44
3.2 Deriving behaviour from structure......Page 50
3.3 Formulating correctness......Page 53
3.4 An example correctness proof......Page 54
3.5 Other approaches......Page 57
4 - Abstraction......Page 62
4.1 Abstraction within a model......Page 63
4.2 Two problems......Page 69
4.3 Abstraction in practice......Page 71
4.4 Validity conditions......Page 73
4.5 A notation for correctness......Page 74
4.6 Abstraction and hierarchical verification......Page 75
4.7 Abstraction between models......Page 81
4.8 Other approaches......Page 83
5.1 Defining concrete types in logic......Page 84
5.2 An example: a transistor model......Page 89
5.3 An example of data abstraction......Page 92
5.4 Reasoning about hardware using bit-vectors......Page 97
5.5 Reasoning about tree-shaped circuits......Page 103
5.6 Other approaches......Page 109
6.1 Temporal abstraction by sampling......Page 112
6.2 An example: abstracting to unit delay......Page 118
6.3 A synchronizing temporal abstraction......Page 120
6.4 A case study: the T-ring......Page 121
6.5 Other approaches......Page 140
7.1 Representing the structure of CMOS circuits......Page 144
7.2 Defining the semantics of CMOS circuits......Page 148
7.4 Correctness in the two models......Page 151
7.5 Relating the models......Page 153
7.6 Improving the results......Page 158
7.7 Other approaches......Page 161
References......Page 162
Index......Page 174