Computational complexity is concerned with the complexity of solving
problems and computing functions and not with the complexity of verifying
circuit designs.
The importance of formal circuit verification is evident.
Therefore, a framework of a complexity theory for formal circuit
verification with binary decision diagrams is developed.
This theory is based on read-once projections.
For many problems it is determined whether and how they are related with
respect to read-once projections.
It is proved that multiplication can be reduced to squaring but
squaring is not a read-once projection of multiplication.
This perhaps surprising result is discussed.
For most of the common binary decision diagram models of polynomial size
complete problems with respect to read-once projections are described.
But for the class of functions with polynomial-size free binary decision
diagrams (read-once branching programs) no complete problem with respect
to read-once projection exists.