| Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW MN Velev, RE Bryant Proceedings of the 38th annual design automation conference, 226-231, 2001 | 314 | 2001 |
| Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic RE Bryant, S German, MN Velev ACM Transactions on Computational Logic (TOCL) 2 (1), 93-134, 2001 | 170 | 2001 |
| Exploiting positive equality in a logic of equality with uninterpreted functions RE Bryant, S German, MN Velev Computer Aided Verification: 11th International Conference, CAV’99 Trento …, 1999 | 147 | 1999 |
| Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction MN Velev, RE Bryant Proceedings of the 37th Annual Design Automation Conference, 112-117, 2000 | 145 | 2000 |
| Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions to propositional logic MN Velev, RE Bryant Correct Hardware Design and Verification Methods: 10th IFIP WG10. 5 Advanced …, 1999 | 120 | 1999 |
| Efficient translation of Boolean formulas to CNF in formal verification of microprocessors MN Velev ASP-DAC 2004: Asia and South Pacific Design Automation Conference 2004 (IEEE …, 2004 | 113 | 2004 |
| Boolean satisfiability with transitivity constraints RE Bryant, MN Velev ACM Transactions on Computational Logic (TOCL) 3 (4), 604-627, 2002 | 78 | 2002 |
| Efficient and accurate value prediction using dynamic classification B Rychlik, J Faistl, B Krug, A Kurland, JJ Sung, MN Velev, JP Shen Carneige Mellon University, CMµART-1998-01, 1998 | 70 | 1998 |
| Boolean satisfiability with transitivity constraints RE Bryant, MN Velev International Conference on Computer Aided Verification, 85-98, 2000 | 55 | 2000 |
| Exploiting positive equality and partial non-consistency in the formal verification of pipelined microprocessors MN Velev, RE Bryant Proceedings of the 36th annual ACM/IEEE Design Automation Conference, 397-401, 1999 | 52 | 1999 |
| Exploiting signal unobservability for efficient translation to CNF in formal verification of microprocessors MN Velev Proceedings Design, Automation and Test in Europe Conference and Exhibition …, 2004 | 50 | 2004 |
| Formal verification of VLIW microprocessors with speculative execution MN Velev Computer Aided Verification: 12th International Conference, CAV 2000 …, 2000 | 50 | 2000 |
| Using rewriting rules and positive equality to formally verify wide-issue out-of-order microprocessors with a reorder buffer MN Velev Proceedings 2002 Design, Automation and Test in Europe Conference and …, 2002 | 49 | 2002 |
| Automatic abstraction of memories in the formal verification of superscalar microprocessors MN Velev Tools and Algorithms for the Construction and Analysis of Systems: 7th …, 2001 | 49 | 2001 |
| Bit-level abstraction in the verification of pipelined microprocessors by correspondence checking MN Velev, RE Bryant International Conference on Formal Methods in Computer-Aided Design, 18-35, 1998 | 49 | 1998 |
| Efficient modeling of memory arrays in symbolic simulation M Velev, RE Bryant, A Jain Computer Aided Verification: 9th International Conference, CAV'97 Haifa …, 1997 | 46 | 1997 |
| Collection of high-level microprocessor bugs from formal verification of pipelined and superscalar designs MN Velev International Test Conference, 2003. Proceedings. ITC 2003., 138-138, 2003 | 44 | 2003 |
| Exploiting hierarchy and structure to efficiently solve graph coloring as SAT MN Velev 2007 IEEE/ACM International Conference on Computer-Aided Design, 135-142, 2007 | 39 | 2007 |
| Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-solver when Formally Verifying Out-Of-Order Processors. MN Velev AI&M, 2004 | 35 | 2004 |
| TLSim and EVC: a term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories MN Velev, RE Bryant International Journal of Embedded Systems 1 (1-2), 134-149, 2005 | 34 | 2005 |
