|
|
|---|
|
|
|
|---|
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.