Journal of Software, Vol 7, No 6 (2012), 1358-1366, Jun 2012
doi:10.4304/jsw.7.6.1358-1366

Biddy — a Multi-platform Academic BDD Package

Robert Meolic

Abstract


Biddy is a BDD package under GPL, developed at the University of Maribor. It uses ROBDDs with comple­ment edges, as described in the paper K. S. Brace, R. L. Rudell, R. E. Bryant, Efficient Implementation of a BDD Package, 1990. Compared to other available BDD packages, Biddy's most distinguishing features are its specially de­signed C interface and an original implementation of auto­matic garbage collection. More generally, the Biddy project is not only concerned with the computer library, but also of­fers a demo application for the visualization of BDDs, called BDD Scout. The whole project is oriented towards a read­able and comprehensible source code in C, which can be compiled unchanged on different platforms, including GNU/Linux and MS Windows.


Keywords


Boolean algebra; binary decision diagram; symbolic manipulation of Boolean functions; formal meth­ods; free software

References


 

[1] S. N. Yanushkevich, D. M. Miller, V. P. Shmerko, R. S. Stankovic. Decision diagram techniques for micro- and nanoelectronic design handbook. CRC Press, 2006.

[2] C. Baier J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008.

[3] Q. Wei, T. Gu, "Symbolic Representation for Rough Set Attribute Reduction Using Ordered Binary Decision Diagrams", Journal of Software, Vol. 6, No. 6, 2011, pp. 977-984.

[4] D. E. Knuth. Art of Computer Programming, Volume 4, Fascicle 1: Bitwise Tricks & Techniques; Binary Decision Diagrams. Addison-Wesley Professional, 2009.

[5] R. E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation", IEEE Transactions on Computers, Vol. C-35, No. 8, 1986, pp. 677-691. Reprinted in M. Yoeli, Formal Verification of Hardware Design, IEEE Computer Society Press, 1990, pp. 253-267.

[6] Wikipedia: Binary decision diagram. On-line (21/10/2011). http://en.wikipedia.org/wiki/Binary_decision_diagram

[7] ABCD. On-line (21/10/2011). http://fmv.jku.at/abcd/

[8] BuDDy. On-line (21/10/2011). http://buddy.wiki.sourceforge.net/

[9] CAL. On-line (21/10/2011). http://embedded.eecs.berkeley.edu/Research/cal_bdd/

[10] CMU BDD. On-line (21/10/2011). http://www-2.cs.cmu.edu/~modelcheck/bdd.html

[11] CUDD. On-line (21/10/2011). http://vlsi.colorado.edu/~fabio/CUDD/

[12] JDD. On-line (21/10/2011). http://javaddlib.sourceforge.net/jdd/

[13] Biddy. On-line (21/10/2011). http://lms.uni-mb.si/biddy/

[14] K. S. Brace, R. L. Rudell, R. E. Bryant, "Efficient Implementation of a BDD Package", In: 27. ACM/IEEE Design Automation Conference (DAC'90), 1990, pp. 40-45.

[15] A. Časar, R. Meolic, "Predstavitev logičnih funkcij z minimalnimi urejenimi binarnimi odločitvenimi grafi", Elektrotehniški vestnik, Vol. 59, No. 5, 1992, pp. 299-307. In Slovene.

[16] A. Časar, R. Meolic, "Representation of Boolean functions with ROBDDs", 1993. Presented at IEEE Region 8 Student Paper Contest, Paris-Evry 1993. Published in: IEEE Student paper contest: regional contest winners 1990-1997, IEEE, 2000.

[17] EST. On-line (21/10/2011). http://lms.uni-mb.si/EST/

[18] S. Paumier, "Why academic software should be Open Source", INFOtheca: Journal of informatics and librarianship, Vol. X, No. 1-2, 2009, pp. 51-54.

[19] G. Janssen, "A Consumer Report on BDD Packages", In: 16th Symposium on Integrated Circuits and Systems Design, 2003, pp. 217.

[20] Free Software Foundation, Inc. On-line (21/10/2011). http://www.fsf.org/

[21] S. B. Akers, "Binary decision diagrams", IEEE Transactions on Computers, Vol. C-27, No. 6, 1978, pp. 509-516.
http://dx.doi.org/10.1109/TC.1978.1675141

[22] S. Minato, N. Ishiura, S. Yajima, "Shared Binary Decision Diagram with Attributed Edges for Efficient Boolean Function Manipulation", In: 27th ACM/IEEE Design Automation Conference (DAC'90), 1990, pp. 52-57.

[23] R. E. Bryant, "Binary Decision Diagrams and Beyond: Enabling Technologies for Formal Verification", In: IEEE/ACM International Conference on Computer-Aided Design (ICCAD '95), 1995, pp. 236-243.

[24] R. Drechsler, B. Becker. Binary decision diagrams: theory and implementation. Springer, 1998.

[25] C. Meinel, T. Theobald. Algorithms and Data Structures in VLSI-Design: OBDD – Foundations and Applications. Springer-Verlag, 1998.

[26] R. Ebendt, G. Fey, R. Drechsler. Advanced BDD optimization. Springer, 2005.

[27] S. Edwards, G. Swamy, "The VIS Engineering Manual", 1996. On-line (21/10/2011). http://vlsi.colorado.edu/~vis/prgDoc.html

[28] BDDTCL. On-line (21/10/2011). http://www2.parc.com/csl/members/kpartrid/

[29] BDD Visualizer. On-line (21/10/2011). http://www.cs.uc.edu/~weaversa/BDD_Visualizer.html

[30] JADE: Implementation and Visualization of a BDD Package in JAVA. On-line (21/10/2011). http://www.informatik.uni-bremen.de/agra/eng/jade.php

[31] Graphviz. On-line (21/10/2011). http://www.graphviz.org/

[32] A. Duşa, "Enhancing Quine-McCluskey", 2007. COMPASSS Working Paper WP 2007-49. http://www.compasss.org/pages/resources/wpfull.html

[33] A. Časar, Z. Brezočnik, T. Kapus, "Exploiting symbolic model checking for sensing stuck-at faults in digital circuits", Inf. MIDEM, Vol. 32, No. 3, 2002, pp. 171-180.


Full Text: PDF


Journal of Software (JSW, ISSN 1796-217X)

Copyright @ 2006-2013 by ACADEMY PUBLISHER – All rights reserved.