| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Miroslav N. Velev, Ping Gao 0002 |
Automated debugging of counterexamples in formal verification of pipelined microprocessors.  |
ASP-DAC  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Ping Gao 0002 |
Exploiting Abstraction for Efficient Formal Verification of DSPs with Arrays of Reconfigurable Functional Units. |
ICFEM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Ping Gao 0002 |
Efficient Pseudo-Boolean Satisfiability Encodings for Routing and Wavelength Assignment in Optical Networks. |
SARA |
2011 |
DBLP BibTeX RDF |
|
| 1 | Miroslav N. Velev, Ping Gao 0002 |
Modular Schemes for Constructing Equivalent Boolean Encodings of Cardinality Constraints and Application to Error Diagnosis in Formal Verification of Pipelined Microprocessors. |
SARA |
2011 |
DBLP BibTeX RDF |
|
| 1 | Miroslav N. Velev, Ping Gao 0002 |
Automatic formal verification of reconfigurable DSPs. |
ASP-DAC |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Ping Gao 0002 |
CNF encodings of cardinality in formal methods for robustness checking of gate-level circuits. |
ISCAS |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Ping Gao 0002 |
Automatic formal verification of multithreaded pipelined microprocessors. |
ICCAD |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Ping Gao 0002 |
Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors. |
ICFEM |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Ping Gao 0002 |
A method for debugging of pipelined processors in formal verification by correspondence checking. |
ASP-DAC |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Ping Gao 0002 |
Design of parallel portfolios for SAT-based solving of Hamiltonian cycle problems. |
ISAIM |
2010 |
DBLP BibTeX RDF |
|
| 1 | Miroslav N. Velev, Ping Gao 0002 |
Efficient SAT-based techniques for Design of Experiments by using static variable ordering. |
ISQED |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Ping Gao 0002 |
Exploiting hierarchical encodings of equality to design independent strategies in parallel SMT decision procedures for a logic of equality. |
HLDVT |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Ping Gao 0002 |
Efficient SAT Techniques for Relative Encoding of Permutations with Constraints. |
Australasian Conference on Artificial Intelligence |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Ping Gao 0002 |
Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles. |
SARA |
2009 |
DBLP BibTeX RDF |
|
| 1 | Miroslav N. Velev, Ping Gao 0002 |
Comparison of Boolean Satisfiability Encodings on FPGA Detailed Routing Problems. |
DATE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Exploiting hierarchy and structure to efficiently solve graph coloring as SAT. |
ICCAD |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Using Abstraction for Efficient Formal Verification of Pipelined Processors with Value Prediction. |
ISQED |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Formal Verification of Pipelined Microprocessors with Delayed Branches. |
ISQED |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Comparison of schemes for encoding unobservability in translation to SAT. |
ASP-DAC |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Tuning SAT for Formal Verification and Testing. |
J. UCS |
2004 |
DBLP BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Efficient formal verification of pipelined processors with instruction queues. |
ACM Great Lakes Symposium on VLSI |
2004 |
DBLP DOI BibTeX RDF |
logic of equality, positive equality, decomposition, SAT |
| 1 | Miroslav N. Velev |
Encoding Global Unobservability for Efficient Translation to SAT. |
SAT |
2004 |
DBLP BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Using positive equality to prove liveness for pipelined microprocessors. |
ASP-DAC |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Efficient translation of boolean formulas to CNF in formal verification of microprocessors. |
ASP-DAC |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-solver when Formally Verifying Out-Of-Order Processors. |
ISAIM |
2004 |
DBLP BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors. |
DATE |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev |
A new generation of ISCAS benchmarks from formal verification of high-level microprocessors. |
ISCAS |
2004 |
DBLP BibTeX RDF |
|
| 1 | 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 |
DBLP BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Comparative Study of Strategies for Formal Verification of High-Level Processors. |
ICCD |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Randal E. Bryant |
Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. |
J. Symb. Comput. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs. |
ITC |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Automatic Abstraction of Equations in a Logic of Equality. |
TABLEAUX |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Miroslav N. Velev |
Boolean satisfiability with transitivity constraints. |
ACM Trans. Comput. Log. |
2002 |
DBLP DOI BibTeX RDF |
formal verification, decision procedures, Boolean satisfiability |
| 1 | Miroslav N. Velev |
Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer. |
DATE |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | 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. |
2001 |
DBLP DOI BibTeX RDF |
processor verfication, decision procedures, uninterpreted functions |
| 1 | Miroslav N. Velev |
Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors. |
TACAS |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Randal E. Bryant |
Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors. |
DAC |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Miroslav N. Velev |
Boolean Satisfiability with Transitivity Constraints |
CoRR |
2000 |
DBLP BibTeX RDF |
|
| 1 | Miroslav N. Velev, Randal E. Bryant |
Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. |
DAC |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Miroslav N. Velev |
Boolean Satisfiability with Transitivity Constraints. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev |
Formal Verification of VLIW Microprocessors with Speculative Execution. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Steven M. German, Miroslav N. Velev |
Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic |
CoRR |
1999 |
DBLP BibTeX RDF |
|
| 1 | Miroslav N. Velev, Randal E. Bryant |
Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors. |
DAC |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Steven M. German, Miroslav N. Velev |
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Randal E. Bryant |
Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. |
TACAS |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Randal E. Bryant |
Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation. |
ACSD |
1998 |
DBLP DOI BibTeX RDF |
pipelined microprocessor verification, memory shadowing, Efficient Memory Model (EMM), circuit correspondence checking, symbolic simulation |
| 1 | Miroslav N. Velev, Randal E. Bryant |
Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking. |
FMCAD |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Miroslav N. Velev |
Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation. |
ASIAN |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Randal E. Bryant, Alok Jain |
Efficient Modeling of Memory Arrays in Symbolic Simulation. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")