×

Polynomial formal verification of multipliers. (English) Zbl 1033.68075

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.

MSC:

68Q65 Abstract data types; algebraic specification
PDFBibTeX XMLCite
Full Text: DOI