An efficient graph representation for arithmetic circuit verification

In this paper, we propose a new data structure called multiplicative power hybrid decision diagrams (*PHDDs) to provide a compact representation for f unctions that map Boolean vectors into integer or floating-point (FP) value s. The size of the graph to represent the IEEE FP encoding is linear with t he word size. The complexity of FP multiplication grows linearly with the w ord size. The complexity of FP addition grows exponentially with the size o f the exponent part, but linearly with the size of the mantissa part. We ap plied *PHDDs to verify integer multipliers and FP multipliers before the ro unding stage, based on a hierarchical verification approach. For integer mu ltipliers, our results are at least six times faster than binary moment dia grams. Previous attempts at verifying FP multipliers required manual interv ention, but we verified FP multipliers before the rounding stage automatica lly.