Polynomial Circuit Verification using BDDs
Rolf Drechsler · 2021 5th International Conference on Electrical, Electronics, Communication, Computer Technologies and Optimization Techniques (ICEECCOT) · 2021
Verification is one of the central tasks during circuit design. While most of the approaches have exponential worst-case behavior, in the following, techniques are discussed for proving polynomial circuit verification based on Binary Decision Diagrams (BDDs). It is shown that for circuits with specific structural properties, like e.g. tree-like circuits, and circuits based on multiplexers derived from BDDs complete formal verification can be carried out in Polynomial Time and Space (PTaS).