Skip to Main content Skip to Navigation

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 metadata
Contributor : Joan Thibault Connect in order to contact the contributor
Submitted on : Thursday, March 19, 2020 - 2:18:52 PM
Last modification on : Wednesday, November 3, 2021 - 8:09:44 AM
Long-term archiving on: : Saturday, June 20, 2020 - 2:35:46 PM




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


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



Les métriques sont temporairement indisponibles