Formal Verification of Floating-Point Hardware Design (eBook)

David M. Russinoff is Principal Engineer at Arm Holdings. He holds a bachelor's degree from the Massachusetts Institute of Technology and a doctorate from New York University, both in mathematics, and a master's in computer sciences from the University of Texas at Austin.  He has spent twenty-five years developing mathematical methods of hardware verification, with an emphasis on interactive theorem proving, and applying them in the analysis of commercial designs, especially arithmetic circuits.  

Foreword 6
Preface 11
Contents and Structure of the Book 13
Formalization: The Role of ACL2 15
Obtaining the Associated ACL2 Code 16
Acknowledgments 17
Contents 18
Part I Register-Transfer Logic 22
1 Basic Arithmetic Functions 23
1.1 Floor and Ceiling 23
1.2 Modulus 26
1.3 Truncation 32
2 Bit Vectors 36
2.1 Bit Slices 37
2.2 Bit Extraction 43
2.3 Concatenation 47
2.4 Integer Formats 51
2.5 Fixed-Point Formats 54
3 Logical Operations 57
3.1 Binary Operations 57
3.2 Complement 64
3.3 Algebraic Properties 67
Part II Floating-Point Arithmetic 69
4 Floating-Point Numbers 71
4.1 Decomposition 71
4.2 Exactness 74
5 Floating-Point Formats 80
5.1 Classification of Formats 80
5.2 Normal Encodings 82
5.3 Denormals and Zeroes 86
5.4 Infinities and NaNs 91
6 Rounding 93
6.1 Rounding Toward Zero 95
6.2 Rounding Away from Zero 102
6.3 Rounding to Nearest 109
6.4 Odd Rounding 125
6.5 IEEE Rounding 133
6.6 Denormal Rounding 143
7 IEEE-Compliant Square Root 151
7.1 Truncated Square Root 152
7.2 Odd-Rounded Square Root 154
7.3 IEEE-Rounded Square Root 157
Part III Implementation of Elementary Operations 161
8 Addition 162
8.1 Bit Vector Addition 162
8.2 Leading Zero Anticipation 170
8.3 Trailing Zero Anticipation 175
9 Multiplication 179
9.1 Radix-2 Booth Encoding 180
9.2 Radix-4 Booth Encoding 181
9.3 Encoding Carry-Save Sums 187
9.4 Statically Encoded Multiplier Arrays 190
9.5 Radix-8 Booth Encoding 193
10 SRT Division and Square Root 197
10.1 SRT Division 197
10.2 Minimally Redundant Radix-4 Division 202
10.3 Minimally Redundant Radix-8 Division 204
10.4 SRT Square Root 205
10.5 Minimally Redundant Radix-4 Square Root 212
11 FMA-Based Division 217
11.1 Reciprocal Approximation 219
11.2 Quotient Refinement 221
11.3 Reciprocal Refinement 227
11.4 Examples 228
Part IV Comparative Architectures: SSE, x87, and Arm 232
12 SSE Floating-Point Instructions 234
12.1 SSE Control and Status Register 234
12.2 Overview of SSE Floating-Point Exceptions 235
12.3 Pre-computation Exceptions 236
12.4 Computation 237
12.5 Post-Computation Exceptions 238
13 x87 Instructions 240
13.1 x87 Control Word 240
13.2 x87 Status Word 241
13.3 Overview of x87 Exceptions 242
13.4 Pre-computation Exceptions 243
13.5 Post-Computation Exceptions 244
14 Arm Floating-Point Instructions 245
14.1 Floating-Point Status and Control Register 246
14.2 Pre-computation Exceptions 247
14.3 Post-Computation Exceptions 248
Part V Formal Verification of RTL Designs 249
15 The Modeling Language 251
15.1 Language Overview 252
Program Structure 252
Data Types 253
Statements 253
Functions 253
15.2 Parameter Passing 254
15.3 Registers 255
15.4 Arithmetic 257
15.5 Control Restrictions 258
15.6 Translation to ACL2 260
16 Double-Precision Multiplication 264
16.1 Parameters 265
16.2 Booth Multiplier 267
16.3 Unrounded Product 268
16.4 FMA Support 278
16.5 Rounded Product and FMUL 280
17 Double-Precision Addition and FMA 289
17.1 Parameters and Input Assumptions 289
17.2 Alignment 295
17.3 Addition 297
17.4 Leading Zero Anticipation 302
17.5 Normalization 304
17.6 Rounding 306
17.7 Correctness Theorems 312
18 Multi-Precision Radix-4 SRT Division 318
18.1 Overview 318
18.2 Pre-processing 320
18.3 Iterative Phase 323
18.4 Post-Processing and Rounding 329
19 Multi-Precision Radix-4 SRT Square Root 339
19.1 Pre-processing 339
19.2 Iterative Phase 341
19.3 Post-Processing and Rounding 345
Appendices 352
A Common Code 352
B Double-Precision Multiplication 354
C Double-Precision Addition with FMA 361
D Multi-Precision Radix-4 Division 369
E Multi-Precision Radix-4 Square Root 379
Bibliography 385
Index 387