Abstract
A major challenge in the area of hardware verification is to devise methods that can handle circuits of practical size. This paper intends to show how the applicability of combinational circuit verification tools based on binary decision diagrams (BDDs) can be greatly improved. The introduction of dynamic variable ordering techniques already makes these tools more robust; a designer no longer needs to worry about a good initial variable order. In addition, we present a novel approach combining BDDs with a technique that exploits structural similarities of the circuits under comparison. We explain how these similarities can be detected and put to effective use in the verification process. Benchmark results show that the proposed method significantly extends the range of circuits that can be verified using BDDs.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Ashar, P., Ghosh, A., Devadas, S.: Boolean Satisfiability and Equivalence Checking using General Binary Decision Diagrams. Proc. ICCD-91, pp. 259–264, 1991
Berkelaar, M.R.C.M., Theeuwen, J.F.M.: Logic Synthesis with Emphasis on Area-Power-Delay Trade-Off. Journal of Semicustom ICs, September 1991, pp. 37–42
Berman, C.L.: On Logic Comparison. Proc. DAC-81, pp. 854–861, 1981
Berman, C.L., Trevillyan, L.H.: Functional Comparison of Logic Designs for VLSI Circuits. Proc. ICCAD-89, pp. 456–459, 1989
Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient Implementation of a BDD package. Proc. DAC-90, pp. 40–45, 1990
Brand, D.: Verification of Large Synthesized Designs. Proc. ICCAD-93, pp. 534–537, 1993
Brglez, F., Fujiwara, H.: A Neutral Netlist of 10 Combinational Benchmark Circuits and a Target Translator in FORTRAN. Special session on the 1985 IEEE Int. Symposium on Circuits and Systems, 1985
Bryant, R.E.: Graph Based Algorithms for Boolean Function Representation. IEEE Transactions on Computers, vol. C-35 no. 8, pp. 677–691, August 1986
Burch, J.R.: Using BDDs to Verify Multipliers. Proc. DAC-91, pp. 408–412, 1991
Fujita, M., Fujisawa, H., Matsunaga, Y.: Variable Ordering Algorithms for Ordered Binary Decision Diagrams and Their Evaluation. IEEE Transactions on CAD, vol. 12 no. 1, pp. 6–12, January 1993
Jain, J., et al.: IBDDs: an Efficient Functional Representation for Digital Circuits. Proc. EDAC-92, pp. 440–446, 1992
Jeong, S.-W., et al.: Variable Ordering and Selection for FSM Traversal. Proc. ICCAD-91, pp. 476–479, 1991
Kropf, T.: Benchmark-Circuits for Hardware-Verification. February 1994
Kunz, W.: HANNIBAL: An Efficient Tool for Logic Verification Based on Recursive Learning. Proc. ICCAD-93, pp. 538–543, 1993
Mets, A.A.: Dynamic Variable Ordering for BDD Minimization. Student report Eindhoven University, Department of Electrical Engineering, January 1994
Rudell, R.: Dynamic Variable Ordering for Ordered Binary Decision Diagrams. Workshop Notes Int. Workshop on Logic Synthesis, 1993
Rudell, R.: Dynamic Variable Ordering for Ordered Binary Decision Diagrams. Proc. ICCAD-93, pp. 42–47, 1993
Tromp, G.J., van de Goor, A.J.: Logic Synthesis of 100-percent Testable Logic Networks. Proc. ICCD-91, pp. 428–431, 1991
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Eijk, C.A.J., Janssen, G.L.J.M. (1995). Exploiting structural similarities in a BDD-based verification method. In: Kumar, R., Kropf, T. (eds) Theorem Provers in Circuit Design. TPCD 1994. Lecture Notes in Computer Science, vol 901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59047-1_45
Download citation
DOI: https://doi.org/10.1007/3-540-59047-1_45
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59047-7
Online ISBN: 978-3-540-49177-4
eBook Packages: Springer Book Archive