An verified algorithm for converting aigs into ubdds.

The

The algorithm uses two methods to simplify an input AIG using BDDs of limited size; it repeatedly applies these methods while varying the BDD size limit. One method is similar to dynamic weakening in that it replaces oversized BDDs by a conservative approximation; the other method introduces fresh variables to represent oversized BDDs.

While we have not documented the algorithm with xdoc, a description of its operation and verification can be found in:

Sol Swords and Warren A. Hunt, Jr. A Mechanically Verified AIG to BDD Conversion Algorithm. In ITP 2010. Springer LNCS 6172, pages 435-449.

Slides from the ITP presentation are also available.