engleski

BDD complexity analysis of multiplier circuits

The equivalence of Boolean functions is an important issue in hardware design. In order to check the equivalence of two combinatorial circuits SAT solvers and BDD based algorithms are used. For complex hardware designs efficient BDD manipulation algorithms must be employed. There is a number of industrial combinatorial circuitry for which BDD representation explodes exponentially in the number of inputs. An example of such a circuitry is multiplier that is known to have no efficient BDD representation regardless of the employed variable ordering. In this paper we analyze some important properties of the BDD representation of multipliers, as well as the complexity of the involved computations

formal verification; symbolic model checking; BDDs; multiplier complexity

nije evidentirano