Keim, Martin; Drechsler, Rolf; Becker, Bernd; Martin, Michael; Molitor, Paul Polynomial formal verification of multipliers. (English) Zbl 1033.68075 Form. Methods Syst. Des. 22, No. 1, 39-58 (2003). Summary: Not long ago, completely automatical formal verification of multipliers was not feasible, even for small input word sizes. However, with Multiplicative Binary Moment Diagrams (\(\ast\)BMD), which is a new data structure for representing arithmetic functions over Boolean variables, methods were proposed by which verification of multipliers with input word sizes of up to 256 Bits is now feasible. Unfortunately, only experimental data has been provided for these verification methods until now. In this paper, we give a formal proof that logic verification with \(\ast\)BMDs is polynomially bounded in both, space and time, when applied to the class of Wallace-tree like multipliers. Using this knowledge online detection of design errors becomes feasible during a verification run. Cited in 1 Document MSC: 68Q65 Abstract data types; algebraic specification Keywords:equivalence checking; formal verification; integer multipliers; backward construction; multiplicative binary moment diagrams PDFBibTeX XMLCite \textit{M. Keim} et al., Form. Methods Syst. Des. 22, No. 1, 39--58 (2003; Zbl 1033.68075) Full Text: DOI