Evaluation and improvement of Boolean comparison method based on binary decision diagrams

R.E. Bryant proposed a method to handle logic expressions (IEEE Trans. Comp., vol.25, no.8, p.667-91, 1986) which is based on binary decision diagrams (BDD) with restriction; variable ordering ix fixed throughout a diagram. The method is more efficient than other methods proposed so far and depends heavily on variable ordering. A simple but powerful algorithm for variable ordering is developed. The algorithm tries to find a variable ordering which minimizes the number of crosspoints of nets when the circuit diagram is drawn. This is applied to the Boolean comparison of ISCAS benchmark circuits for test pattern generation. The results show that binary decision diagrams (BDD) with the proposed ordering method can verify almost all benchmark circuits in less than several central processor unit (CPU) minutes, which is one hundred times (or more) faster than times reported in the literature. Some techniques for circuit evaluation ordering are also mentioned.>