Boolean Matching Using SBDD

In logic verification and logic synthesis，Boolean matching is widely used to testify whether two given functions are logically equal by means of OBDD．In order to improve the effi-ciency of matching algorithm，we count the number of minterms connected with every single vari-able or variable composition．Treating these numbers as “signature” of variables，algorithm can distinguish variables from each other．Then，impossible orders of variables are pruned during matching and time is saved．For extracting signatures of variables，we put forward SBDD，a new kind of binary decision diagram containing less nodes than OBDD，thus accerlating the extraction of signature．Experiments show that our algorithm reduces execution time．