TRANS: Efficient sequential verification of loop-free circuits

Bischoff et al [2] proposed a method for reducing sequential verification of loop-free circuits to combinational verification, by constructing and comparing the so called Timed (ternary) Binary Decision Diagrams (TBDDs). Ranjan et al [8] independently re-discovered a similar method. Here we propose a much more simple and efficient algorithm for constructing TBDDs. Furthermore, we prove the soundness of the algorithm, and describe very briefly a (restricted) new algorithm for generating sequential counter examples. These algorithms are implemented in Intel's sequential verification engine, TRANS.