SAT-based sequential depth computation

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.