布林配對尋找兩個電路的輸入/輸出之對應/補數關係，使得兩者功能相等。這在電路修正與技術映射中很重要。先前的文獻探討了輸入/輸出數量相等的情形，但它們無法處理非確切投射布林配對，也就是輸入/輸出數量不相同的情形。我們使用了基於布林可滿足問題的方法與函數性質(對稱)，以設計一套可用於非確切布林配對的技巧。我們設計的技巧可以使布林配對加速收斂。新定義的函數性質與對應的方法能移除更多的不可行解並避免過度修剪解空間。實驗顯示，不限於非確切布林配對，我們提出的方法有更好的能力解決較大的電路問題。

Boolean matching is to determine whether two circuits can be equivalent under permutation and/or negation of their inputs and outputs. It is important in circuit rectification and technology mapping. Previous works discussed Boolean matching under the same numbers of inputs and outputs. They are inapplicable to Non-exact Projective NPNP Boolean matching (NP3), in which inputs/outputs numbers of two circuits are different. We use SAT-based method and functional properties (symmetry) to design a technique which is applicable to NP3. We design a technique to speed up convergence of Boolean matching procedure. A newly defined functional property is used to remove more infeasible solutions. Experimental data shows, besides to NP3, the proposed technique has better capability of matching circuits with large number of inputs.

[1] A. Abdollahi and M. Pedram. Symmetry detection and boolean matching utilizing a
signature-based canonical form of boolean functions. IEEE Transactions on ComputerAided
Design of Integrated Circuits and Systems, 27(6):1128–1137, June 2008.
[2] Manindra Agrawal and Thomas Thierauf. The boolean isomorphism problem. In Foundations
of Computer Science, 1996. Proceedings., 37th Annual Symposium on, pages
422–430. IEEE, 1996.
[3] S. B. Akers. Binary decision diagrams. IEEE Transactions on Computers, C-27(6):509–
516, June 1978.
[4] Fadi A Aloul, Igor L Markov, and Karem A Sakallah. Mince: A static global variableordering
for sat and bdd.
[5] Gilles Audemard and Laurent Simon. Glucose 2.1: Aggressive - but reactive - clause
database management, dynamic restarts. In Proc. of International Workshop of Pragmatics
of SAT (Affiliated to SAT), Trento, Italie, Jun 2012.
[6] Luca Benini and Giovanni De Micheli. A survey of boolean matching techniques for
library binding. ACM Transactions on Design Automation of Electronic Systems (TODAES),
2(3):193–226, 1997.
[7] Armin Biere, Keijo Heljanko, and Siert Wieringa. Aiger 1.9 and beyond. 2011.
[8] Bernd Borchert, Desh Ranjan, and Frank Stephan. On the computational complexity
of some classical equivalence relations on boolean functions. Theory of Computing
Systems, 31(6):679–693, 1998.
[9] Karl S. Brace, Richard L. Rudell, and Randal E. Bryant. Efficient implementation of a
bdd package. In Proceedings of the 27th ACM/IEEE Design Automation Conference,
DAC ’90, pages 40–45, New York, NY, USA, 1990. ACM.
[10] Robert Brayton and Alan Mishchenko. Abc: An academic industrial-strength verification
tool. In International Conference on Computer Aided Verification, pages 24–40.
Springer, 2010.
[11] Randal E Bryant. Graph-based algorithms for boolean function manipulation. IEEE
Transactions on computers, 100(8):677–691, 1986.
[12] Cadence®. Encounter conformal equivalence checker. https:
//www.cadence.com/content/cadence-www/global/en_US/home/
tools/digital-design-and-signoff/equivalence-checking/
conformal-equivalence-checker.html/.
[13] Jason Jingsheng Cong and Yean-Yow Hwang. Boolean matching for lut-based logic
blocks with applications to architecture evaluation and technology mapping. IEEE
82
TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS
AND SYSTEMS, 20(9):1077, 2001.
[14] Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J.
ACM, 7(3):201–215, July 1960.
[15] Niklas Eén and Niklas Sörensson. An extensible sat-solver. In International conference
on theory and applications of satisfiability testing, pages 502–518. Springer, 2003.
[16] Niklas Eén and Niklas Sorensson. Translating pseudo-boolean constraints into sat. Journal
on Satisfiability, Boolean Modeling and Computation, 2:1–26, 2006.
[17] Zhaohui Fu and Sharad Malik. On solving the partial max-sat problem. In International
Conference on Theory and Applications of Satisfiability Testing, pages 252–265.
Springer, 2006.
[18] Chih-Jen Hsu, Wei-Hsun Lin, Chi-An Wu, and Kei-Yong Khoo. Iccad-2014 cad contest
in simultaneous cnf encoder optimization with sat solver setting selection and
benchmark suite. In Proceedings of the 2014 IEEE/ACM International Conference
on Computer-Aided Design, ICCAD ’14, pages 357–360, Piscataway, NJ, USA, 2014.
IEEE Press.
[19] H. Katebi and I. L. Markov. Large-scale boolean matching. In 2010 Design, Automation
Test in Europe Conference Exhibition (DATE 2010), pages 771–776, March 2010.
[20] S. Krishnaswamy, H. Ren, N. Modi, and R. Puri. Deltasyn: An efficient logic difference
optimizer for eco synthesis. In 2009 IEEE/ACM International Conference on ComputerAided
Design - Digest of Technical Papers, pages 789–796, Nov 2009.
[21] Andreas Kuehlmann and Florian Krohm. Equivalence checking using cuts and heaps. In
Proceedings of the 34th annual Design Automation Conference, pages 263–268. ACM,
1997.
[22] Chih-Fan Lai, Jie-Hong R. Jiang, and Kuo-Hua Wang. Boolean matching of function
vectors with strengthened learning. In Proceedings of the International Conference
on Computer-Aided Design, ICCAD ’10, pages 596–601, Piscataway, NJ, USA, 2010.
IEEE Press.
[23] Chih-Fan Lai, Jie-Hong R Jiang, and Kuo-Hua Wang. Boom: a decision procedure for
boolean matching with abstraction and dynamic learning. In Proceedings of the 47th
Design Automation Conference, pages 499–504. ACM, 2010.
[24] Alan Mishchenko, Satrajit Chatterjee, and Robert Brayton. Dag-aware aig rewriting a
fresh look at combinational logic synthesis. In Proceedings of the 43rd annual Design
Automation Conference, pages 532–535. ACM, 2006.
[25] Saburo Muroga. Logic Design and Switching Theory. John Wiley & Sons, Inc., New
York, NY, USA, 1979.
[26] Pawel Swierczynski, Marc Fyrbiak, Christof Paar, Christophe Huriaux, and Russell
Tessier. Protecting against cryptographic trojans in fpgas. In Field-Programmable Custom
Computing Machines (FCCM), 2015 IEEE 23rd Annual International Symposium
on, pages 151–154. IEEE, 2015.
83
[27] Grigori S Tseitin. On the complexity of derivation in propositional calculus. In Automation
of reasoning, pages 466–483. Springer, 1983.
[28] Miroslav N. Velev. Efficient translation of boolean formulas to cnf in formal verification
of microprocessors. In Proceedings of the 2004 Asia and South Pacific Design
Automation Conference, ASP-DAC ’04, pages 310–315, Piscataway, NJ, USA, 2004.
IEEE Press.
[29] K. H. Wang, C. M. Chan, and Jung-Chang Liu. Simulation and sat-based boolean
matching for large boolean networks. In 2009 46th ACM/IEEE Design Automation
Conference, pages 396–401, July 2009.
[30] Chi-An (Rocky) Wu, Chih-Jen (Jacky) Hsu, and Kei-Yong Khoo. Iccad-2016 cad contest
in non-exact projective npnp boolean matching and benchmark suite. In Proceedings
of the 35th International Conference on Computer-Aided Design, ICCAD ’16,
pages 40:1–40:5, New York, NY, USA, 2016. ACM.
[31] Jin S Zhang, Malgorzata Chrzanowska-Jeske, Alan Mishchenko, and Jerry R Burch.
Generalized symmetries in boolean functions: Fast computation and application to
boolean matching. In in IWLS. Citeseer, 2004.