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 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^4. We have successfully verified 64-bit multipliers of several type in 3-6 hours with 40 Mbyte of memory on SPARCstation10/51. This result outperforms previous BDD-based approaches for verifying multipliers.