next up previous
Next: Efficient Identification of Non-Robustly Up: Formal Verification Previous: Dynamic Variable Reordering in

Timed Binary Decision Diagrams

Efficient representation and manipulation of the circuit behavior including both temporal and logical information is an important issue of design and test for high performance VLSI systems. OBDDs as a data structure for symbolic Boolean representation and manipulation have been successful in solving many difficult problems. The paper [22] presents an extension to OBDDs with timing information, called Timed Binary Decision Diagrams(TBDDs), which are also canonical and allow the symbolic manipulation of Boolean functions with timing information. A TBDD software package is implemented based on the existing CMU BDD package. Experimental results demonstrate the efficiency of the TBDDs in representing circuits with both functional and timing information.



Robert K. Brayton
Sat Mar 1 15:01:03 PST 1997