research-article

Incremental learning approach and SAT model for Boolean matching with don't cares

Authors:

Kuo-Hua Wang,

Chung-Ming ChanAuthors Info & Claims

ICCAD '07: Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design

Pages 234 - 239

Published: 05 November 2007 Publication History

Get Access

Abstract

In this paper, we will propose an incremental learning approach to solve Boolean matching for incompletely specified functions. This approach can incrementally analyze current feasible partial mappings, detect and eliminate redundant manipulations in a proactive way. A new type of signature exploiting single variable symmetries is also given to reduce the searching space. Moreover, a SAT model of Boolean matching will be proposed to handle large Boolean functions. Through the utilization of these novel mechanisms, a drastic improvement on the performance of our Boolean matching algorithms are achieved. The experimental results demonstrate the effectiveness and efficiency of the proposed learning-based and SAT-based Boolean matching algorithms on many large benchmarking circuits.

References

[1]

J. Cong and Y. Hwang, "Boolean Matching for LUT-Based Logic Blocks with Application to Architecture Evaluation and Technology Mapping," IEEE Transactions on Computer-Aided Design, Vol. 20, No. 9, pp. 1077--1090, Sep. 2001.

Digital Library

Google Scholar

[2]

A. Mishchenko, S. Chatterjee, and R. Brayton, "Improvements to Technology Mapping for LUT-Based FPGAs," IEEE Transactions on Computer-Aided Design, Vol. 26, No. 2, pp. 240--253, Feb. 2007.

Digital Library

Google Scholar

[3]

F. Mailhot and G. D. Micheli, "Technology mapping using Boolean Matching and Don't Care Sets," in Proc. of the Conference on European Design Automation, pp. 212--216, 1990.

Digital Library

Google Scholar

[4]

L. Benini and G. D. Micheli, "A Survey of Boolean Matching Techniques for Library Binding," ACM Trans. Design Automation of Electronic Systems, Vol. 2, No. 3, pp. 193--226, July 1997.

Digital Library

Google Scholar

[5]

A. Abdollahi and M. Pedram, "A New Canonical Form for Fast Boolean Matching in Logic Synthesis and Verification," in Proc. of Design Automation Conference, pp. 379--384, June 2005.

Digital Library

Google Scholar

[6]

K. H. Wang and T. Hwang, "Boolean Matching for Incompletely Specified Functions," IEEE Transaction on Computer-Aided-Design of Integrated Circuits and Systems, Vol. 16., No. 2., pp. 160--168, Febraruary, 1997.

Digital Library

Google Scholar

[7]

J. P. Marques-Silva and K. A. Sakallah, "GRASP: A Search Algorithm for Propositional Satisfiability," IEEE Transactions on Computer-Aided Design, Vol. 48, No. 5, pp. 506--521, May 1999.

Digital Library

Google Scholar

[8]

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Chaff: Engineering an Efficient SAT Solver," in Proc. of Design Automation Conference, pp. 530--535, June 2001.

Digital Library

Google Scholar

[9]

J. P. Marques-Silva and K. A. Sakallah, "Boolean Satisfiability in Electronic Design Automation," in Proc. of Design Automation Conference, pp. 675--680, June 2000.

Digital Library

Google Scholar

[10]

A. Ling, D. Singh, and S. Brown, "FPGA Technology Mapping: A Study of Optimality," in Proc. of Design Automation Conference, pp. 427--432, 2005.

Digital Library

Google Scholar

[11]

S. Safarpour, A. Veneris, G. Baeckler, R. Yuan, "Efficient SAT-based Boolean Matching for FPGA Technology Mapping," in Proc. of Design Automation Conference, pp.466--471, July 2006.

Digital Library

Google Scholar

[12]

J. Cong and K. Minkovich, "Improved SAT-Based Boolean Matching using Implicants for LUT-based FPGAs," in Proc. of Int. Symp. on FPGAs, pp.139--147, Feb., 2007.

Digital Library

Google Scholar

[13]

J. Denzinger, M. Fuchs, C. Goller, and S. Schulz, "Learning from Previous Proof Experience: A Survey," AR-Report AR-99-4, TU München, 1999.

Google Scholar

[14]

K. H. Wang and J. H. Chen, "Symmetry Detection for Incompletely Specified Functions," in Proc. of Design Automation Conference, pp.434--437, June 2004.

Digital Library

Google Scholar

Cited By

View all

Lai CJiang JWang KScheffer LPhillips JHu A(2010)Boolean matching of function vectors with strengthened learningProceedings of the International Conference on Computer-Aided Design10.5555/2133429.2133555(596-601)Online publication date: 7-Nov-2010
https://dl.acm.org/doi/10.5555/2133429.2133555
Lai CJiang JWang KSapatnekar S(2010)BooMProceedings of the 47th Design Automation Conference10.1145/1837274.1837398(499-504)Online publication date: 13-Jun-2010
https://dl.acm.org/doi/10.1145/1837274.1837398
Wang KChan CLiu J(2009)Simulation and SAT-based Boolean matching for large Boolean networksProceedings of the 46th Annual Design Automation Conference10.1145/1629911.1630016(396-401)Online publication date: 26-Jul-2009
https://dl.acm.org/doi/10.1145/1629911.1630016
Show More Cited By

Recommendations

Stochastic local search for incremental SAT

The boolean satisfiability problem (SAT) is stated as follows: given a boolean formula in CNF, find a truth assignment that satisfies its clauses. In this paper, we present a general framework based on stochastic local search and the structure of the ...
Pseudo-Boolean Solving by incremental translation to SAT
FMCAD '11: Proceedings of the International Conference on Formal Methods in Computer-Aided Design

We revisit pseudo-Boolean Solving via compilation to SAT. We provide an algorithm for solving pseudo-Boolean problems through an incremental translation to SAT that works with any incremental SAT solver as a backend. Experimental evaluation shows that ...
Simulation and SAT-based Boolean matching for large Boolean networks
DAC '09: Proceedings of the 46th Annual Design Automation Conference

Boolean matching is to check the equivalence of two target functions under input permutation and input/output phase assignment. This paper addresses the permutation independent (P-equivalent) Boolean matching problem. We will propose a matching ...

Comments

Information & Contributors

Information

Published In

ICCAD '07: Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design

November 2007

933 pages

ISBN:1424413826

General Chair:
Georges Gielen
ESAT-MICAS, Katholieke Univ. Leuven, Leuven, Belgium

Publisher

IEEE Press

Publication History

Published: 05 November 2007

Check for updates

Qualifiers

Research-article

Conference

ICCAD07

Sponsor:

CEDA
SIGDA
IEEE-CS\DATC

ICCAD07: The International Conference on Computer-Aided Design 2007

November 5 - 8, 2007

California, San Jose

Acceptance Rates

ICCAD '07 Paper Acceptance Rate 139 of 510 submissions, 27%;

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
134
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Lai CJiang JWang KScheffer LPhillips JHu A(2010)Boolean matching of function vectors with strengthened learningProceedings of the International Conference on Computer-Aided Design10.5555/2133429.2133555(596-601)Online publication date: 7-Nov-2010
https://dl.acm.org/doi/10.5555/2133429.2133555
Lai CJiang JWang KSapatnekar S(2010)BooMProceedings of the 47th Design Automation Conference10.1145/1837274.1837398(499-504)Online publication date: 13-Jun-2010
https://dl.acm.org/doi/10.1145/1837274.1837398
Wang KChan CLiu J(2009)Simulation and SAT-based Boolean matching for large Boolean networksProceedings of the 46th Annual Design Automation Conference10.1145/1629911.1630016(396-401)Online publication date: 26-Jul-2009
https://dl.acm.org/doi/10.1145/1629911.1630016
Marques-Silva JPlanes JSciuto D(2008)Algorithms for maximum satisfiability using unsatisfiable coresProceedings of the conference on Design, automation and test in Europe10.1145/1403375.1403474(408-413)Online publication date: 10-Mar-2008
https://dl.acm.org/doi/10.1145/1403375.1403474

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Recommendations

Stochastic local search for incremental SAT

Pseudo-Boolean Solving by incremental translation to SAT

Simulation and SAT-based Boolean matching for large Boolean networks

Comments

Information

Published In

Sponsors

Publisher

Publication History

Check for updates

Qualifiers

Conference

Acceptance Rates

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Login options

Full Access

View options

PDF

eReader

Share

Share this Publication link

Share on social media

Affiliations