BDD-based boolean functional synthesis

Dror Fried, Lucas M. Tabajara, Moshe Y. Vardi

نتاج البحث: فصل من :كتاب / تقرير / مؤتمرمنشور من مؤتمرمراجعة النظراء


Boolean functional synthesis is the process of automatically obtaining a constructive formalization from a declarative relation that is given as a Boolean formula. Recently, a framework was proposed for Boolean functional synthesis that is based on Craig Interpolation and in which Boolean functions are represented as And-Inverter Graphs (AIGs). In this work we adapt this framework to the setting of Binary Decision Diagrams (BDDs), a standard data structure for representation of Boolean functions. Our motivation in studying BDDs is their common usage in temporal synthesis, a fundamental technique for constructing control software/hardware from temporal specifications, in which Boolean synthesis is a basic step. Rather than using Craig Interpolation, our method relies on a technique called Self-Substitution, which can be easily implemented by using existing BDD operations. We also show that this yields a novel way to perform quantifier elimination for BDDs. In addition, we look at certain BDD structures called input-first, and propose a technique called TrimSubstitute, tailored specifically for such structures. Experiments on scalable benchmarks show that both Self- Substitution and TrimSubstitute scale well for benchmarks with good variable orders and significantly outperform current Boolean-synthesis techniques.

اللغة الأصليةالإنجليزيّة
عنوان منشور المضيفComputer Aided Verification - 28th International Conference, CAV 2016, Proceedings
المحررونSwarat Chaudhuri, Azadeh Farzan
ناشرSpringer Verlag
عدد الصفحات20
رقم المعيار الدولي للكتب (المطبوع)9783319415390
المعرِّفات الرقمية للأشياء
حالة النشرنُشِر - 2016
منشور خارجيًانعم
الحدث28th International Conference on Computer Aided Verification, CAV 2016 - Toronto, كندا
المدة: ١٧ يوليو ٢٠١٦٢٣ يوليو ٢٠١٦

سلسلة المنشورات

الاسمLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
مستوى الصوت9780
رقم المعيار الدولي للدوريات (المطبوع)0302-9743
رقم المعيار الدولي للدوريات (الإلكتروني)1611-3349


!!Conference28th International Conference on Computer Aided Verification, CAV 2016

ملاحظة ببليوغرافية

Publisher Copyright:
© Springer International Publishing Switzerland 2016.


أدرس بدقة موضوعات البحث “BDD-based boolean functional synthesis'. فهما يشكلان معًا بصمة فريدة.

قم بذكر هذا