Skip to Main content Skip to Navigation
Reports

Ordered Functional Decision Diagrams: A Functional Semantic For Binary Decision Diagrams

Joan Thibault 1 Khalil Ghorbal 1
1 HYCOMES - Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Several BDD variants were designed to exploit special features of Boolean functions to achieve better compression rates. Deciding a priori which variant to use is as hard as constructing the diagrams themselves and the conversion between variants comes in general with a prohibitive cost. This observation leads naturally to a growing interest into when and how one can combine existing variants to benefit from their respective sweet spots. In this paper, we introduce a novel framework, termed λDD (LDD), that revisits BDD from a purely functional point of view. The framework allows to classify the already existing variants, including the most recent ones like ChainDD and ESRBDD, as implementations of a special class of ordered models. We enumerate, in a principled way, all the models of this class and isolate its most expressive model. This new model, termed λDD-O-NUCX, is suitable for both dense and sparse Boolean functions, and, unlike ChainDD and ESRBDD, is invariant by negation. The canonicity of λDD-O-NUCX is formally verified using the Coq proof assistant. We furthermore provide experimental evidence corroborating our theoretical findings: more expressive λDD models achieve, indeed, better memory compression rates.
Complete list of metadatas

https://hal.inria.fr/hal-02512117
Contributor : Joan Thibault <>
Submitted on : Thursday, March 19, 2020 - 2:18:52 PM
Last modification on : Thursday, January 7, 2021 - 4:34:31 PM
Long-term archiving on: : Saturday, June 20, 2020 - 2:35:46 PM

Licence


Copyright

Identifiers

  • HAL Id : hal-02512117, version 1
  • ARXIV : 2003.09340

Citation

Joan Thibault, Khalil Ghorbal. Ordered Functional Decision Diagrams: A Functional Semantic For Binary Decision Diagrams. [Research Report] RR-9333, Inria. 2020. ⟨hal-02512117⟩

Share

Metrics

Record views

97

Files downloads

442