Abstract
In this paper, we present CacBDD, a new efficient BDD (Binary Decision Diagrams) package. It implements a dynamic cache management algorithm, which takes account of the hit-rate of computed table and available memory. Experiments on the BDD benchmarks of both combinational circuits and model checking show that CacBDD is more efficient compared with the state-of-the-art BDD package CUDD.
Chapter PDF
Similar content being viewed by others
References
Bryant, R.E.: GraphBased Algorithms for Boolean Function Manipulation. IEEE Trans. Computers, 677–691 (1986)
Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient Implementation of a BDD Package. In: Proc. 27th DAC 1990, pp. 40–45 (1990)
Somenzi, F.: CUDD: CU Decision Diagram Package Release, http://vlsi.colorado.edu/~fabioi/
Long, D.E.: The Design of a Cache-Friendly BDD Library. In: International Conference on Computer-Aided Design (ICCAD 1998), pp. 639–645 (1998)
Janssen, G.: Design of a Pointerless BDD Package. In: Workshop Handouts, 10th IWLS, pp. 310–315 (2001)
Lv, G., Su, K., Chen, Q., Chen, Y., Feng, Y.: A Succinct and Efficient Implementation of a 232 BDD Package. In: The Sixth International Symposium on Theoretical Aspects of Software Engineering (TASE 2012), Beijing, China (2012)
Janssen, G.: A Consumer Report on BDD Packages. In: Proceedings of the 16th Symposium on Integrated Circuits and Systems Design (SBCCI 2003), Sao Paulo, Brazil (2003)
The BDD benchmark, http://www.cs.cmu.edu/~bwolen/software/
Somenzi, F.: Efficientmanipulation of decision diagrams. International Journal on Software Tools for Technology Transfer 3, 17–181 (2001)
Yang, B., Bryant, R.E., O’Hallaron, D.R., Biere, A., Coudert, O., Janssen, G., Ranjan, R.K., Somenzi, F.: A performance study of BDD-based model checking. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 255–289. Springer, Heidelberg (1998)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Pnueli, A., Sa’ar, Y., Zuck, L.D.: jtlv: A Framework for Developing Verification Algorithms. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 171–174. Springer, Heidelberg (2010)
Rudell, R.: Dynamic Variable Reordering for Ordered Binary Diagrams. In: Proc. ICCAD, pp. 139–144 (1993)
Armin Biere: ABCD, http://fmv.jku.at/abcd/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lv, G., Su, K., Xu, Y. (2013). CacBDD: A BDD Package with Dynamic Cache Management. In: Sharygina, N., Veith, H. (eds) Computer Aided Verification. CAV 2013. Lecture Notes in Computer Science, vol 8044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-39799-8_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39798-1
Online ISBN: 978-3-642-39799-8
eBook Packages: Computer ScienceComputer Science (R0)