journal article
Open Access
Jul 31, 2020
Using Extended Logical Primitives for Efficient BDD Building
Abstract
Binary Decision Diagrams (BDDs) have been used to represent logic models in a variety of research contexts, such as software product lines, circuit testing, and plasma confinement, among others. Although BDDs have proven to be very useful, the main problem with this technique is that synthesizing BDDs can be a frustratingly slow or even unsuccessful process, due to its heuristic nature. We present an extension of propositional logic to tackle one recurring phenomenon in logic modeling, namely groups of variables related by an exclusive-or relationship, and also consider two other extensions: one in which at least n variables in a group are true and another one for in which at most n variables are true. We add XOR, atLeast-n and atMost-n primitives to logic formulas in order to reduce the size of the input and also present algorithms to efficiently incorporate these constructions into the building of BDDs. We prove, among other results, that the number of nodes created during the process for XOR groups is reduced from quadratic to linear for the affected clauses. the XOR primitive is tested against eight logical models, two from industry and six from Kconfig-based open-source projects. Results range from no negative effects in models without XOR relations to performance gains well into two orders of magnitude on models with an abundance of this kind of relationship.
Topics
No keywords indexed for this article. Browse by subject →
References
64
[1]
Bryant "Graph-Based Algorithms for Boolean Function Manipulation" IEEE Trans. Comput. (1986) 10.1109/tc.1986.1676819
[2]
The complexity of theorem-proving procedures
Stephen A. Cook
Proceedings of the third annual ACM symposium on T...
10.1145/800157.805047
[3]
Bollig "Improving the Variable Ordering of OBDDs is NP-Complete" IEEE Trans. Comput. (1996) 10.1109/12.537122
[4]
Kang, K., Cohen, S., Hess, J., Novak, W., and Peterson, S. (1990). Feature-Oriented Domain Analysis (FODA) Feasibility Study, Software Engineering Institute. Technical Report CMU/SEI-90-TR-21.
10.21236/ada235785
[5]
Mendonca, M., Wasowski, A., and Czarnecki, K. (2009, January 24–28). SAT-based Analysis of Feature Models is Easy. Proceedings of the 13th International Software Product Line Conference, San Francisco, CA, USA.
[6]
Heradio "Efficient Identification of Core and Dead Features in Variability Models" IEEE Access (2015) 10.1109/access.2015.2498764
[7]
Heradio, R., Fernandez-Amoros, D., Mayr-Dorn, C., and Egyed, A. (2019, January 25–31). Supporting the Statistical Analysis of Feature Models. Proceedings of the IEEE/ACM 41st International Conference on Software Engineering, Montreal, QC, Canada.
10.1109/icse.2019.00091
[8]
Zaid, L.A., Kleinermann, F., and De Troyer, O. (2009, January 9–12). Applying Semantic Web Technology to Feature Modeling. Proceedings of the 2009 ACM Symposium on Applied Computing, Honolulu, HI, USA.
10.1145/1529282.1529563
[9]
Bachmeyer, R.C., and Delugach, H.S. (2007, January 22–27). A conceptual graph approach to feature modeling. Proceedings of the International Conference on Conceptual Structures, Sheffield, UK.
[10]
Benavides, D., Trinidad, P., and Cortés, A.R. (2005, January 14–16). Using Constraint Programming to Reason on Feature Models. Proceedings of the 17th International Conference on Software Engineering and Knowledge Engineering, SEKE, Taipei, Taiwan.
[11]
Fernandez-Amoros, D., Heradio, R., and Cerrada, J.A. (2009, January 24–28). Inferring Information from Feature Diagrams to Product Line Economic Models. Proceedings of the 13th International Software Product Line Conference, San Francisco, CA, USA.
[12]
Hemakumar, A. (2008, January 8–12). Finding Contradictions in Feature Models. Proceedings of the Software Product Lines, 12th International Conference, SPLC, Limerick, Ireland.
[13]
Kastner, C., Apel, S., and Batory, D. (2007, January 10–14). A Case Study Implementing Features Using AspectJ. Proceedings of the 11th International Software Product Line Conference (SPLC 2007), Tokyo, Japan.
10.1109/spline.2007.12
[14]
Mannion, M. (2002, January 19–22). Using First-Order Logic for Product Line Model Validation. Proceedings of the Software Product Lines, Second International Conference, SPLC 2, San Diego, CA, USA.
10.1007/3-540-45652-x_11
[15]
Mendonça, M., Wasowski, A., Czarnecki, K., and Cowan, D.D. (2008, January 19–23). Efficient compilation techniques for large scale feature models. Proceedings of the Generative Programming and Component Engineering, 7th International Conference, GPCE, Nashville, TN, USA.
10.1145/1449913.1449918
[16]
Plazar, Q., Acher, M., Perrouin, G., Devroey, X., and Cordy, M. (2019, January 4–9). Uniform Sampling of SAT Solutions for Configurable Systems: Are We There Yet?. Proceedings of the Validation and Verification (ICST), 12th IEEE Conference Software Testing, San Francisco, CA, USA.
10.1109/icst.2019.00032
[17]
Bartlett "Choosing a heuristic for the "fault tree to binary decision diagram" conversion, using neural networks" IEEE Trans. Reliab. (2002) 10.1109/tr.2002.802892
[18]
Jung "A fast BDD algorithm for large coherent fault trees analysis" Reliab. Eng. Syst. Saf. (2004) 10.1016/j.ress.2003.10.009
[19]
Remenyte, R., and Andrews, J.D. (2006, January 20–22). A Simple Component Connection Approach for Fault Tree Conversion to Binary Decision Diagram. Proceedings of the The First International Conference on Availability, Reliability and Security, ARES 2006, the International Dependability Conference—Bridging Theory and Practice, Vienna, Austria.
10.1109/ares.2006.17
[20]
Deng "BDD algorithms based on modularization for fault tree analysis" Prog. Nucl. Energy (2015) 10.1016/j.pnucene.2015.06.019
[21]
Bitner, J.R., Jain, J., Abadir, M.S., Abraham, J.A., and Fussell, D.S. (1994, January 15–17). Efficient Algorithmic Circuit Verification Using Indexed BDDs. Proceedings of the Digest of Papers: FTCS/24, the Twenty-Fourth Annual International Symposium on Fault-Tolerant Computing, Austin, TX, USA.
[22]
"A BDD-based verification method for large synthesized circuits" Integration (1997)
[23]
Scholl "BDD minimization using symmetries" IEEE Trans. CAD Integr. Circuits Syst. (1999) 10.1109/43.743706
[24]
Drechsler "Fast exact minimization of BDD’s" IEEE Trans. CAD Integr. Circuits Syst. (2000) 10.1109/43.833206
[25]
Aloul, F.A., Markov, I.L., and Sakallah, K.A. (2002, January 4–7). Efficient Gate and Input Ordering for Circuit-to-BDD Conversion. Proceedings of the 11th IEEE/ACM International Workshop on Logic & Synthesis, IWLS 2002, New Orleans, LA, USA.
[26]
Fey, G., Shi, J., and Drechsler, R. (September, January 31). BDD Circuit Optimization for Path Delay Fault Testability. Proceedings of the Euromicro Symposium on Digital Systems Design (DSD 2004), Architectures, Methods and Tools, Rennes, France.
10.1109/dsd.2004.1333273
[27]
Ebendt "Combining ordered best-first search with branch and bound for exact BDD minimization" IEEE Trans. CAD Integr. Circuits Syst. (2005) 10.1109/tcad.2005.852053
[28]
Fey "Minimizing the number of paths in BDDs: Theory and algorithm" IEEE Trans. CAD Integr. Circuits Syst. (2006) 10.1109/tcad.2005.852662
[29]
Ebendt "Effect of improved lower bounds in dynamic BDD reordering" IEEE Trans. CAD Integr. Circuits Syst. (2006) 10.1109/tcad.2005.854632
[30]
Dinh, Q., Chen, D., and Wong, M.D.F. (2010, January 3–6). BDD-based circuit restructuring for reducing dynamic power. Proceedings of the 28th International Conference on Computer Design, ICCD 2010, Amsterdam, The Netherlands.
10.1109/iccd.2010.5647524
[31]
Ubar, R., Marenkov, M., Mironov, D., and Viies, V. (2014, January 16–18). Modeling sequential circuits with shared structurally synthesized BDDs. Proceedings of the 9th International Design and Test Symposium, IDT 2014, Algeries, Algeria.
10.1109/idt.2014.7038600
[32]
Rauchenecker, A., and Wille, R. (2017, January 19–21). An efficient physical design of fully-testable BDD-based circuits. Proceedings of the 20th IEEE International Symposium on Design and Diagnostics of Electronic Circuits & Systems, DDECS 2017, Dresden, Germany.
10.1109/ddecs.2017.7934560
[33]
Ubar, R., Jürimägi, L., Adekoya, A.O., and Jenihhin, M. (2019, January 28–30). True Path Tracing in Structurally Synthesized BDDs for Testability Analysis of Digital Circuits. Proceedings of the 22nd Euromicro Conference on Digital System Design, DSD 2019, Kallithea, Greece.
10.1109/dsd.2019.00077
[34]
Matsuo "Methods for Reducing Power and Area of BDD-based Optical Logic Circuits" IEICE Trans. (2019) 10.1587/transfun.e102.a.1751
[35]
Narodytska, N., and Walsh, T. (2007, January 6–12). Constraint and Variable Ordering Heuristics for Compiling Configuration Problems. Proceedings of the International Joint Conference on Artifical Intelligence, Hyderabad, India.
[36]
Trinidad, P., Benavides, D., Ruiz-Cortes, A., Segura, S., and Jimenez, A. (2008, January 8–12). FAMA Framework. Proceedings of the Software Product Line Conference, Limerick, Ireland.
10.1109/splc.2008.50
[37]
Mendonça, M. (2009). Efficient Reasoning Techniques for Large Scale Feature Models. [Ph.D. Thesis, University of Waterloo].
10.1145/1449913.1449918
[38]
Czarnecki, K., She, S., and Wasowski, A. (2008, January 8–12). Sample Spaces and Feature Models: There and Back Again. Proceedings of the 12th International Software Product Line Conference, Limerick, Ireland.
10.1109/splc.2008.49
[39]
Classen, A., Heymans, P., Schobbens, P., and Legay, A. (2011, January 21–28). Symbolic model checking of software product lines. Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Honolulu, HI, USA.
10.1145/1985793.1985838
[40]
Heradio "Improving the accuracy of COPLIMO to estimate the payoff of a software product line" Expert Syst. Appl. (2012) 10.1016/j.eswa.2012.01.109
[41]
Heradio "Exemplar driven development of software product lines" Expert Syst. Appl. (2012) 10.1016/j.eswa.2012.05.004
[42]
Beyer, D., and Stahlbauer, A. (2012, January 25–28). BDD-Based Software Model Checking with CPAchecker. Proceedings of the Mathematical and Engineering Methods in Computer Science, 8th International Doctoral Workshop, MEMICS 2012, Znojmo, Czech Republic. Revised Selected Papers.
[43]
Heradio "Speeding up Derivative Configuration from Product Platforms" Entropy (2014) 10.3390/e16063329
[44]
Apel, S., von Rhein, A., Wendler, P., Größlinger, A., and Beyer, D. (2013, January 18–26). Strategies for product-line verification: Case studies and experiments. Proceedings of the 35th International Conference on Software Engineering, ICSE ’13, San Francisco, CA, USA.
10.1109/icse.2013.6606594
[45]
Heradio "Augmenting measure sensitivity to detect essential, dispensable and highly incompatible features in mass customization" Eur. J. Oper. Res. (2016) 10.1016/j.ejor.2015.08.005
[46]
Aloul, F.A., Markov, I.L., and Sakallah, K.A. (2003, January 28–29). FORCE: A fast and easy-to-implement variable-ordering heuristic. Proceedings of the 13th ACM Great Lakes Symposium on VLSI 2003, Washington, DC, USA.
10.1145/764808.764839
[47]
Aloul "MINCE: A Static Global Variable-Ordering Heuristic for SAT Search and BDD Manipulation" J. UCS (2004)
[48]
Meinel, C., Somenzi, F., and Theobald, T. (1998, January 10–13). Function Decomposition and Synthesis Using Linear Sifting. Proceedings of the ASP-DAC ’98, Asia and South Pacific Design Automation Conference 1998, Pacifico Yokohama, Yokohama, Japan.
[49]
Rudell, R. (2003). Dynamic Variable Ordering for Ordered Binary Decision Diagrams. The Best of ICCAD: 20 Years of Excellence in Computer-Aided Design, Springer.
10.1007/978-1-4615-0292-0_5
[50]
Benavides "Automated analysis of feature models 20 years later: A literature review" Inf. Syst. (2010) 10.1016/j.is.2010.01.001
Showing 50 of 64 references
Metrics
10
Citations
64
References
Details
- Published
- Jul 31, 2020
- Vol/Issue
- 8(8)
- Pages
- 1253
- License
- View
Authors
Funding
Comunidad de Madrid
Award: RoboCity2030 S2013/MIT-2748
Ministerio de Ciencia, Innovación y Universidades
Award: DPI2016-77677-P
Cite This Article
David Fernandez-Amoros, Sergio Bra, Ernesto Aranda-Escolástico, et al. (2020). Using Extended Logical Primitives for Efficient BDD Building. Mathematics, 8(8), 1253. https://doi.org/10.3390/math8081253
Related
You May Also Like
Mitigating the Multicollinearity Problem and Its Machine Learning Approach: A Review
Jireh Yi-Le Chan, Steven Mun Hong Leow · 2022
463 citations
Numerical Solution of Fractional Differential Equations: A Survey and a Software Tutorial
Roberto Garrappa · 2018
418 citations
Survey on Synthetic Data Generation, Evaluation Methods and GANs
Alvaro Figueira, Bruno Vaz · 2022
344 citations
Roles and Research Trends of Artificial Intelligence in Mathematics Education: A Bibliometric Mapping Analysis and Systematic Review
Gwo-Jen Hwang, Yun-Fang Tu · 2021
271 citations
Auto-Encoders in Deep Learning—A Review with New Perspectives
Shuangshuang Chen, Wei Guo · 2023
265 citations