Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking

This publication has 16 references indexed in Scilit:

• Verifying pipelined hardware using symbolic logic simulation
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,2003
• Optimizing designs containing black boxes
  Published by Association for Computing Machinery (ACM) ,1997
• Verification of pipelined microprocessors by comparing memory execution sequences in symbolic simulation
  Published by Springer Nature ,1997
• Techniques for verifying superscalar microprocessors
  Published by Association for Computing Machinery (ACM) ,1996
• Formal verification by symbolic evaluation of partially-ordered trajectories
  Formal Methods in System Design, 1995
• Automatic verification of pipelined microprocessor control
  Published by Springer Nature ,1994
• Symbolic Boolean manipulation with ordered binary-decision diagrams
  ACM Computing Surveys, 1992
• Simplification by Cooperating Decision Procedures
  ACM Transactions on Programming Languages and Systems, 1979
• A Practical Decision Procedure for Arithmetic with Function Symbols
  Journal of the ACM, 1979
• Proof of correctness of data representations
  Acta Informatica, 1972