Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
From MaRDI portal
Publication:1426130
DOI10.1016/S0747-7171(02)00091-3zbMath1069.68119MaRDI QIDQ1426130
Randal E. Bryant, Miroslav N. Velev
Publication date: 14 March 2004
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Hardware implementations of nonnumerical algorithms (VLSI algorithms, etc.) (68W35) Mathematical problems of computer architecture (68M07)
Related Items (14)
Backdoors to Satisfaction ⋮ Exploiting multivalued knowledge in variable selection heuristics for SAT solvers ⋮ The state of SAT ⋮ Regular-SAT: A many-valued approach to solving combinatorial problems ⋮ Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) ⋮ NuMDG: a new tool for multiway decision graphs construction ⋮ Constrained pseudo-propositional logic ⋮ Decomposing SAT Instances with Pseudo Backbones ⋮ Visualizing SAT instances and runs of the DPLL algorithm ⋮ Empirical Study of the Anatomy of Modern Sat Solvers ⋮ UnitWalk: A new SAT solver that uses local search guided by unit clause elimination ⋮ A formal methods approach to predicting new features of the eukaryotic vesicle traffic system ⋮ \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver ⋮ Backdoors to q-Horn
Uses Software
Cites Work
- A discrete Lagrangian-based global-search method for solving satisfiability problems
- A satisfiability procedure for quantified Boolean formulae
- Zero-suppressed BDDs and their applications
- Efficient manipulation of decision diagrams
- Design of experiments and evaluation of BDD ordering heuristics
- Formal verification based on Boolean expression diagrams
- Heavy-tailed phenomena in satisfiability and constraint satisfaction problems
- The propositional formula checker HeerHugo
- BerkMin: A fast and robust SAT-solver
- Solvable cases of the decision problem
- Experimental results on the crossover point in random 3-SAT
- Graph-Based Algorithms for Boolean Function Manipulation
- GRASP: a search algorithm for propositional satisfiability
- SATO: An efficient propositional prover
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
- Boolean satisfiability with transitivity constraints
- Bounded model checking using satisfiability solving
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
