Detection of symmetry of Boolean functions represented by ROBDDs

Addresses the problem of the detection of symmetries of Boolean functions. To know these symmetries may be important in several stages of logic design, e.g. in logic optimization, in logic synthesis, and in technology mapping. Reduced ordered binary decision diagrams (ROBDDs) play an important role in these tools. Using this representation form for Boolean functions there is a simple symmetry test by checking if certain cofactor functions are equivalent, i.e. if their ROBDD representations are the same. Unfortunately, this procedure may be very time and storage consuming because of the necessary cofactor computations. The approach presented in this paper uses preprocessing methods to find as many asymmetric pairs of variables as possible to avoid cofactor computations at the end. For that, special properties of the ROBDD structure as well as properties of Boolean functions are used. Experimental results on a large number of benchmarks show that this is a very efficient approach.