The formal verification of a pipelined double-precision IEEE floating-point multiplier

This publication has 5 references indexed in Scilit:

• A simple theorem prover based on symbolic trajectory evaluation and BDD's
  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1995
• Verification of Arithmetic Functions with Binary Moment Diagrams
  Published by Defense Technical Information Center (DTIC) ,1994
• A proof of the nonrestoring division algorithm and its implementation on an ALU
  Formal Methods in System Design, 1994
• A pipelined 50-MHz CMOS 64-bit floating-point arithmetic processor
  IEEE Journal of Solid-State Circuits, 1989
• Formal methods applied to a floating-point number system
  IEEE Transactions on Software Engineering, 1989