Formal verification of floating-point hardware design : a mathematical approach

Description

Foreword Preface to the Second Edition Preface to the First Edition Contents and Structure of the Book Formalization: The Role of ACL2 Obtaining the Associated ACL2 Code Acknowledgments Contents Part I Register-Transfer Logic 1 Basic Arithmetic Functions 1.1 Floor and Ceiling 1.2 Modulus 1.3 Truncation 2 Bit Vectors 2.1 Bit Slices 2.2 Bit Extraction 2.3 Concatenation 2.4 Integer Formats 2.5 Fixed-Point Formats 3 Logical Operations 3.1 Binary Operations 3.2 Complement Part II Floating-Point Arithmetic 4 Floating-Point Numbers 4.1 Decomposition 4.2 Exactness 5 Floating-Point Formats 5.1 Classification of Formats 5.2 Normal Encodings 5.3 Denormals and Zeroes 5.4 Infinities and NaNs 6 Rounding 6.1 Rounding Toward Zero 6.2 Rounding Away from Zero 6.3 Rounding to Nearest 6.4 Odd Rounding 6.5 IEEE Rounding 6.6 Denormal Rounding 6.7 Underflow Detection 7 IEEE-Compliant Square Root 7.1 Truncated Square Root 7.2 Odd-Rounded Square Root 7.3 IEEE-Rounded Square Root Part III Implementation of Elementary Operations 8 Addition 8.1 Bit Vector Addition 8.2 Parallel Prefix Adders 8.3 Leading Zero Anticipation 8.4 Counting Leading Zeroes 9 Multiplication 9.1 Radix-2 Booth Encoding 9.2 Radix-4 Booth Encoding 9.3 Encoding Carry-Save Sums 9.4 Statically Encoded Multiplier Arrays 9.5 Radix-8 Booth Encoding 10 SRT Division and Square Root 10.1 SRT Division 10.2 Minimally Redundant Radix-4 Division 10.3 Minimally Redundant Radix-8 Division 10.4 SRT Square Root 10.5 Minimally Redundant Radix-4 Square Root 10.6 Minimally Redundant Radix-8 Square Root 11 Division Based on Fused Multiply-Add 11.1 Reciprocal Approximation 11.2 Quotient Refinement 11.3 Reciprocal Refinement 11.4 Examples Part IV Comparative Architectures: SSE, x87, and Arm 12 SSE Floating-Point Instructions 12.1 SSE Control and Status Register 12.2 Overview of SSE Floating-Point Exceptions 12.3 Pre-computation Exceptions 12.4 Computation 12.5 Post-computation Exceptions 13 x87 Instructions 13.1 x87 Control Word 13.2 x87 Status Word 13.3 Overview of x87 Exceptions 13.4 Pre-computation Exceptions 13.5 Post-computation Exceptions 14 Arm Floating-Point Instructions 14.1 Floating-Point Status and Control Register 14.2 Pre-computation Exceptions 14.3 Post-computation Exceptions Part V Formal Verification of RTL Designs 15 The RAC Modeling Language 15.1 Language Overview 15.2 Parameter Passing 15.3 Registers 15.4 Arithmetic 15.5 Control Restrictions 15.6 Translation to ACL2 16 Double-Precision Multiplication and Scaling 16.1 Parameters 16.2 Booth Multiplier 16.3 Unrounded Product 16.4 FMA Support 16.5 Rounded Product: FMUL and FSCALE 17 Double-Precision Addition and Fused Multiply-Add 17.1 Preliminary Analysis 17.2 Alignment 17.3 Addition 17.4 Leading Zero Anticipation 17.5 Normalization 17.6 Rounding 17.7 Correctness Theorems 18 Multi-precision Radix-8 SRT Division 18.1 Overview 18.2 Pre-processing 18.3 Iterative Phase 18.4 Post-processing and Rounding 19 64-Bit Integer Division 19.1 Preliminary Analysis and Early Exit 19.2 Detecting Powers of 2 19.3 Instantiating the SRT Algorithm 19.4 Post-processing 20 Multi-precision Radix-4 SRT Square Root 20.1 Pre-processing 20.2 Iterative Phase 20.3 Post-processing and Rounding 21 Multi-precision Radix-2 SRT Division 21.1 Overview 21.2 Pre-processing 21.3 Iterative Phase 21.4 Post-processing 22 Fused Multiply-Add of a Graphics Processor 22.1 Overview 22.2 Multiplication 22.3 Rescaling 22.4 Addition 22.5 Final Result Bibliography Index