  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.
