Abstract
This paper describes a new method that is useful in combinational equivalence checking with very challenging industrial designs. The method does not build a miter; instead it builds BDDs of reference and implementation circuits independently – so that each BDD can have its best order while building the BDD – then compares the two BDDs directly without transforming one variable order to the other. In the comparison, checking containment of two BDDs is necessary to handle don’t cares efficiently. Even though there are polynomial algorithms for checking equality of two BDDs, those algorithms are not extendible to containment checking. Thus we also present an efficient algorithm, of polynomial complexity, to check both equality and containment of two BDDs with different variable orders. Our non-miter-based method was able to verify many hard industrial designs previously infeasible with existing miter-based state-of-the-art techniques. Experimental results show that the non-miter-based method is very efficient for designs that are especially difficult to check due to dissimilarities and don’t cares. The current work does not suggest an alternative that replaces conventional equivalence checking algorithms, but rather an approach that augments their capability for designs that are very hard to check.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Anastasakis, D., Damiano, R., Ma, H.T., Stanion, T.: A practical and efficient method for compare-point matching. In: Proceedings of the Design Automation Conference, New Orleans, LA, June 2002, pp. 305–310 (2002)
Berman, C.L., Trevillyan, L.H.: Functional comparison of logic designs for VLSI circuits. In: Proceedings of the International Conference on Computer-Aided Design, Santa Clara, CA, November 1989, pp. 456–459 (1989)
Bern, J., Meinel, C., Slobodova, A.: Global rebuilding of obdd’s avoiding memory requirement maxima. IEEE Transactions on CAD 15(1), 131–134 (1996)
Blum, M., Chandra, A., Wegman, M.: Equivalence of free boolean graphs can be decided probabilistically in polynomial time. Information Processing Letters 10(2), 80–82 (1980)
Brand, D.: Verification of large synthesized designs. In: Proceedings of the International Conference on Computer-Aided Design, Santa Clara, CA, November 1993, pp. 534–537 (1993)
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)
Cabodi, G., Quer, S., Meinel, C., Sack, H., Slobodova, A., Stangier, C.: Binary decision diagrams and the multiple variable order problem. In: International Workshop on Logic Synthesis, Lake Tahoe, CA (May 1998)
Fortune, S., Hopcroft, J., Schmidt, E.: The complexity of equivalence and containment for free single variable program schemes. In: Ausiello, G., Böhm, C. (eds.) ICALP 1978. LNCS, vol. 62, pp. 227–240. Springer, Heidelberg (1978)
Fujii, H., Ootomo, G., Hori, C.: Interleaving based variable ordering methods for ordered binary decision diagrams. In: Proceedings of the International Conference on Computer-Aided Design, Santa Clara, CA, November 1993, pp. 38–41 (1993)
Kuehlmann, A., Krohm, F.: Equivalence checking using cuts and heaps. In: Proceedings of the Design Automation Conference, Anaheim, CA, June 1997, pp. 263–268 (1997)
Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property checking. IEEE Transactions on CAD 21(12), 1377–1394 (2002)
Kwak, H.H., Moon, I.-H., Kukula, J., Shiple, T.: Combinational equivalence checking through function transformation. In: Proceedings of the International Conference on Computer-Aided Design, San Jose, CA (November 2002)
Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on CAD 48(5), 506–521 (1999)
Matsunaga, Y.: An efficient equivalence checker for combinational circuits. In: Proceedings of the Design Automation Conference, June 1996, pp. 629–634 (1996)
Mohnke, J., Malik, S.: Permutation and phase independent boolean comparison. In: Proceedings of the European Conference on Design Automation, Paris, France, February 1993, pp. 86–92 (1993)
Moon, I.-H., Kwak, H.H., Kukula, J., Shiple, T., Pixley, C.: Simplifying circuits for formal verification using parametric representation. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 52–68. Springer, Heidelberg (2002)
Moondanos, J., Seger, C.-J.H., Hanna, Z., Kaiss, D.: Clever: Divide and conquer combinational logic equivalence verification with false negative elimination. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 131–143. Springer, Heidelberg (2001)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the Design Automation Conference, June 2001, pp. 530–535 (2001)
Park, J., Burns, M., Pixley, C., Cho, H.: An efficient logic checker for industrial circuits. Journal of Electronic Testing 16(1-2), 91–106 (2000)
Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of the International Conference on Computer-Aided Design, Santa Clara, CA, November 1993, pp. 42–47 (1993)
Scholl, C., Becker, B., Brogle, A.: Multiple variable order problem for binary decision diagrams: Theory and practical application. In: Proceedings of the Asia and South Pacific Design Automation Conference, February 2001, pp. 85–90 (2001)
Stanion, T.: Circuit synthesis verification method and apparatus. U.S. Patent 6,056,784 (May 2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Moon, IH., Pixley, C. (2004). Non-miter-based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders. In: Hu, A.J., Martin, A.K. (eds) Formal Methods in Computer-Aided Design. FMCAD 2004. Lecture Notes in Computer Science, vol 3312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30494-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-30494-4_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23738-9
Online ISBN: 978-3-540-30494-4
eBook Packages: Springer Book Archive