Publikation
Polynomial-Time Formal Verification of Adder Circuits for Multiple-Valued Logic
Philipp Niemann; Rolf Drechsler
In: 52nd International Symposium on Multiple-Valued Logic (ISMVL). IEEE International Symposium on Multiple-Valued Logic (ISMVL-2022), May 18-20, Dallas, USA, 2022.
Zusammenfassung
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.