Canonical form based boolean matching and symmetry detection in logic synthesis and verification

Boolean matching algorithms have many applications in logic synthesis especially in technology mapping and combinational logic verification. Canonical form based Boolean matching has been studied by many researchers. However, none of the previous work has produced in an algorithm with reasonable space and time complexities for general Boolean matching problem. In contrast, this dissertation provides an efficient and compact canonical form for representing the set of all Boolean functions that are equivalent under permutation of input variables and complementation of input or output variables (i.e., NPN-equivalent Boolean functions). In particular, important properties of the proposed canonical form are investigated, and subsequently utilized to devise an effective algorithm for computing the proposed canonical form. The low average computational complexity of this algorithm allows it to be applied to large complex Boolean functions with no limitation on the number of input variables as opposed to previous approaches, which are not capable of handling functions with more than seven inputs. Key contributions of this thesis include the introduction of the complete set of generalized signatures of a Boolean function, development of efficient methods of recognizing variable symmetries, and presentation of a proficient algorithm for computing the canonical form of the class of NPN-equivalent Boolean functions based on the generalized signatures and variable symmetries.