| 2009 |
|---|
| 41 | EE | Miroslav N. Velev,
Ping Gao:
Efficient SAT-based techniques for Design of Experiments by using static variable ordering.
ISQED 2009: 371-376 |
| 2008 |
|---|
| 40 | EE | Miroslav N. Velev,
Ping Gao:
Comparison of Boolean Satisfiability Encodings on FPGA Detailed Routing Problems.
DATE 2008: 1268-1273 |
| 2007 |
|---|
| 39 | EE | Miroslav N. Velev:
Exploiting hierarchy and structure to efficiently solve graph coloring as SAT.
ICCAD 2007: 135-142 |
| 2006 |
|---|
| 38 | EE | Miroslav N. Velev:
Formal Verification of Pipelined Microprocessors with Delayed Branches.
ISQED 2006: 296-299 |
| 37 | EE | Miroslav N. Velev:
Using Abstraction for Efficient Formal Verification of Pipelined Processors with Value Prediction.
ISQED 2006: 51-56 |
| 2005 |
|---|
| 36 | EE | Miroslav N. Velev:
Comparison of schemes for encoding unobservability in translation to SAT.
ASP-DAC 2005: 1056-1059 |
| 35 | EE | Miroslav N. Velev:
Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units.
CHARME 2005: 97-113 |
| 34 | EE | Miroslav N. Velev,
Randal E. Bryant:
TLSim and EVC: a term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories.
IJES 1(1/2): 134-149 (2005) |
| 2004 |
|---|
| 33 | EE | Miroslav N. Velev:
Efficient formal verification of pipelined processors with instruction queues.
ACM Great Lakes Symposium on VLSI 2004: 92-95 |
| 32 | EE | Miroslav N. Velev:
Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-solver when Formally Verifying Out-Of-Order Processors.
AMAI 2004 |
| 31 | EE | Miroslav N. Velev:
Efficient translation of boolean formulas to CNF in formal verification of microprocessors.
ASP-DAC 2004: 310-315 |
| 30 | EE | Miroslav N. Velev:
Using positive equality to prove liveness for pipelined microprocessors.
ASP-DAC 2004: 316-321 |
| 29 | EE | Miroslav N. Velev:
Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors.
DATE 2004: 266-271 |
| 28 | EE | Miroslav N. Velev:
Comparative Study of Strategies for Formal Verification of High-Level Processors.
ICCD 2004: 119-124 |
| 27 | | Miroslav N. Velev:
A new generation of ISCAS benchmarks from formal verification of high-level microprocessors.
ISCAS (5) 2004: 213-216 |
| 26 | EE | Miroslav N. Velev:
Encoding Global Unobservability for Efficient Translation to SAT.
SAT 2004 |
| 25 | EE | Miroslav N. Velev:
Tuning SAT for Formal Verification and Testing.
J. UCS 10(12): 1559-1561 (2004) |
| 2003 |
|---|
| 24 | EE | Miroslav N. Velev:
Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs.
ITC 2003: 138-147 |
| 23 | EE | Sudarshan K. Srinivasan,
Miroslav N. Velev:
Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions.
MEMOCODE 2003: 65-74 |
| 22 | EE | Miroslav N. Velev:
Automatic Abstraction of Equations in a Logic of Equality.
TABLEAUX 2003: 196-213 |
| 21 | EE | Miroslav N. Velev,
Randal E. Bryant:
Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
J. Symb. Comput. 35(2): 73-106 (2003) |
| 2002 |
|---|
| 20 | EE | Miroslav N. Velev:
Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer.
DATE 2002: 28-35 |
| 19 | EE | Randal E. Bryant,
Miroslav N. Velev:
Boolean satisfiability with transitivity constraints.
ACM Trans. Comput. Log. 3(4): 604-627 (2002) |
| 2001 |
|---|
| 18 | EE | Miroslav N. Velev,
Randal E. Bryant:
EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations.
CAV 2001: 235-240 |
| 17 | EE | Miroslav N. Velev,
Randal E. Bryant:
Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors.
DAC 2001: 226-231 |
| 16 | EE | Miroslav N. Velev:
Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors.
TACAS 2001: 252-267 |
| 15 | EE | Randal E. Bryant,
Steven M. German,
Miroslav N. Velev:
Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic.
ACM Trans. Comput. Log. 2(1): 93-134 (2001) |
| 2000 |
|---|
| 14 | | Miroslav N. Velev:
Formal Verification of VLIW Microprocessors with Speculative Execution.
CAV 2000: 296-311 |
| 13 | | Randal E. Bryant,
Miroslav N. Velev:
Boolean Satisfiability with Transitivity Constraints.
CAV 2000: 85-98 |
| 12 | EE | Miroslav N. Velev,
Randal E. Bryant:
Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction.
DAC 2000: 112-117 |
| 11 | EE | Randal E. Bryant,
Miroslav N. Velev:
Boolean Satisfiability with Transitivity Constraints
CoRR cs.LO/0008001: (2000) |
| 1999 |
|---|
| 10 | EE | Randal E. Bryant,
Steven M. German,
Miroslav N. Velev:
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions.
CAV 1999: 470-482 |
| 9 | EE | Miroslav N. Velev,
Randal E. Bryant:
Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic.
CHARME 1999: 37-53 |
| 8 | EE | Miroslav N. Velev,
Randal E. Bryant:
Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors.
DAC 1999: 397-401 |
| 7 | | Randal E. Bryant,
Steven M. German,
Miroslav N. Velev:
Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions.
TABLEAUX 1999: 1-13 |
| 6 | EE | Randal E. Bryant,
Steven M. German,
Miroslav N. Velev:
Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic
CoRR cs.LO/9910014: (1999) |
| 1998 |
|---|
| 5 | EE | Miroslav N. Velev,
Randal E. Bryant:
Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation.
ACSD 1998: 200-212 |
| 4 | EE | Miroslav N. Velev,
Randal E. Bryant:
Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking.
FMCAD 1998: 18-35 |
| 3 | EE | Miroslav N. Velev,
Randal E. Bryant:
Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation.
TACAS 1998: 136-150 |
| 1997 |
|---|
| 2 | | Randal E. Bryant,
Miroslav N. Velev:
Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation.
ASIAN 1997: 18-31 |
| 1 | | Miroslav N. Velev,
Randal E. Bryant,
Alok Jain:
Efficient Modeling of Memory Arrays in Symbolic Simulation.
CAV 1997: 388-399 |
