Polynomial-Time Formal Verification of Adder Circuits for Multiple-Valued Logic

Functional correctness of a circuit implementation can only be ensured by applying formal verification approaches. Although the underlying verification problem is NP-complete and, thus, no efficient verification is possible in general, for many circuits fast verification is indeed possible. There has been lots of work on formal verification of arithmetic circuits in the binary, two-valued logic domain. In this paper, we consider formal verification of adder circuits for multiple-valued logic and prove that for different types of adder circuits polynomial-time verification can be performed based on decision diagrams (DDs). While it is known that the output functions for addition are polynomially bounded, we show in the following that the entire construction process of the corresponding DD representation can be carried out in polynomial time. This is shown for the simple Ripple Carry Adder, but also for fast adders like the Conditional Sum Adder and the Carry Lookahead Adder.