Computational complexity is concerned with the complexity of solving problems and computing functions and not with the complexity of verifying ircuit designs. The importance of formal verification is evident. Therefore, the framework of a complexity theory for formal 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. The result that circuits for squaring may be harder to verify than circuits for multiplication is derived and discussed. It is shown that the class of functions with polynomial-size free binary decision diagrams has no complete problem while for the corresponding classes for the other considered types of binary decisin diagrams complete problems are presented.
展开▼
