| 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 | 316 | 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 | 167 | 2001 |
| Exploiting positive equality in a logic of equality with uninterpreted functions RE Bryant, S German, MN Velev International Conference on Computer Aided Verification, 470-482, 1999 | 152 | 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 | 149 | 2000 |
| Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions to propositional logic MN Velev, RE Bryant Advanced Research Working Conference on Correct Hardware Design and …, 1999 | 123 | 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 | 117 | 2004 |
| Boolean satisfiability with transitivity constraints RE Bryant, MN Velev ACM Transactions on Computational Logic (TOCL) 3 (4), 604-627, 2002 | 80 | 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 | 67 | 1998 |
| 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 | 53 | 1999 |
| 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 | 53 | 1998 |
| 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 | 51 | 2004 |
| Boolean satisfiability with transitivity constraints RE Bryant, MN Velev International Conference on Computer Aided Verification, 85-98, 2000 | 51 | 2000 |
| Formal verification of VLIW microprocessors with speculative execution MN Velev International Conference on Computer Aided Verification, 296-311, 2000 | 51 | 2000 |
| Efficient modeling of memory arrays in symbolic simulation M Velev, RE Bryant, A Jain International Conference on Computer Aided Verification, 388-399, 1997 | 50 | 1997 |
| Automatic abstraction of memories in the formal verification of superscalar microprocessors MN Velev International Conference on Tools and Algorithms for the Construction and …, 2001 | 49 | 2001 |
| 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 | 48 | 2002 |
| 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 | 43 | 2007 |
| 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 | 43 | 2003 |
| 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 |
| 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 | 34 | 2004 |
