Application of Lifting in Partial Design Analysis

In the past, we have investigated satisfiability-based combinational equivalence checking and bounded model checking of partial circuit designs, i.e., circuit designs where one or more components of the design are not implemented yet. Especially for satisfiability-based bounded model checking, typically a counterexample is generated in case that the specification property is violated. Minimizing the number of assigned variables in the satisfying assignment that corresponds to such a counterexample is the objective of lifting. In this work we show that lifting is also feasible and profitable for counterexamples obtained via satisfiability-based bounded model checking of partial designs. We provide first experimental results on this issue that show its feasibility. Furthermore, we present a novel application scenario for lifting in the context of automated blackbox synthesis. This is a useful concept that can be applied during combinational equivalence checking of partial circuit designs, where realizability of the missing components was already proven, but the functionality of the missing components is still unknown. As a summary, this work provides first experimental results as well as a novel concept regarding the application of lifting for the analysis of partial designs.