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

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)

zbMATH Keywords

decision diagramsequality with uninterpreted functions and memoriesSAT-checkers

Mathematics Subject Classification ID

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

• Walksat
• SATO
• Chaff
• BerkMin
• DIMACS
• Velev SAT Benchmarks
• EVC

Cites Work

• 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
• 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

This page was built for publication: Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.