Combinational Logic Verification:Binary Decision Diagrams

• [Bryant 84] [Madre et. al. 88]

  • Ordering of variables left to user.

• Ordering Algorithm [Friedman, et al 87]

  • O((N^2)*(3^n)) algorithm, not useful for verification.

• Improved Significantly by [Malik, et al 88] and since by [Rudell, et. al. 89].

  • Take advantage of canonical form

Previous slide

Next slide

Back to first slide

View graphic version