Analysis of Incomplete Circuits Using Dependency Quantified Boolean Formulas

Abstract

We consider Dependency Quantified Boolean Formulas (DQBFs), a generalization of Quantified Boolean Formulas (QBFs), and demonstrate that DQBFs are a natural calculus to exactly express the realizability problem of incomplete combinational and sequential circuits with an arbitrary number of (combinational or bounded-memory) black boxes. In contrast to usual approaches for controller synthesis, restrictions to the interfaces of missing circuit parts in distributed architectures are strictly taken into account. We present a solution method for DQBFs together with the extraction of Skolem functions for existential variables, which can directly serve as implementations for the black boxes. First experimental results are provided.

1 Introduction

Solver-based techniques have proven to be successful in many areas in computer-aided design, ranging from formal verification of digital circuits [1, 3, 9, 29] over automatic test pattern generation [11, 13] to circuit synthesis [4, 5]. While research on solving quantifier-free Boolean formulas (the famous SAT-problem [10]) has reached a certain level of maturity, designing and improving algorithms for quantified Boolean formulas (QBFs) is one focus of active research. However, there are applications like the verification of partial circuits [18, 19, 29], the synthesis of safe controllers [4], and the analysis of games with incomplete information [26] for which QBF is not expressive enough to provide a compact and natural formulation. The reason is that QBF requires linearly ordered dependencies of the existential variables on the universal ones: Each existential variable implicitly depends on all universal variables in whose scope it is. Relaxing this condition yields so-called dependency quantified Boolean formulas (DQBFs). DQBFs are strictly more expressive than QBFs in the sense that an equivalent QBF formulation can be exponentially larger than a DQBF formulation. This comes at the price of a higher complexity of the decision problem: DQBF is NEXPTIME-complete [26], compared to QBF, which is “only” PSPACE-complete. Encouraged by the success of SAT and QBF solvers and driven by the mentioned applications, research on solving DQBFs has started during the last few years [16, 17, 20, 33], yielding first prototypic solvers like iDQ [17] and HQS [20].

In this paper, we focus on the application of DQBF for analyzing incomplete combinational and sequential circuits. Such incomplete circuits appear in early design stages, when only a subset of the system’s modules has already been implemented and verification is applied in order to find errors in the available parts as early as possible. Incomplete circuits also result if the complexity of the verification task is too high and therefore some parts, which are supposed not to influence the validity of some properties, e. g., multiplier or memory modules, have been removed to make verification feasible. Analyzing incomplete circuits is also useful if a designer wants to localize errors (then one can remove parts of the design and if for all possible implementations of the removed parts the error does not disappear, the remaining parts must be erroneous). Therefore this problem has received considerable attention in the research community during the last 15 years, see, e. g., [12, 14, 21, 25, 29–31]. All solver-based approaches are restricted in the sense that they can either only handle a single black box or do not take the interfaces of the black boxes into account, allowing the black boxes to read signals which are not available to them in the actual design.

We show how the realizability problem for incomplete combinational and sequential circuits with an arbitrary number of combinational or bounded-memory black boxes can be expressed as a DQBF. Here we show for the first time a DQBF-based solution for sequential circuits with several bounded-memory black boxes where the exact interface of the black boxes, i.e., the signals entering and leaving the black boxes, can be taken into account. We also show that solving a DQBF has the same complexity as deciding realizability. We do not only sketch how DQBFs are solved in our DQBF solver HQS [20, 33], but also how so-called Skolem functions can be obtained from the solution process, provided that the formula is satisfied [34]. These Skolem functions can directly serve as an implementation of the black boxes.

This paper builds on different sources: [18, 19] applies DQBF-based methods to incomplete combinational circuits with combinational black boxes. SAT- and QBF-based techniques for controller synthesis are considered in [4]; there a footnote gives hints how a DQBF formulation can be used for that purpose. Due to the lack of efficient DQBF solvers at that time, this idea was not investigated further. However the method described there considers only a single black box which can read all primary inputs and the complete state information. The basic techniques implemented in our DQBF solver HQS have been described in [20], and [33] defines preprocessing techniques for DQBF, which speed up the solution process considerably.

1.1 Structure of the Paper

In the next section, we introduce dependency quantified Boolean formulas (DQBFs). In Sect. 3, we describe how realizability of incomplete combinational and sequential circuits can be formulated as a DQBF. Section 4 presents a method to solve DQBFs and to obtain Skolem functions for satisfied DQBFs. In Sect. 5 we give preliminary experimental results, and we conclude the paper in Sect. 6, pointing out challenges which need to be solved.

2 Foundations

Let φ and κ be quantifier-free Boolean formulas over the set V of Boolean variables and v ∈ V . We denote by φ[κ/v] the Boolean formula which results from φ by replacing all occurrences of v (simultaneously) by κ. For a set V ′⊆ V , we denote by $\mathcal {A}(V')$ the set of Boolean assignments for V ′, i.e., $\mathcal {A}(V')=\big \{\nu \,\big |\,\nu :V'\to \{0,1\}\big \}$. For each quantifier-free formula φ over V , a variable assignment ν to the variables in V induces a truth value 0 or 1 of φ, which we call ν(φ).

Definition 1 (Syntax of DQBF)

Let V = {x ₁, …, x _n , y ₁, …, y _m } be a set of Boolean variables. A dependency quantified Boolean formula (DQBF) ψ over V has the form $\psi := \forall x_1\ldots \forall x_n\exists y_1(D_{y_1})\ldots \exists y_m(D_{y_m}):\varphi ,$ where $D_{y_i}\subseteq \{x_1,\ldots ,x_n\}$ for i = 1, …, m is the dependency set of y _i , and φ is a quantifier-free Boolean formula over V , called the matrix of ψ.

$V^{\forall }_{\psi } = \{x_1,\ldots ,x_n\}$ denotes the set of universal and $V^{\exists }_{\psi } = \{y_1,\ldots ,y_m\}$ the set of existential variables. We often write ψ = Q : φ with the quantifier prefix Q and the matrix φ. Q ∖{v} denotes the prefix that results from removing a variable v ∈ V from Q together with its quantifier. If v is existential, then its dependency set is removed as well; if v is universal, then all occurrences of v in the dependency sets of existential variables are removed. Similarly we use Q ∪{∃y(D _y )} to add existential variables to the prefix. We sometimes assume that a DQBF ψ = Q : φ as in Definition 1 with φ in conjunctive normal form (CNF) is given. A formula is in CNF if it is a conjunction of (non-tautological) clauses; a clause is a disjunction of literals, and a literal is either a variable v or its negation ¬v. As usual, we identify a formula in CNF with its set of clauses and a clause with its set of literals. For a formula φ (resp. clause C, literal ℓ), var(φ) (resp. var(C), var(ℓ)) means the set of variables occurring in φ (resp. C, ℓ), lit(φ) (lit(C)) means the set of literals occurring in φ (C).

A quantified Boolean formula (QBF) (in prenex normal form) is a DQBF such that $D_y\subseteq D_{y'}$ or $D_{y'}\subseteq D_y$ holds for any two existential variables $y,y'\in V^{\exists }_{\psi }$. Then the variables in V can be ordered resulting in a linear quantifier prefix, such that for each $y \in V^{\exists }_{\psi }$, D _y equals the set of universal variables which are to the left of y.

The semantics of a DQBF is usually defined by so-called Skolem functions.

Definition 2 (Semantics of DQBF)

Let ψ be a DQBF as above. It is satisfiable, iff there are functions $s_y:\mathcal {A}(D_y)\to \mathbb {B}$ for $y\in V^{\exists }_{\psi }$ such that replacing each $y\in V^{\exists }_{\psi }$ by (a Boolean expression for) s _y turns φ into a tautology. The functions $(s_y)_{y\in V^{\exists }_{\psi }}$ are called Skolem functions for ψ.

Example 1

Consider the following DQBF:

$$\displaystyle \begin{aligned} \forall x_1\forall x_2\exists y_1(x_1)\exists y_2(x_2): (x_1\vee \neg y_1)\land (x_2\vee y_1\vee y_2)\end{aligned} $$

Here the variable y ₁ depends only on x ₁, but not on x ₂; y ₂ depends only on x ₂, but not on x ₁. It is satisfied by using the Skolem functions $s_{y_1}(x_1) = x_1$ and $s_{y_2}(x_2) = \neg x_2$. Replacing y ₁ and y ₂ by their Skolem functions yields (x ₁ ∨¬x ₁) ∧ (x ₂ ∨ x ₁ ∨¬x ₂), which is obviously a tautology.

3 Analysis of Incomplete Circuits

In this section, we show how DQBFs can be used to analyze incomplete combinational and sequential circuits. In both cases we ask for realizability: Are there implementations of the missing parts (“black boxes”) such that the complete circuit satisfies its specification.

We assume that the missing parts are either combinational or contain only a bounded amount of memory. In the latter case, we can put the flipflops of the black boxes into the available circuit part such that the incoming and outgoing signals of these flipflops are written and read only by the black boxes as sketched in Fig. 7.1.

Fig. 7.1

Sequential circuits with extracted memory

Then the black boxes themselves are purely combinational. Note that the case of several black boxes with an unbounded amount of memory is undecidable [28].

We use the notation for incomplete sequential circuits as sketched in Fig. 7.2. The primary inputs are denoted by x, the current state by s, and the next state by s ′. The missing parts are BB₁, …, BB _n , whose interfaces, i.e., the signals entering and leaving the black boxes, are known. The input signals of black box BB _i are denoted by I _i , its output signals by y _i . The input cone of black box BB _i ensures the constraint I _i  ≡F _i (s, x, y ₁, …, y _i−1), the next state is described by trans:= (s ′≡R(s, x, y ₁, …, y _n )). We assume w. l. o. g. that no black box output is directly connected to an input of another black box or a flipflop, i.e., y _i  ∩I _j  = ∅ for all i, j and s ′∩y _j  = ∅ for all j. Otherwise a buffer is inserted between the two black boxes without changing the functionality of the circuit. Additionally we assume that there are no cyclic dependencies between the combinational black boxes, i.e., that BB _i only depends on the outputs of BB₁, …, BB _i−1. Otherwise, implementing the black boxes with combinational circuits can lead to cycles in the combinational part of the circuit which do not run through memory elements. This can cause undefined behavior of the circuit.

Fig. 7.2

Notation for incomplete sequential circuits

We consider invariant properties inv(s, x, y ₁, …, y _n ), defined over the primary inputs x, the current state s and the black box outputs y ₁, …, y _n , which are required to hold at any time.

3.1 Combinational Circuits

The same notation as introduced above is also used for combinational circuits. Here, the state and next state signals s and s ′ as well as the memory elements are omitted.

Definition 3

The partial equivalence checking problem (PEC) is defined as follows: Given an incomplete circuit C _impl and a (complete) specification C _spec, are there implementations of the black boxes in C _impl such that C _impl and C _spec become equivalent?

In the following, we assume that (incomplete) implementation C _impl and specification C _spec are combined into a single circuit using a miter construction: Corresponding primary inputs are connected, corresponding outputs are connected via XOR gates. The outputs of the XOR gates are combined via OR gates into a single output signal. This output signal is constantly one iff, for some implementation of the black boxes, the two circuits are equivalent. This can be considered as a kind of invariant property, valid at the primary output of the combined circuit.

We now show how a DQBF formulation can be used to decide PEC.

Consider a PEC problem with black boxes BB₁, …, BB _n . We first construct the quantifier prefix of the DQBF. The primary inputs x and the black box inputs I ₁, …, I _n are universally quantified, all other variables are existentially quantified. The dependency set of black box outputs y _i contains exactly the inputs I _i of BB _i . Hence the quantifier prefix is

$$\displaystyle \begin{aligned} \forall{\mathbf x}\forall{\mathbf I}_1 \dots \forall{\mathbf I}_n \exists{\mathbf y}_1({\mathbf I}_1) \dots \exists{\mathbf y}_m({\mathbf I}_m)\,. \end{aligned}$$

If the black boxes are not directly connected to the primary inputs but to internal signals, we have to take into account that not all possible combinations of values may arrive at the inputs of the black boxes. Since we use a universal quantification for the black box inputs we have to ensure that our formula is satisfied if the value of the black box inputs I _i deviates from the values obtained as a function F _i (x, I ₁, …, I _i−1).

$$\displaystyle \begin{aligned} \varphi({\mathbf x},{\mathbf I}_1,\ldots,{\mathbf I}_n,{\mathbf y}_1,\ldots,{\mathbf y}_n):= \left(\bigwedge_{i=1}^n {\mathbf I}_i\equiv\mathbf F_i\right)\Rightarrow \mathrm{inv}({\mathbf x},{\mathbf y}_1,\ldots,{\mathbf y}_n)\,. \end{aligned}$$

This formula is not necessarily given in CNF. By applying Tseitin transformation [32], which is essentially introducing auxiliary variables for the internal signals of the circuit, one can obtain a CNF φ′ that is equisatisfiable to φ and whose size is linear in the size of φ. Let a be the vector of these auxiliary variables, which are existentially quantified in the quantifier prefix. As their values are implied by the values of the variables in their input cone, we can use as their dependency sets either the universal variables in their input cone or the set of all universal variables (or any set in between). We prefer making the Tseitin variables depend on all universal variables, because this typically leads to DQBFs that are easier to solve.

The resulting DQBF is:

$$\displaystyle \begin{aligned} \psi := {}& \forall{\mathbf x}\forall{\mathbf I}_1\dots\forall{\mathbf I}_n \exists{\mathbf y}_1 ({\mathbf I}_1) \dots \exists{\mathbf y}_n ({\mathbf I}_n) \exists{\mathbf a}({\mathbf x},{\mathbf I}_1,\ldots,{\mathbf I}_n): \\ &\qquad\varphi'({\mathbf x}, {\mathbf I}_1,\dots, {\mathbf I}_n, {\mathbf y}_1 , \dots, {\mathbf y}_n, {\mathbf a} )\,. \end{aligned} $$

This formula ψ is satisfied iff we can replace all y _i (I _i ) with Skolem functions s _i (I _i ) such that φ′ becomes a tautology. The Skolem functions s _i exist if and only if there are implementations for the black boxes BB _i of the PEC, such that the PEC is satisfied. Therefore any PEC can be translated with linear effort into a DQBF and the PEC is satisfied iff the DQBF is satisfied.

It is easy to see that there is also the converse transformation [19]: Each DQBF can be turned into a PEC, having one black box for each existential variable such that the PEC is realizable iff the DQBF is satisfiable. This implies that PEC is NEXPTIME-complete.

3.2 Sequential Circuits

For incomplete sequential circuits with multiple combinational or bounded-memory black boxes, we investigate the following problem:

Definition 4

The realizability problem for incomplete sequential circuits (RISC) is defined as follows: Given an incomplete sequential circuit with multiple combinational (or bounded-memory) black boxes and an invariant property, are there implementations of the black boxes such that in the complete circuit the invariant holds at all times?

To decide RISC, one can apply a generalization of ideas described in [4] for the synthesis of controllers (which are in fact single black boxes with access to all state bits and all primary circuit inputs).

According to the notations introduced in the previous section, let s denote the variables encoding the current state of the circuit, s ′ the next state, and x the primary inputs. The formulas F ₁, …, F _n describe the input cones of the black boxes, I ₁, …, I _n their inputs, y ₁, …, y _n their outputs, and R is the next state function of the circuit. Additionally we assume that init represents the circuit’s initial state(s) and inv its states that satisfy the invariant.

Definition 5

A subset W ⊆ S is a winning set if all states in W satisfy the invariant and, for all values of the primary inputs, the black boxes can ensure (by computing appropriate values) that the successor state is again in W.

A given RISC is realizable if there is a winning set that includes the initial state of the circuit. This can be formulated as a DQBF. To encode the winning sets, we introduce two existential variables w and w′; w depends on the current state and is supposed to be true for a state s if s is in the winning set. The variable w′ depends on the next state variables s ′ and has the same Skolem function as w (but defined over s ′ instead of s). We ensure that w and w′ have the same semantics by the condition (s ≡s ′⇒ w ≡ w′).

Similar to the combinational case, we have to take into account that the black boxes are typically not directly connected to the primary inputs, but to internal signals. This is done by restricting the requirement that the successor state is again a winning state to the case when the black box inputs are assigned consistently with the values computed by their input cones.

Theorem 1

Given a RISC as defined above, the following DQBF is satisfied if and only if the RISC is realizable:

$$\displaystyle \begin{aligned} \forall{\mathbf s}\,\forall{\mathbf s\,'}\forall{\mathbf x}\,\forall{\mathbf I}_1\ldots\forall{\mathbf I}_n\ \exists{\mathbf y}_1({\mathbf I}_1)\ldots\exists{\mathbf y}_n({\mathbf I}_n)\ \exists w({\mathbf s})\ \exists w'({\mathbf s\,'}): \\ \big( \mathrm{init}\Rightarrow w\big)\land \big( w\Rightarrow\mathrm{inv}\big) \land \big( {\mathbf s}\equiv{\mathbf s\,'}\Rightarrow w\equiv w'\big)\\ \land {} \Big(\big ( w\land \bigwedge_{i=1}^n {\mathbf I}_i\equiv\mathbf F_i \land {\mathbf s\,'}\equiv R\big)\Rightarrow w'\Big). \end{aligned} $$

Theorem 2

RISC is NEXPTIME-complete.

Proof

The reduction to DQBF above shows that RISC is in NEXPTIME. To show the hardness, we give a reduction from DQBF to RISC. First we transform the DQBF into an incomplete combinational circuit as shown in [18] such that the output of the circuit is constantly 1 iff the DQBF is satisfied. We now turn this combinational circuit into a sequential circuit with two states by storing the output of the combinational circuit in a 1-bit flipflop s. The initial state is s ≡ 1, the invariant is given by s ≡ 1. The original DQBF is satisfied iff the unsafe state 0 can be made unreachable by appropriate black box implementations. □

Example 2

We illustrate the solution of RISC using two incomplete circuits in Figs. 7.3 and 7.4. The circuits are simple, but still illustrate the basic idea. We first start with the circuit in Fig. 7.3. The sequential circuit in Fig. 7.3 consists of two parts. The first part on the left can be seen as the specification for a simple sequential circuit: There are two bit streams applied to the inputs bit₁ and bit₂. The circuit computes the parities of the bit streams applied to bit₁ and bit₂ and outputs 1 iff the parity for bit stream bit₁ is smaller or equal to the parity for bit stream bit₂. The right-hand side shows a given architecture for an implementation with two black boxes, one reading bit stream bit₁ and the other reading bit stream bit₂. The outputs of the black boxes are connected by an equivalence gate. Then the output of the overall circuit is computed by an equivalence gate connecting the outputs of specification and incomplete implementation. We require the invariant property that the output of the overall circuit is 1 at all times, i.e., that the black boxes are implemented in a way such that the implementation part agrees with the specification part. For this simple example it is easy to see that a corresponding implementation does not exist, even for black boxes with unbounded memory. Here we use our method where the number of flip flops for each black box is restricted to one. Figure 7.3 already shows the transformed circuit where the memory is extracted from the black boxes.

Fig. 7.3

Sequential circuit with two black boxes

Fig. 7.4

The same sequential circuit as in Fig. 7.3, but with a single black box

Applying Theorem 1, we obtain the following formula parts:

• initial state:

  $$\displaystyle \begin{aligned} \mathrm{init}:= {} & (\neg s_1\land \neg s_2\land\neg i_1\land\neg i_2) \end{aligned} $$

• transition relation:

  $$\displaystyle \begin{aligned} \mathrm{trans} := {} & (s_1^{\prime} \equiv s_1\oplus\mathrm{bit_1})\land (s_2^{\prime} \equiv s_2\oplus\mathrm{bit_1}) \\ & \qquad {} \land (i_1^{\prime} \equiv y_2^1)\land (i_2^{\prime}\equiv y_2^2) \end{aligned} $$

• invariant:

  $$\displaystyle \begin{aligned} \mathrm{inv}:= {} & \big(\neg s_1\vee s_2)\equiv (y_1^1\equiv y_2^1)\big) \end{aligned} $$

Putting these parts together yields the following DQBF:

$$\displaystyle \begin{aligned} \forall \mathrm{bit}_1\forall\mathrm{bit}_2\forall s_1\forall s_1^{\prime}\forall s_2\forall s_2^{\prime} \forall i_1\forall i_1^{\prime}\forall i_2\forall i_2^{\prime} \\ \exists y_1^1(i_1,\mathrm{bit}_1) \exists y_2^1(i_1,\mathrm{bit}_1) \exists y_1^2(i_2,\mathrm{bit}_2) \exists y_2^2(i_2,\mathrm{bit}_2) \\ \exists w(s_1,s_2,i_1,i_2)\exists w'(s_1^{\prime},s_2^{\prime},i_1^{\prime},i_2^{\prime}): \\ (\mathrm{init}\Rightarrow w) \land (w\Rightarrow \mathrm{inv}) \land \big((w\land\mathrm{trans})\Rightarrow w'\big) \\ \land \big(((s_1\equiv s_1^{\prime})\land (s_2\equiv s_2^{\prime})\land (i_1\equiv i_1^{\prime})\land (i_2\equiv i_2^{\prime}))\Rightarrow (w\equiv w')\big) \end{aligned} $$

By applying a DQBF solver, one can verify that this formula is unsatisfiable, meaning that the design in Fig. 7.3 is not realizable.

Now consider the circuit in Fig. 7.4. It differs from the design in Fig. 7.3 only in the black boxes: Both black boxes can read both input signals bit₁ and bit₂. Thus, the black boxes can equivalently be merged into one as shown in Fig. 7.4. It is easy to see that this implementation, which does not pay attention to the exact architecture by disregarding the interface of the black boxes, is now realizable. More precisely, it is realizable if we assume that the black box with bounded memory has at least 2 memory cells at its disposal. In Fig. 7.4 we depict the incomplete circuit with two memory cells extracted from the black box. Using our approach we can indeed prove realizability. The formula differs only in the dependency sets of the black box outputs: $D_{y_1^1} = D_{y_2^1} = D_{y_1^2} = D_{y_2^2} = \{ \mathrm {bit}_1, \mathrm {bit}_2, i_1, i_2\}$. Now the formula is satisfiable. The following Skolem functions turn the matrix into a tautology:

Variable	$y_1^1$	$y_2^1$	$y_1^2$	$y_2^2$	w	w′
Skolem function	1	bit1 ⊕ i 1	¬i 1 ∨ i 2	bit2 ⊕ i 2	1	1

Using these Skolem functions, the two flipflops in the right half store the same values as the two flipflops in the left half, i.e., s ₁ = i ₁ and s ₂ = i ₂. The equivalence $y^1_1\equiv y^1_2$ corresponds to 1 ≡ (¬i ₁ ∨ i ₂), which is the same as i ₁ ≤ i ₂. Therefore the design is realizable.

For both incomplete circuits, our solver HQS [20] solved the DQBF in at most 0.1 s.

We can conclude that it is necessary to take the precise interfaces of the black boxes into account in order to obtain a valid answer whether the design is realizable.

4 Solving DQBFs

Elimination-based DQBF solvers like HQS [20, 33] apply a series of satisfiability-preserving transformation steps to the formula until a SAT or QBF problem results, which can be solved by an arbitrary SAT or QBF solver. As a pure yes/no answer is not satisfactory when solving analysis problems as presented in the previous section, we provide the main ideas how Skolem functions can be extracted from the solution process. More details can be found in [34, 35]. This extraction proceeds in the reverse order of transformation, starting with (constant) Skolem functions for the final SAT problem, which correspond to a satisfying assignment.

4.1 Transformation Steps

The central operation of elimination-based solvers is the elimination of existential and universal variables from the formula. QBF solvers can eliminate variables in the order given by the quantifier prefix (starting with the inner-most variable block). Because there is no linear order on the variables in a DQBF, this is typically no longer possible.

Lemma 1

Let ψ = Q : ϕ be a DQBF and $y\in V^{\exists }_{\psi }$ an existential variable which depends on all universal variables. Then ψ is equisatisfiable to ψ′:= Q ∖{∃y(D _y )} : ϕ[0/y] ∨ ϕ[1/y].

If $s^{\psi '}_z$ for $z\in V^{\exists }_{\psi '}$ are Skolem functions for the formula ψ′, obtained by eliminating $y\in V^{\exists }_{\psi }$, we set $s^{\psi }_y:= \phi [1/y][s^{\psi '}_z/z]$ and $s^{\psi }_z:= s_z^{\psi '}$ for z ≠ y. This yields Skolem functions for ψ [34].

The elimination of universal variables in solvers like HQS [20] is done by universal expansion [2, 7, 8, 19]. This is applicable even if some existential variables depend on the expanded universal one.

Lemma 2

For a DQBF $\psi =\forall x_1\ldots \forall x_n\exists y_1(D_{y_1})$ $\ldots \exists y_m(D_{y_m}):\varphi$ with $E_{x_i} = \big \{y_j \in V^{\exists }_{\psi }\,\big |\,x_i\in D_{y_j})\big \}$ , the universal expansion w.r.t. variable $x_i\in V^{\forall }_{\psi }$ , is defined by

$$\displaystyle \begin{aligned} \big(Q\setminus\{x_i\}\big)\cup\big\{ \exists y_j^{\prime}(D_{y_j}\setminus\{x_i\})\,\big|\,y_j\in E_{x_i}\big\} : \\ \varphi[1/x_i]\land\varphi[0/x_i][y_j^{\prime}/y_j { \ for \ all \ } y_j\in E_{x_i}]\,. \end{aligned} $$

That means, when eliminating a universal variable $x\in V^{\forall }_{\psi }$, we have to copy all existential variables $y\in V^{\exists }_{\psi }$ that depend on x.

Assume that $s^{\psi '}_z$ for $z\in V^{\exists }_{\psi '}$ are Skolem functions for ψ′. Then $s^{\psi }_y:= (x\land s^{\psi '}_{y'})\lor (\neg x\land s_y^{\psi '})$ for $y\in V^{\exists }_{\psi }$ with x ∈ D _y and $s_z^{\psi }:= s_y^{\psi '}$ for $z\in V^{\exists }_{\psi }$ with x∉D _z are Skolem functions for ψ [34].

In principle, these two operations suffice to turn each DQBF into an (exponentially larger) SAT problem. In order to reduce computation time and memory consumption, pre- and inprocessing steps have turned out to be essential.

Standard operations are the detection of unit and pure literals. A literal ℓ is unit if (ℓ) is a clause in the formula. A literal ℓ is pure if ¬ℓ does not appear in the formula. In both cases var(ℓ) can be replaced by a constant (which is also the Skolem function for that variable). Further preprocessing techniques like blocked clause elimination, the identification of equivalent variables, and structure extraction have been devised for DQBF [33, 36]. All of them are supported when Skolem functions are to be computed. We refer to [34] for more details.

4.2 Elimination Sets

Since the expansion of all universal variables leads to an exponentially larger SAT instance, this is typically not feasible. Instead, the solver HQS eliminates variables only until a QBF is obtained, which can be solved by an arbitrary QBF solver. The central problem is to determine a minimum set of universal variables whose elimination turns the DQBF into a QBF [20]. To solve this, we can use the following dependency graph:

Definition 6

Let ψ be a DQBF. Its dependency graph $G_\psi =(V^{\exists }_{\psi }, E_\psi )$ is a directed graph with the existential variables as its nodes and edges $E_\psi = \{ (y,z)\in V^{\exists }_{\psi }\times V^{\exists }_{\psi }\,|\, D_y\not \subseteq D_z\}$.

It can be used to recognize if a DQBF is actually a QBF:

Lemma 3

Let ψ be a DQBF. Its dependency graph G _ψ is acyclic iff ψ has an equivalent QBF prefix.

That means we have to find a minimum set $U\subseteq V^{\forall }_{\psi }$ of universal variables whose elimination makes G _ψ acyclic. One can show that for making the graph acyclic by eliminating universal variables, it suffices to consider the cycles of length 2. The selection of variables can be done using a MAXSAT solver: for each universal variable x a variable m _x is created in the MAXSAT solver such that m _x  = 1 means that x needs to be eliminated. Soft clauses are used to get an assignment with a minimum number of variables assigned to 1. Hard clauses enforce that for all $y,z\in V^{\exists }_{\psi }$, y ≠ z, either all variables in D _y  ∖ D _z or in D _z  ∖ D _y are eliminated.

The variables in U are then eliminated, ordered according to the number of existential variables that depend upon them.

For more details, including formal correctness proofs, we refer the reader to [20].

4.3 Solver Overview

Figure 7.5 shows the structure of the general-purpose DQBF solver HQS. The input is a DQBF in CNF. After preprocessing, which is done on the CNF, gate detection is applied, essentially undoing Tseitin transformation and removing the existential variables introduced by the CNF transformation. The result is a representation of the formula as an And-Inverter graph (AIG), on which the further steps are performed. Before the actual elimination loop starts, we determine a minimum elimination set as described above.

Fig. 7.5

Structure of the solver (adapted from [20])

Within the elimination loop, we check for unit and pure variables, which can be replaced by constants. This is done on the AIG using syntactic checks. Additionally, all existential variables are eliminated for which this is possible. Otherwise they would double for each eliminated universal variable. Then we check if the dependency graph has already become acyclic. If this is the case we generate the corresponding QBF prefix and solve the formula using the QBF solver AIGsolve [27], which operates directly on AIGs. Otherwise we select the next universal variable to eliminate and expand it.

5 Experimental Results

In the following, we present preliminary experimental results for incomplete combinational circuits. To solve the DQBFs, we use our elimination-based DQBF solver HQS [20], which was described briefly in the previous section.

We have extended HQS by the possibility to compute Skolem functions for satisfied DQBFs. The computation of Skolem functions works in two phases: During the solution process we collect the necessary data and store it on a stack. When the satisfiability of the formula has been determined, we free the other data structures of the solver and extract the Skolem functions from the collected data. We can apply don’t-care minimization to the Skolem functions, based on Craig interpolants [24], and use the tool ABC [6] for further minimization of the Skolem functions’ AIG representation.

All experiments were run on one Intel Xeon E5-2650v2 CPU core at 2.60 GHz clock frequency and 64 GB of main memory under Ubuntu Linux as operating system. We aborted all experiments which either took more than 1000 s CPU time or more than 8 GB ( = 2³⁰ bytes) of main memory. As benchmarks we used 4318 DQBF instances from different sources. Most of them are DQBFs resulting from equivalence checking of incomplete combinational circuits [15, 17, 19]. The remaining ones are controller synthesis problems [4]. The sizes of the circuits range from a few hundred to a few thousand gates. The incomplete circuits contain one to five randomly selected black boxes. The controller synthesis problems are essentially sequential circuits with a single black box.

We first compare the efficiency of HQS with the only other available DQBF solver iDQ [17], which solves the formula by iteratively solving SAT instances generated from the DQBF. Both solvers were run after preprocessing the DQBFs. Since iDQ relies on a formula in CNF, while HQS does not, different preprocessing operations had to be applied: besides standard techniques like the detection of unit and pure literals and equivalent variables, preprocessing for HQS applies gate detection, which reverses Tseitin transformation in order to reconstruct the original circuit. This is not possible in case of iDQ. Instead, for iDQ, we apply blocked clause elimination and variable elimination by resolution, which are both not beneficial for HQS. We refer the reader to [33, 36] for more details on DQBF preprocessing.

Figure 7.6 shows the results for incomplete combinational circuits (left, 3686 instances) and instances from controller synthesis (right, 89 instances) for those instances that could be solved by at least one solver; the remaining 543 instances could not be solved. The controller synthesis instances are incomplete sequential circuits with a single black box that can read all state bits and all primary inputs. We can observe in both cases, that HQS (with few exceptions) is more efficient and solves considerably more instances than iDQ. A closer look shows that the computation time and memory consumption is strongly influenced by the number of universal variables which have to be eliminated in order to obtain an equisatisfiable QBF. This is caused by the copies of the existential variables that are created when eliminating universal variables.

Fig. 7.6

Computation times (in seconds) of HQS and iDQ (both with preprocessing) on PEC instances [15, 17, 20] (left) and instances from controller synthesis [4] (right)

In spite of the improvements made during the last few years, the size of the instances that can effectively be solved is smaller by roughly one to two orders of magnitude than solvable QBF instances—strongly dependent on the number of variable copies which are created to obtain an equisatisfiable QBF.

The second set of experiments concerns the computation of Skolem functions for satisfiable DQBFs. We first measured the overhead of collecting the necessary data for computing Skolem functions during the solution process, i.e., until the truth value of the formula has been determined. The results are shown in Fig. 7.7. We can observe that the overhead is in most cases negligible—in a very few cases, the memory consumption is even reduced. The reason for this behavior is that within the AIG package different optimizations like rewriting are triggered when certain thresholds are exceeded. This can lead to smaller AIGs and thus save memory (and computation time for the subsequent operations).

Fig. 7.7

Overhead of Skolem function computation on memory consumption (left) and running time (right)

For all 720 satisfiable instances we were able to solve without Skolem functions, we could also compute Skolem functions. For these instances we compare the sizes of the Skolem functions with and without optimizations using interpolation and ABC. Figure 7.8 displays the results. In many cases, we can reduce the sizes of the Skolem functions considerably, sometimes by up to two orders of magnitude.

Fig. 7.8

Size of the computed Skolem functions with and without optimizations

Because QBFs are a special case of DQBFs, we can use HQS to compute Skolem functions for satisfied QBFs as well. In Fig. 7.9, we compare the sizes of the Skolem functions generated by HQS with those generated by the state-of-the-art QBF solver DepQBF 5.0 [22, 23] for a set of satisfiable QBF instances from the QBF Gallery 2013¹ and from partial equivalence checking [29] (with a single black box). Since HQS (and in particular its preprocessor) is not optimized for solving QBF instances, we abstain from a detailed comparison of the running times of HQS and DepQBF. DepQBF is often (but not always) faster than HQS. In a few cases, the generation of Skolem functions with DepQBF failed, because the necessary resolution proof became too large (we aborted DepQBF when the size of the dumped resolution proof exceeded 20 GB).

Fig. 7.9

Comparison of the sizes of Skolem functions from HQS and from DepQBF on QBF instances. The instances are ordered according to the size of DepQBF’s Skolem functions

Figure 7.9 shows the sizes of the Skolem functions computed by DepQBF and by HQS (with interpolation and ABC). To enable a fair comparison, we also applied ABC with the same commands to the Skolem functions generated using DepQBF. We can observe that HQS’ Skolem functions are in most cases smaller (often significantly) than those obtained from DepQBF.

In summary, the experiments show that HQS is able to solve the DQBFs resulting from small to medium-sized circuits effectively. We can not only obtain a pure yes/no answer, but also Skolem functions for the satisfiable instances without significant overhead. On satisfiable QBF instances, the size of the Skolem functions computed by HQS is similar, in many cases smaller in comparison to Skolem functions computed by DepQBF.

As a side remark, the example provided in Sect. 3 can easily be solved with a recent DQBF solver within fractions of a second. Benchmarks dealing with the synthesis of multiple black boxes in sequential circuits currently do not exist, but would be interesting to have.

6 Conclusion and Open Challenges

This paper has shown that DQBF formulations allow to express the realizability of invariant properties for incomplete combinational and sequential circuits with an arbitrary number of black boxes in a natural way. First prototypic solvers allow not only to solve the resulting DQBFs for small to medium-sized circuits, but also to extract Skolem functions, which can serve as implementations of the missing parts.

Still, many challenges remain: The scalability of the solvers has to be improved and might be tuned towards specific applications. More powerful preprocessing techniques are necessary as well as improvements in the solver core. We hope that with the availability of solvers more applications of these techniques become feasible (distributed controller synthesis) or are newly discovered thereby inspiring further improvements of the solvers—just as it was for propositional SAT solving and is for QBF solving.