Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
type: Item
instance of: scholarly article
title: Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
zbMATH Open document ID: 1069.68119
DOI: 10.1016/S0747-7171(02)00091-3
author: Miroslav N. Velev
author: Randal E. Bryant
published in: Journal of Symbolic Computation
publication date: 2004-03-14T00:00:00Z
Mathematics Subject Classification ID: 68W35
Mathematics Subject Classification ID: 68M07
zbMATH DE Number: 2056553
zbMATH Keywords: SAT-checkers
zbMATH Keywords: decision diagrams
zbMATH Keywords: equality with uninterpreted functions and memories
describes a project that uses: BerkMin
describes a project that uses: DIMACS
describes a project that uses: Velev SAT Benchmarks
describes a project that uses: Walksat
describes a project that uses: Chaff
describes a project that uses: EVC
describes a project that uses: SATO
MaRDI profile type: Publication
cites work: Solvable cases of the decision problem
cites work: Q4473048
cites work: Q4553262
cites work: Graph-Based Algorithms for Boolean Function Manipulation
cites work: Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
cites work: Boolean satisfiability with transitivity constraints
cites work: Bounded model checking using satisfiability solving
cites work: Q4551177
cites work: Experimental results on the crossover point in random 3-SAT
cites work: A machine program for theorem-proving
cites work: A Computing Procedure for Quantification Theory
cites work: BerkMin: A fast and robust SAT-solver
cites work: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems
cites work: The propositional formula checker HeerHugo
cites work: Design of experiments and evaluation of BDD ordering heuristics
cites work: Q4003964
cites work: Q4475671
cites work: Q4276004
cites work: Stochastic systematic search algorithms for satisfiability
cites work: Q4473057
cites work: GRASP: a search algorithm for propositional satisfiability
cites work: Q4864698
cites work: Zero-suppressed BDDs and their applications
cites work: A satisfiability procedure for quantified Boolean formulae
cites work: Q4818813
cites work: Q5687271
cites work: A discrete Lagrangian-based global-search method for solving satisfiability problems
cites work: Efficient manipulation of decision diagrams
cites work: Q2754092
cites work: Q2769591
cites work: Q4553255
cites work: Formal verification based on Boolean expression diagrams
cites work: Q2754079
cites work: SATO: An efficient propositional prover
description: scientific article; zbMATH DE number 2056553