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