Progressive Generation of Canonical Irredundant Sums of Products Using a SAT Solver - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier Access content directly
Book Sections Year : 2017

Progressive Generation of Canonical Irredundant Sums of Products Using a SAT Solver

Abstract

We present an algorithm that progressively generates canonical irredun-dant Sums Of Products (SOPs) for completely-and incompletely-specified Boolean functions using a satisfiability (SAT) solver. The progressive generation allows for real time monitoring and early termination, as well as for generation of partial SOPs for incremental applications. On the other hand, canonicity brings independence of the original representation and often yields smaller and more regular SOPs that lead to smaller circuits after algebraic factoring. Also, canonicity is key in applications such as constraint solving and random assignment generation, which traditionally rely on methods based on Binary Decision Diagram (BDD). However, in contrast with BDDs, our algorithm can relax canonicity to improve speed and scalability. In general, our method is more scalable for benchmarks with many structurally isomor-phic outputs. It also improves the quality of results up to 10%, in terms of the SOP size, compared to a state-of-the-art BDD-based method. Experiments with global circuit restructuring using SAT-based SOPs show that area-delay product can be improved up to 27%, compared to global restructuring using BDD-based SOPs.
Fichier principal
Vignette du fichier
book17-satclp.pdf (845.6 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

lirmm-01712044 , version 1 (19-02-2018)

Identifiers

Cite

Ana Petkovska, Alan Mishchenko, David Novo, Muhsen Owaida, Paolo Ienne. Progressive Generation of Canonical Irredundant Sums of Products Using a SAT Solver. André Inácio Reis; Rolf Drechsler. Advanced Logic Synthesis, Springer, pp.169-188, 2017, 978-3-319-67295-3. ⟨10.1007/978-3-319-67295-3_8⟩. ⟨lirmm-01712044⟩
349 View
290 Download

Altmetric

Share

Gmail Mastodon Facebook X LinkedIn More