References

1

A. Aziz, S. Tasiran, and R. K. Brayton. BDD Variable Ordering for Interacting Finite State Machines. In Proc. of the Design Automation Conf., pages 283-288, San Diago, CA, June 1994.

2

R. K. Brayton et al. VIS: A System for Verification and Synthesis. Technical Report UCB/ERL M95, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, Dec. 1995.

3

E. M. Clarke, O. Grumberg, K. L. McMillan, and X. Zhao. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proc. 32nd Design Automat. Conf., pages 427-432, June 1995.

4

S. Edwards. The Ext System, 1995. http://www.eecs.berkeley.edu/~ sedwards/ext.

5

H. Fujii, G. Ootomo, and C. Hori. Interleaving based variable ordering methods for ordered binary decision diagrams. In Proc. Intl. Conf. on Computer-Aided Design, pages 38-41, Nov. 1993.

6

R. K. Ranjan, A. Aziz, B. Plessier, C. Pixley, and R. K. Brayton. Efficient Formal Design Verification: Data Structure + Algorithms. Technical Report UCB/ERL M94/100, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, Oct. 1994.

7

E. M. Sentovich, K. J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P. R. Stephan, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. SIS: A System for Sequential Circuit Synthesis. Technical Report UCB/ERL M92/41, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, May 1992.

8

The VIS Group. VIS: Verification Interacting with Synthesis, 1995. http://www-cad.eecs.berkeley.edu/Respep/Research/vis .