De plus en plus, le problème de la vérification automatique des circuits électroniques se pose. Pour éviter qu'un bogue similaire à celui qu'a connu le Pentium ne survienne à nouveau, les industriels ont besoin de méthodes automatiques de preuve de correction de leurs circuits.
Les multiplicateurs, circuits chargés de calculer le produit de deux nombres entiers encodés en binaire, apparaissent fréquemment dans des circuits plus complexes. Il en existe de nombreux types, suivant le codage des nombres utilisé, les optimisations effectuées...
Malheureusement, les méthodes classiques de vérification automatique de circuits électroniques, comme les célèbres Binary Decision Diagrams (BDDs) inventés en 1986 par Bryant, sont très inefficaces sur les multiplicateurs. L'approche la plus prometteuse à ce jour semble être l'utilisation des Multiplicative Binary Moment Diagrams (*BMDs), conçus par ce même Bryant en 1995. L'approche de haut niveau proposée initialement nécessitait des informations sur la structure du circuit, ce qui n'est plus nécessaire si on construit les *BMDs par une méthode de balayage à rebours du circuit.