This paper describes a new algorithm for extracting unsatisfiable subformulas from a given unsatisfiable CNF formula. Such unsatisfiable cores can be very helpful in diagnosing the causes of infeasibility in large systems. Our algorithm is unique in that it adapts the learning process of a modern SAT solver to identify unsatisfiable subformulas rather than search for satisfying assignments. Compared to existing approaches, this method can be viewed as a bottom-up core extraction procedure which can be very competitive when the core sizes are much smaller than the original formula size. Repeated runs of the algorithm with different branching orders yield different cores. We present experimental results on a suite of large automotive benchmarks showing the performance of the algorithm and highlighting its ability to locate not just one but several cores.

Determining the depth of sequential circuits is a crucial step towards the completeness of bounded model checking proofs in hardware verification. In this paper, we formulate sequential depth computation as a logical inference problem for Quantified Boolean Formulas. We introduce a novel technique to simplify the complexity of the constructed formulas by applying simple transformations to the circuit netlist. We also study the structure of the resulting simplified QBFs and construct an efficient SAT-based algorithm to check their satisfiability. We report promising experimental results on some of the ISCAS 89 benchmarks.

We introduce a new approach to Boolean satisfiability (SAT) that combines backtrack search techniques and zero-suppressed binary decision diagrams (ZBDDs). This approach implicitly represents SAT instances using ZBDDs, and performs search using an efficient implementation of unit propagation on the ZBDD structure. The adaptation of backtrack search algorithms to such an implicit representation allows for a potential exponential increase in the size of problems that can be handled.

We introduce a new verification methodology for modern micro-processors that uses a simple checker processor to validate the exe-cution of a companion high-performance processor. The checker can be viewed as an at-speed emulator that is formally verified to be compliant to an ISA specification. This verification approach en-ables the practical deployment of formal methods without impact-ing overall performance.