Personal information

United States

Activities

Works (50 of 65)

Items per page:
Page 1 of 2

Automatic Formal Verification of RISC-V Pipelined Microprocessors with Fault Tolerance by Spatial Redundancy at a High Level of Abstraction

2024 | Book chapter
Contributors: Miroslav N. Velev
Source: check_circle
Crossref

Welcome Message

2016 IEEE International High Level Design Validation and Test Workshop, HLDVT 2016
2016 | Conference paper
EID:

2-s2.0-85006401757

Contributors: Varma, P.; Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Exploiting abstraction, learning from random simulation, and SVM classification for efficient dynamic prediction of software health problems

Proceedings - International Symposium on Quality Electronic Design, ISQED
2015 | Conference paper
EID:

2-s2.0-84944324064

Part of ISSN: 19483295 19483287
Contributors: Velev, M.N.; Zhang, C.; Gao, P.; Groce, A.D.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Improving the efficiency of automated debugging of pipelined microprocessors by symmetry breaking in modular schemes for Boolean encoding of cardinality

IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
2015 | Conference paper
EID:

2-s2.0-84936863937

Part of ISSN: 10923152
Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Application of constraints to formal verification and artificial intelligence

Annals of Mathematics and Artificial Intelligence
2014 | Journal article
EID:

2-s2.0-84901200033

Part of ISSN: 10122443
Contributors: Velev, M.N.; Franco, J.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Efficient parallel GPU algorithms for BDD manipulation

Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
2014 | Conference paper
EID:

2-s2.0-84897865475

Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Formal verification of safety of polymorphic heterogeneous multi-core architectures

Proceedings - International Symposium on Quality Electronic Design, ISQED
2014 | Conference paper
EID:

2-s2.0-84899487930

Part of ISSN: 19483295 19483287
Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Application of hierarchical hybrid encodings to efficient translation of csps to sat

Proceedings - International Conference on Tools with Artificial Intelligence, ICTAI
2013 | Conference paper
EID:

2-s2.0-84897731172

Part of ISSN: 10823409
Contributors: Nguyen, V.-H.; Velev, M.N.; Barahona, P.-T.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Automated debugging of counterexamples in formal verification of pipelined microprocessors

Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
2012 | Conference paper
EID:

2-s2.0-84859976623

Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Automatic formal verification of multithreaded pipelined microprocessors

IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
2011 | Conference paper
EID:

2-s2.0-84855819085

Part of ISSN: 10923152
Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Automatic formal verification of reconfigurable DSPs

Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
2011 | Conference paper
EID:

2-s2.0-79952948353

Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

CNF encodings of cardinality in formal methods for robustness checking of gate-level circuits

Proceedings - IEEE International Symposium on Circuits and Systems
2011 | Conference paper
EID:

2-s2.0-79960871881

Part of ISSN: 02714310
Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Efficient Pseudo-Boolean Satisfiability encodings for routing and wavelength assignment in optical networks

SARA 2011 - Proceedings of the 9th Symposium on Abstraction, Reformulation, and Approximation
2011 | Conference paper
EID:

2-s2.0-84890769816

Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Exploiting abstraction for efficient formal verification of DSPs with arrays of reconfigurable functional units

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2011 | Book
EID:

2-s2.0-80455140643

Part of ISSN: 03029743 16113349
Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Modular schemes for constructing equivalent Boolean encodings of cardinality constraints and application to error diagnosis in formal verification of pipelined microprocessors

SARA 2011 - Proceedings of the 9th Symposium on Abstraction, Reformulation, and Approximation
2011 | Conference paper
EID:

2-s2.0-84890720770

Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

A method for debugging of pipelined processors in formal verification by correspondence checking

Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
2010 | Conference paper
EID:

2-s2.0-77951213261

Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

DATICS-2010: Welcome message from workshop organizers: FutureTech 2010

2010 5th International Conference on Future Information Technology, FutureTech 2010 - Proceedings
2010 | Conference paper
EID:

2-s2.0-77954412602

Contributors: Man, K.L.; Mercaldi, M.; Hahanov, V.; Prinetto, P.; Poncino, M.; MacIi, A.; Choi, J.; Li, W.; Schellekens, M.; Popovici, E. et al.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Design of parallel portfolios for SAT-based solving of Hamiltonian Cycle Problems

11th International Symposium on Artificial Intelligence and Mathematics, ISAIM 2010
2010 | Conference paper
EID:

2-s2.0-84874162138

Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Method for formal verification of soft-error tolerance mechanisms in pipelined microprocessors

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2010 | Book
EID:

2-s2.0-78649627510

Part of ISSN: 03029743 16113349
Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Preface of the 2010 IAENG International Conference on Electrical Engineering special session: Design, analysis and tools for integrated circuits and systems

Proceedings of the International MultiConference of Engineers and Computer Scientists 2010, IMECS 2010
2010 | Conference paper
EID:

2-s2.0-79952376775

Contributors: Man, K.L.; Mercaldi, M.; Hahanov, V.; Prinetto, P.; Poncino, M.; MacIi, A.; Choi, J.; Li, W.; Schellekens, M.; Popovici, E. et al.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Proceedings - 4th International Conference on Emerging Security Information, Systems and Technologies, SECURWARE 2010: Preface

Proceedings - 4th International Conference on Emerging Security Information, Systems and Technologies, SECURWARE 2010
2010 | Conference paper
EID:

2-s2.0-79952063370

Contributors: Buchegger, S.; Chen, E.; Dini, P.; Falk, R.; Flegel, U.; Inácio, P.; Jakubowski, M.; Jiang, D.; Roning, J.; Savola, R. et al.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Efficient SAT techniques for absolute encoding of permutation problems: Application to hamiltonian cycles

SARA 2009 - Proceedings, 8th Symposium on Abstraction, Reformulation and Approximation
2009 | Conference paper
EID:

2-s2.0-84890264418

Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Efficient SAT techniques for relative encoding of permutations with constraints

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2009 | Book
EID:

2-s2.0-78650475960

Part of ISSN: 03029743 16113349
Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Efficient SAT-based techniques for design of experiments by using static variable ordering

Proceedings of the 10th International Symposium on Quality Electronic Design, ISQED 2009
2009 | Conference paper
EID:

2-s2.0-67649660567

Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Exploiting hierarchical encodings of equality to design independent strategies in parallel SMT decision procedures for a logic of equality

Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT
2009 | Conference paper
EID:

2-s2.0-76649097979

Part of ISSN: 15526674
Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Comparison of boolean satisfiability encodings on FPGA detailed routing problems

Proceedings -Design, Automation and Test in Europe, DATE
2008 | Conference paper
EID:

2-s2.0-49749121795

Part of ISSN: 15301591
Contributors: Velev, M.N.; Gao, P.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Special track on embedded systems: Applications, solutions, and techniques

Proceedings of the ACM Symposium on Applied Computing
2008 | Conference paper
EID:

2-s2.0-56749177582

Contributors: Bechini, A.; Prete, C.A.; Altenbernd, P.; Bartolini, S.; Bertin, V.; Buttazzo, G.; Cardoso, J.M.P.; Dean, A.; Engels, M.; Foglia, P. et al.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Exploiting hierarchy and structure to efficiently solve graph coloring as SAT

IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
2007 | Conference paper
EID:

2-s2.0-49749126465

Part of ISSN: 10923152
Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Formal verification of pipelined microprocessors with delayed branches

Proceedings - International Symposium on Quality Electronic Design, ISQED
2006 | Conference paper
EID:

2-s2.0-80455152221

Part of ISSN: 19483287 19483295
Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Using abstraction for efficient formal verification of pipelined processors with value prediction

Proceedings - International Symposium on Quality Electronic Design, ISQED
2006 | Conference paper
EID:

2-s2.0-84886745524

Part of ISSN: 19483287 19483295
Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Automatic formal verification of liveness for pipelined processors with multicycle functional units

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2005 | Book
EID:

2-s2.0-33646398590

Part of ISSN: 03029743 16113349
Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Comparison of schemes for encoding unobservability in translation to SAT

Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
2005 | Conference paper
EID:

2-s2.0-84861451904

Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Integrating formal verification into an advanced computer architecture course

IEEE Transactions on Education
2005 | Journal article
EID:

2-s2.0-20344406225

Part of ISSN: 00189359
Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

TLSim and EVC: a term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories

International Journal of Embedded Systems
2005 | Journal article
EID:

2-s2.0-51549105845

Part of ISSN: 17411076 17411068
Contributors: Velev, M.N.; Bryant, R.E.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

A new generation of ISCAS benchmarks from formal verification of high-level microprocessors

Proceedings - IEEE International Symposium on Circuits and Systems
2004 | Conference paper
EID:

2-s2.0-4344716058

Part of ISSN: 02714310
Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Comparative study of strategies for formal verification of high-level processors

Proceedings - IEEE International Conference on Computer Design: VLSI in Computers and Processors
2004 | Conference paper
EID:

2-s2.0-17644416138

Part of ISSN: 10636404
Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Efficient formal verification of pipelined processors with instruction queues

Proceedings of the ACM Great Lakes Symposium on VLSI
2004 | Conference paper
EID:

2-s2.0-2942630759

Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Efficient translation of boolean formulas to CNF in formal verification of microprocessors

Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
2004 | Conference paper
EID:

2-s2.0-2442557232

Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Exploiting signal unobservability for efficient translation to CNF in formal verification of microprocessors

Proceedings - Design, Automation and Test in Europe Conference and Exhibition
2004 | Conference paper
EID:

2-s2.0-3042660498

Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Formal verification of pipelined processors with load-value prediction

Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT
2004 | Conference paper
EID:

2-s2.0-19944405796

Part of ISSN: 15526674
Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Using positive equality to prove liveness for pipelined microprocessors

Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
2004 | Conference paper
EID:

2-s2.0-2442500564

Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Automatic abstraction of equations in a logic of equality

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2003 | Book
EID:

2-s2.0-7044252008

Part of ISSN: 16113349 03029743
Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs

IEEE International Test Conference (TC)
2003 | Conference paper
EID:

2-s2.0-0142153743

Part of ISSN: 10893539
Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors

Journal of Symbolic Computation
2003 | Journal article
EID:

2-s2.0-0037331793

Part of ISSN: 07477171
Contributors: Velev, M.N.; Bryant, R.E.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Formal verification of an Intel XScale processor model with scoreboarding, specialized execution pipelines, and impress data-memory exceptions

Proceedings - 1st ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE 2003
2003 | Conference paper
EID:

2-s2.0-3042639039

Contributors: Srinivasan, S.K.; Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Integrating formal verification into an advanced computer architecture course

ASEE Annual Conference Proceedings
2003 | Conference paper
EID:

2-s2.0-8744290910

Part of ISSN: 01901052
Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Boolean Satisfiability with Transitivity Constraints

ACM Transactions on Computational Logic
2002 | Journal article
EID:

2-s2.0-84974717885

Part of ISSN: 1557945X 15293785
Contributors: Bryant, R.E.; Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Using rewriting rules and positive equality to formally verify wide-issue out-of-order microprocessors with a reorder buffer

Proceedings -Design, Automation and Test in Europe, DATE
2002 | Conference paper
EID:

2-s2.0-84893735603

Part of ISSN: 15301591
Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Automatic abstraction of memories in the formal verification of superscalar microprocessors

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2001 | Book
EID:

2-s2.0-84903158789

Part of ISSN: 16113349 03029743
Contributors: Velev, M.N.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier

Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors

Proceedings - Design Automation Conference
2001 | Conference paper
EID:

2-s2.0-0034854260

Part of ISSN: 0738100X
Contributors: Velev, M.N.; Bryant, R.E.
Source: Self-asserted source
Miroslav Velev via Scopus - Elsevier
Items per page:
Page 1 of 2