Incomplete or partial specifications arise out of mistakes in design, or in purpose to avoid loss of generality in application. When designing a system with several partially specified functions, we often impose constraints on the global behavior of the system. In this paper, we study the problem of verifying whether a set of partially specified functions meets such constraints. We show that the problem is $\Pi_2^P$ complete. While symbolic BDD-based algorithms have been widely used for propositional satisfiability ($\Sigma_1^P$ complete) and validity ($\Pi_1^P$ complete) problems, the structure of BDDs is not natural for solving $\Pi_2^P$ complete problems. We present a two-step BDD-based method for solving the above $\Pi_2^P$ complete problem and show that the method is effective when the number of functions is small.
In IEEE Symp. on Circ. and Systems (ISCAS), May 2001, Sydney, Australia.