Functional simulation using binary decision diagrams

In many verification techniques, fast functional evaluation of a Boolean network is needed. We investigate the idea of using binary decision diagrams (BDDs) for functional simulation. The area-time trade-off that results from different minimization techniques of the BDD is discussed. We propose new minimization methods based on dynamic reordering that allow smaller representations with (nearly) no runtime penalty.