Higher Order Logic and Hardware Verification Book

	List of Figures
	Preface
1	Hardware Verification	1
1.1	The hardware verification method	2
1.2	Limitations of hardware verification	3
1.3	Abstraction	4
1.4	Hardware verification using higher order logic	6
2	Higher Order Logic and the HOL System	9
2.1	Types	9
2.2	Terms	12
2.3	Sequents, theorems and inference rules	16
2.4	Constant definitions	18
2.5	The primitive constant [epsilon]	19
2.6	Recursive definitions	20
2.7	Type definitions	21
2.8	The HOL system	24
3	Hardware Verification using Higher Order Logic	29
3.1	Specifying hardware behaviour	29
3.2	Deriving behaviour from structure	35
3.3	Formulating correctness	38
3.4	An example correctness proof	39
3.5	Other approaches	42
4	Abstraction	47
4.1	Abstraction within a model	48
4.2	Two problems	54
4.3	Abstraction in practice	56
4.4	Validity conditions	58
4.5	A notation for correctness	59
4.6	Abstraction and hierarchical verification	60
4.7	Abstraction between models	66
4.8	Other approaches	68
5	Data Abstraction	69
5.1	Defining concrete types in logic	69
5.2	An example: a transistor model	74
5.3	An example of data abstraction	77
5.4	Reasoning about hardware using bit-vectors	82
5.5	Reasoning about tree-shaped circuits	88
5.6	Other approaches	94
6	Temporal Abstraction	97
6.1	Temporal abstraction by sampling	97
6.2	An example: abstracting to unit delay	103
6.3	A synchronizing temporal abstraction	105
6.4	A case study: the T-ring	106
6.5	Other approaches	125
7	Abstraction between Models	129
7.1	Representing the structure of CMOS circuits	129
7.2	Defining the semantics of CMOS circuits	133
7.3	Defining satisfaction	136
7.4	Correctness in the two models	136
7.5	Relating the models	138
7.6	Improving the results	143
7.7	Other approaches	146
	References	147
	Index	159