Travelled to:1 × Canada
1 × Germany
1 × Israel
1 × Portugal
2 × Italy
3 × France
4 × USA
Collaborated with:R.E.Bryant ∅ P.Gao S.M.German A.Jain
Talks about:microprocessor (7) formal (7) verif (6) equal (6) exploit (4) memori (4) effici (4) posit (4) function (3) satisfi (3)
Person: Miroslav N. Velev
DBLP: Velev:Miroslav_N=
Contributed to:
20082004
20042002
2001
2001
2001200020001999199919981997Wrote 14 papers:
- DATE-2008-VelevG #comparison #encoding #problem #satisfiability
- Comparison of Boolean Satisfiability Encodings on FPGA Detailed Routing Problems (MNV, PG), pp. 1268–1273.
- DATE-v1-2004-Velev #performance #verification
- Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors (MNV), pp. 266–271.
- SAT-2004-Velev #encoding #performance #satisfiability
- Encoding Global Unobservability for Efficient Translation to SAT (MNV), pp. 197–204.
- DATE-2002-Velev #similarity #using #verification
- Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer (MNV), pp. 28–35.
- CAV-2001-VelevB #logic #named #similarity
- EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations (MNV, REB), pp. 235–240.
- DAC-2001-VelevB #effectiveness #satisfiability #using #verification
- Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors (MNV, REB), pp. 226–231.
- TACAS-2001-Velev #abstraction #automation #verification
- Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors (MNV), pp. 252–267.
- CAV-2000-BryantV #constraints #satisfiability #transitive
- Boolean Satisfiability with Transitivity Constraints (REB, MNV), pp. 85–98.
- CAV-2000-Velev #execution #verification
- Formal Verification of VLIW Microprocessors with Speculative Execution (MNV), pp. 296–311.
- DAC-2000-VelevB #branch #exception #functional #multi #predict #verification
- Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction (MNV, REB), pp. 112–117.
- CAV-1999-BryantGV #logic #similarity
- Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions (REB, SMG, MNV), pp. 470–482.
- DAC-1999-VelevB #pipes and filters #similarity #verification
- Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors (MNV, REB), pp. 397–401.
- TACAS-1998-VelevB #array #memory management #modelling #performance #simulation
- Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation (MNV, REB), pp. 136–150.
- CAV-1997-VelevBJ #array #memory management #modelling #performance #simulation
- Efficient Modeling of Memory Arrays in Symbolic Simulation (MNV, REB, AJ), pp. 388–399.