Verification of all circuits in a floating-point unit using word-level model checking

This publication has 16 references indexed in Scilit:

• Dynamic variable ordering for ordered binary decision diagrams
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
• Efficient construction of binary moment diagrams for verifying arithmetic circuits
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
• RuleBase
  Published by Association for Computing Machinery (ACM) ,1996
• Non-restoring integer square root: A case study in design by principled optimization
  Published by Springer Nature ,1995
• A proof of the nonrestoring division algorithm and its implementation on an ALU
  Formal Methods in System Design, 1994
• Symbolic Model Checking
  Published by Springer Nature ,1993
• Spectral transforms for large boolean functions with applications to technology mapping
  Published by Association for Computing Machinery (ACM) ,1993
• Verification of a multiplier: 64 bits and beyond
  Published by Springer Nature ,1993
• On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
  IEEE Transactions on Computers, 1991
• Developing the WTL3170/3171 Sparc floating-point coprocessors
  IEEE Micro, 1990