Word Level Symbolic Model Checking A New Approach for Verifying Arithmetic Circuits

The highly-publicized decision error in the Pentium has emphasized the importance of formal verification of arithmetic operations.