Publication: Using Extended Logical Primitives for Efficient BDD Building
Loading...
Date
2020
Editor
Director
Advisor
Coordinator
Commentator
Reviewer
Illustrator
Access rights
info:eu-repo/semantics/openAccess
Journal Title
Journal ISSN
Volume Title
Publisher
MDPI
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.
Description
The registered version of this article, first published in “Mathematics, 8, 2020", is available online at the publisher's website: MDPI, https://doi.org/10.3390/math8081253
La versión registrada de este artículo, publicado por primera vez en “Mathematics, 8, 2020", está disponible en línea en el sitio web del editor: MDPI, https://doi.org/10.3390/math8081253
UNESCO Categories
Keywords
binary decision diagrams, software product lines, circuit testing, configurable systems
Citation
Fernandez-Amoros, D., Bra, S., Aranda-Escolástico, E., & Heradio, R. (2020). Using Extended Logical Primitives for Efficient BDD Building. Mathematics, 8(8), 1253. https://doi.org/10.3390/math8081253
Center
E.T.S. de Ingeniería Informática
Department
Ingeniería de Software y Sistemas Informáticos