Skip to Main content Skip to Navigation
Book sections

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.
Document type :
Book sections
Complete list of metadata

Cited literature [31 references]  Display  Hide  Download
Contributor : David Novo Connect in order to contact the contributor
Submitted on : Monday, February 19, 2018 - 11:06:35 AM
Last modification on : Friday, August 5, 2022 - 3:02:14 PM
Long-term archiving on: : Monday, May 7, 2018 - 2:29:48 AM


Files produced by the author(s)




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⟩



Record views


Files downloads