Scalable Hardware Verification with Symbolic Simulation

Contents......Page 6
Dedication......Page 5
List of Figures......Page 10
List of Tables......Page 12
Preface......Page 13
Acknowledgments......Page 16
1. INTRODUCTION......Page 18
1.1 Functional validation......Page 19
1.2.1 Symbolic simulation......Page 20
1.3 Organization of the book......Page 22
2.1 The design flow......Page 24
2.2 RTL verification......Page 28
2.3 Boolean functions and their representation......Page 31
2.3.1 NP-equivalence......Page 33
2.4 Binary decision diagrams......Page 34
2.5 Models for design verification......Page 36
2.5.1 Structural network model......Page 37
2.5.2 State diagrams......Page 39
2.5.3 Mathematical model of finite state machines......Page 40
2.6 Functional validation......Page 41
2.7 Formal verification......Page 45
2.7.1 Symbolic finite state machine traversal......Page 46
References......Page 48
3.1 The origins of symbolic simulation......Page 51
3.2 Symbolic simulation of a logic gate......Page 52
3.3 Symbolic simulation, time frame-by-time frame......Page 53
3.3.1 Symbolic simulation to expose design flaws......Page 56
3.4.1 Symbolic reachability analysis......Page 58
3.4.2 Symbolic trajectory evaluation......Page 60
3.5 Enhancements and optimizations......Page 61
3.6 The challenge in symbolic simulation......Page 63
References......Page 64
4.1 Parametric transformations......Page 67
4.1.1 A formal definition......Page 68
4.1.2 Applications to symbolic simulation......Page 69
4.1.3 A brief history of parametric solutions......Page 72
4.2 Disjoint-support decompositions......Page 73
4.2.2 Decomposition trees......Page 75
4.3.1 Building decompositions bottom-up......Page 78
4.3.2 Putting it all together: The DEC procedure......Page 80
4.3.3 Complexity analysis and considerations......Page 83
4.3.4 Decomposability experiments......Page 84
4.4 On the decomposability of Boolean functions......Page 91
4.5 Evolution of disjoint-support decompositions......Page 92
4.6 Summary......Page 93
References......Page 94
5. APPROXIMATE SIMULATION......Page 97
5.2 The CBSS algorithm......Page 98
5.3 The reparametrization phase......Page 99
5.3.1 Using functional dependencies......Page 101
5.3.2 How to classify the components of the state vector......Page 103
5.3.3 The remap function......Page 107
5.4 Implementation and insights......Page 109
5.4.1 Experimental results......Page 110
5.5 Quasi-Symbolic Simulation......Page 115
5.5.1 Simulation with X values......Page 116
5.5.2 Approximating and reclassifying symbolic variables......Page 117
5.5.3 Care and Don\'t care sets......Page 118
5.6 Summary......Page 119
References......Page 120
6.1 Re-encoding the state function using DSDs......Page 121
6.1.1 Reduction at free points......Page 124
6.1.2 Elimination of prime functions......Page 127
6.1.3 Removal of non-dominant variables......Page 130
6.2.1 Experimental results......Page 133
6.3 Parametrization in the micro-processor domain......Page 138
6.3.1 Structural decompositions......Page 139
6.3.2 Parametrization for data-space partitions......Page 140
References......Page 141
7. CONCLUSION......Page 143
7.2 Scalable symbolic simulation techniques......Page 144
References......Page 145
A.l Function decompositions......Page 146
A.2 The unique maximal Disjoint-Support Decomposition......Page 147
A.3 The canonical decomposition tree......Page 156
A.4 Building the decomposition tree from a BDD......Page 160
A.5 The DEC procedure......Page 174
References......Page 181
References......Page 183
D......Page 190
R......Page 191
V......Page 192