{'fraction_non_alphanumeric': 0.02954808806488992, 'fraction_numerical': 0.006228273464658169, 'mean_word_length': 4.254566210045662, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
PolyAdd: Polynomial Formal Verification of Adder Circuits

Only by formal verification approaches functional correctness can be ensured. While for many circuits fast verification is possible, in other cases the approaches fail. In general no efficient algorithms can be given, since the underlying verification problem is NP-complete. In this paper we prove that for different types of adder circuits polynomial verification can be ensured based on BDDs. While it is known that the output functions for addition are polynomially bounded, we show in the following that the entire construction process can be carried out in polynomial time. This is shown for the simple Carry Ripple Adder, but also for fast adders like the Conditional Sum Adder and the Carry Look Ahead Adder. Properties about the adder function are proven and the core principle of polynomial verification is described that can also be extended to other classes of functions and circuit realizations.


Introduction
Ensuring the functional correctness of circuits and systems is one of the major challenges in today's circuit and system design. While simulation and emulation approaches reach their limits due to the complexity of the system under verification according to Moore's Law, only formal proof techniques can ensure correctness according to the specification (see e.g. [7,8]). In these approaches proof engines, like BDD, SAT or SMT, are applied.
In practice these techniques work often well and can handle circuits of several million gates. But it might also happen that the proof fails due to run time or memory constraints. One of the major difficulties is that this can hardly be predicted resulting in non-robust behavior of the tools. For this, a deeper understanding is required which circuits can be handled efficiently and for which ones the formal approach will fail.
In the context of the highly relevant class of arithmetic circuits early studies on BDDs have shown that they are not well-suited to verify multipliers [5], but using dedicated data structures, like *BMDs [6] it was possible to represent the output functions of a multiplier polynomially. In [11] it has been shown that not only the outputs can be represented, but for a specific type of Wallace tree multiplier the complete verification can be carried out polynomially.
In this paper, we consider circuits for addition of two binary numbers. While it is well known that the BDD size for the adder function is only linear in the bit size [4], we show that the complete construction process of the BDD is also bounded polynomially. This is shown for three different adder architectures, namely the Carry Ripple Adder (CRA), the Conditional Sum Adder (CSA) and the Carry Look Ahead Adder. Theoretical bounds on the BDD sizes are proven and it is shown that the complete symbolic simulation starting from the inputs to the outputs of the circuit can by carried out polynomially. Furthermore, for specific functions upper bounds on the BDD size are proven.
The paper is structured as follows: In Section 2 notations and definitions are reviewed to make the paper selfcontained. The adder function and BDDs are introduced. For the three adders the circuit realization is reviewed in Section 3. in Section 4 for the three adder architectures it is proven that formal verification can be done efficiently. Finally, the results are summarized and open problems are addressed.

Adder Function
Let a, b and s be three binary numbers of n bits, where s is the sum of a, b and an incoming carry bit c −1 . The relation between the sum s and the operands a and b can be described by the following two equations: The variable c i is called the i-the carry bit. The core cells of many adder architectures are the Half Adder (HA) and Full Adder (FA) cells realizing a 1-bit addition without or with carry input, respectively.
The function table of the HA is shown in following table It is easy to see that the function ha 1 can be realized by and AND-gate, while ha 0 is described by an ⊕-gate, i.e.: Analogously it follows for the FA with inputs a i , b i and c i−1 :

Binary Decision Diagrams
Reduced ordered Binary Decision Diagrams (BDDs) [4,9] are Directed Acyclic Graphs (DAGs) where a Shannon decomposition is carried out in each node. Example 1. The BDD for the full adder is shown in Figure  1.
An important property of BDDs is that the synthesis operations, like AND, OR or composition, can be carried out in polynomial time and space. This can be described by the operator if-then-else (ite) [4, 3] 1 . A sketch of the algorithm is as follows, where Rh Rl denote the high-and low-successors, respectively, and e.g. F1i is the cofactor to 1 with respect to variable i: The ite-operator has a polynomial worst case behavior, i.e. for graphs F , G and H the result is bound by O(|F |·|G|· |H|). This bound holds under the assumption of an optimal hashing in O(1). But also in the case of a worst case behavior of the hashing function, ite remains polynomial (see [10]).

Symbolic Simulation
To build the BDDs for the output signals of a circuit, the circuit is traversed in a topological order starting from the inputs. For the inputs signals the corresponding BDDs are initially generated. Then, for each gate in the circuit the corresponding synthesis operation based on ite is carried out. This process is called symbolic simulation in the following.
Example 2. The symbolic simulation for a circuit consisting of a single AND gate is shown in Figure 2.

Circuit Realization
In this section different realizations for adder circuits are briefly reviewed. Only the basic principles are reviewed as far as it is needed for making the paper self-contained. For more details see [2].

Carry Ripple Adder
The Carry Ripple Adder (CRA) simply consists of a sequence on n full adders. The cells are connected via the carry chain (see Figure 3).
The CRA is very area efficient, since it only requires a linear number of gates. But the CRA is also very slow, since the delay -measured in the number of gates that has to be traversed -is also linear in the number of inputs.

Conditional Sum Adder
The Conditional Sum Adder (CSA) can be recursively described. While the lower n/2 bits are computed by a CSA of bit-width n/2, for the higher n/2 bits the result is computed by two CSAs in parallel, where one assumes an incoming carry, while the other does not. Thus, the adder makes use of the fact that the higher bits only depend on the incoming carry from the lower half. Both results are precomputed and the correct result is selected by a multiplexer  Figure 4. For the 1-bit adders, simply full adders can be used.
The CSA is a fast adder, i.e. it has a depth of O(log(n)). The circuit has a gate count of O(n · log(n)).

Carry Look Ahead Adder
The Carry Look Ahead Adder (CLA) makes use of a fast prefix computation in a block P n (see Figure 5). From Equation (2) it is obvious that it is sufficient to compute the carry bits c i for all i. This can be done based on parallel prefex computation of the generation and propagation properties for addition. These are described by function g and p, respectively: This means that either a carry bit is generated in the upper part or a carry is generated in the lower part and is propagated through the higher part. Thus, the carry bits can be computed as (0 ≤ i < n): The CLA has a logarithmic depth and a size linear in the number of input variables.

Polynomial Verification
It is well known that the size of BDDs for the adder function is dependent on the variable ordering. It has also been proven that the BDD size is linearly bounded (see Section 4.4 in [12]), where exact estimates are given for BDD sizes. There, addition without the incoming carry bit has been considered. The results can be extended to also consider the incoming carry bit as it is required for all adder circuits in the following. 2. The carry bit c i of an adder has the BDD size bounded by 3i + 6.
Proof. We use the interleaved variable ordering from the least to the most significant bits. For the sum bits the results from Lemma 4.4.2 in [12] can be generalized, where an upper bound of 3i+5 has been proven for the adder function without an incoming carry bit. For the additional carry bit two more nodes are required, i.e. one for the carry bit itself and one for the a 0 variable.
The same argument holds for the carry bit, but here on the lowest level one node is saved, since in case of generation by a i and the incoming carry, b i does not have to be tested any more (see Figure 6 for the case of 4 variables).
It is important to notice that these results were always related to the representation size of the output functions, but not for the entire construction process. Remark 1. In the following, detailed bounds are not provided, since the goal of this paper is to show that the construction process is polynomial.
Thus, it is sufficient to show that each individual step can be carried out in polynomial time and space. We make use of the following observation: Remark 2. If for each internal signal the size of the BDD representation and the number of gates in the circuit is polynomially bounded in the number of inputs n, the whole circuit can be formally verified in polynomial time due to the polynomially bounded synthesis operations on BDDs.
This method can be applied to general circuits, but is used for adders only in the following. For the adder circuits from Section 3 the upper bounds hold, that each circuit only has a number of gates polynmial in the numer of inputs n.

Carry Ripple Adder
For the CRA it is very simple to see that the complete construction is polynomially bounded. For the HA of the least significant bit and all FAs the BDD can be locally constructed and has only a constant size. Due to the structure of the CRA each carry output of a cell is connected to the carry input of the next cell. The substitution of the input variable can be carried out by the compose algorithm based on ite and has a polynomial worst-case complexity. Furthermore, according to Theorem 1 the size of the BDD for the carry signal for all i is always linear. Thus, the whole construction process is polynomially bounded, since the composition only has to be carried out n times.
Theorem 2. The BDD for the CRA can be constructed polynomially.

Conditional Sum Adder
The n bit CSA consists of three CSAs of bit-size n/2 and a multiplexer stage. From Theorem 1 it follows that each of the connecting signals shown in Figure 4 can be represented by a BDD of linear size. Only the carry inputs have to be set to 0 and 1, respectively. The only operation that has to be carried out is the one corresponding to the MUX unit. But this can be described by ite and is polynomially bounded. Thus, we obtain: Theorem 3. The BDD for the CSA can be constructed polynomially.
Remark 3. The results of Theorems 2 and 3 can easily be generalized to further adder types that are based on full adders connected together using MUX cells, like e.g. the Carry Select Adder in [1] with a runtime of O( √ n).

Carry Look Ahead Adder
In the CLA the sum bits are computed by determining the carry bits first and finally EXOR-ing them with the corresponding a i and b i inputs according to Equation (2). Thus, the core circuit computes the carry bits starting based on the property of generation and propagation, i.e. functions p and g. The union of propagation intervals is based on Boolean AND-operations, i.e. larger interval only propagates a carry bit, if the left and the right part of the interval do so. For the generation part it holds that either the left part (using the higher bits) already propagates or the lower part generates, while the higher part propagates. In both cases, the structure consists of AND-and OR-operations only and it can be seen that the whole structure can be represented by BDDs of polynomial size. More formally, this can be proven as follows: 2. Function g j,i has the BDD size bounded by 6(j −i)−6 (j > i).
Proof. For function p j,i it holds: The BDD for the EXOR of two variables has three nodes.
Since each variable only appears once, the corresponding BDDs can simply be connected (see Figure 7 for the case of 4 variables).
Since the BDD is a cannonical representation, in g j,i = g j,k+1 + (g k,i p j,k+1 ) the choice of k does not influence the BDD size and we choose k = j − 1 resulting in g j,i = g j,j + (g j−1,i p j,j ).
For each pair of variables a l , b l at most 6 nodes can be generated resulting from all combinations of the EXOR and the AND (see Figure 8 for the case of 4 variables). For the top and bottom variables even some more nodes are saved, i.e. two at the top level and one at the 2nd one, and accordingly at the bottom. The exact estimate is not considered (see Remark 1), since a polynomial upper bound case is sufficient.
Based on this observation, the whole BDD for the CLA can be computed based on ite.

Conclusion
In this paper it has been proven for three different adder architectures that the complete formal verification process can be carried out polynomially. It was proven that the underlying BDDs remain polynomial in the whole construction process. This was ensured by proving upper bounds on the BDD sizes for each internal signal. While the BDD sizes for the outputs of the adder functions were known to be polynomially bounded, this is the first time that for efficient adder circuits of logarithmic run time a polynomial proof process could be ensured.
It is focus of future work to identify further classes of circuits and functions that can be polynomially verified using BDDs. Furthermore, alternative proof engines on the Boolean level, like SAT or O(K)FDDs, can be considered. Also extension to the word-level, like SMT or WLDDs, will be studied.