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 metadatas

Cited literature [31 references]  Display  Hide  Download

https://hal-lirmm.ccsd.cnrs.fr/lirmm-01712044
Contributor : David Novo <>
Submitted on : Monday, February 19, 2018 - 11:06:35 AM
Last modification on : Wednesday, August 7, 2019 - 12:19:22 PM
Long-term archiving on: Monday, May 7, 2018 - 2:29:48 AM

File

book17-satclp.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

497

Files downloads

349