Polynomial Circuit Verification using BDDs

TL;DR

This paper explores polynomial-time verification methods for certain classes of circuits using Binary Decision Diagrams, especially those with specific structural properties like tree-like structures and multiplexers.

Contribution

It demonstrates that for circuits with particular structures, formal verification can be achieved efficiently in polynomial time using BDDs.

Findings

Verification of tree-like circuits is polynomial in time and space.

Multiplexer-based circuits derived from BDDs can be verified efficiently.

Structural properties enable polynomial verification, unlike general exponential methods.

Abstract

Verification is one of the central tasks during circuit design. While most of the approaches have exponential worst-case behaviour, 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.