Abstract
The dramatic performance improvements of SAT solvers over the past decade have increased their deployment in hardware verification applications. Many problems that were previously too large and complex for SAT techniques can now be handled in an efficient manner. One such problem is reachability analysis, whose instances are found throughout verification applications such as unbounded model checking and trace reduction. In circuit-based reachability analysis important circuit information is often lost during the circuit-to-SAT translation process. Observability Don’t Cares (ODCs) are an example of such information that can potentially help achieve better and faster results for the SAT solver. This work proposes to use the ODCs to improve the quality and performance of SAT-based reachability analysis frameworks. Since ODCs represent variables whose values do not a ect the outcome of a problem, it is possible to satisfy a problem with fewer assigned variables. This in turn leads to more compact solutions and thus fewer solutions to cover the entire solution space. Specifically, this work presents an efficient way to identify ODCs, proves the correctness of leaving ODC variables unassigned, and develops a reachability analysis platform that benefits greatly from the ODCs. The advantages of using ODCs in reachability analysis is demonstrated through extensive experiments on unbounded model checking and trace reduction applications.