Efficient construction of binary moment diagrams for verifying arithmetic circuits

BDD-based approaches cannot handle some arithmetic functions such as multiplication efficiently, while Binary Moment Diagrams proposed by Bryant and Chen (1994) provide compact representations for those functions. They reported a BMD-based polynomial-time algorithm for verifying multipliers. This approach requires high-level information such as specifications to subcomponents. This paper presents a new technique called backward construction which can construct BMDs directly from circuit descriptions without any high-level information. The experiments show that the computation time for verifying for n-bit multipliers is approximately n/sup 4/. We have successfully verified 64-bit multipliers of several type in 3-6 hours with 46 Mbyte of memory on SPARCstation 10/51. This result outperforms previous BDD-based approaches for verifying multipliers.