This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
To SAT or Not to SAT: Scalable Exploration of Functional Dependency
April 2010 (vol. 59 no. 4)
pp. 457-467
ASCII Text
x 
 
Jie-Hong Roland Jiang, Chih-Chun Lee, Alan Mishchenko, Chung-Yang (Ric) Huang, "To SAT or Not to SAT: Scalable Exploration of Functional Dependency," IEEE Transactions on Computers, vol. 59, no. 4, pp. 457-467, April, 2010.
 
 
BibTex
x
 
@article{ 10.1109/TC.2010.12,
author = {Jie-Hong Roland Jiang and Chih-Chun Lee and Alan Mishchenko and Chung-Yang (Ric) Huang},
title = {To SAT or Not to SAT: Scalable Exploration of Functional Dependency},
journal ={IEEE Transactions on Computers},
volume = {59},
number = {4},
issn = {0018-9340},
year = {2010},
pages = {457-467},
doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2010.12},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Computers
TI - To SAT or Not to SAT: Scalable Exploration of Functional Dependency
IS - 4
SN - 0018-9340
SP457
EP467
EPD - 457-467
A1 - Jie-Hong Roland Jiang,
A1 - Chih-Chun Lee,
A1 - Alan Mishchenko,
A1 - Chung-Yang (Ric) Huang,
PY - 2010
KW - Automatic synthesis
KW - design aids
KW - logic design
KW - optimization.
VL - 59
JA - IEEE Transactions on Computers
ER -
 
Jie-Hong Roland Jiang, National Taiwan University, Taipei
Chih-Chun Lee, National Taiwan University, Taipei
Alan Mishchenko, University of California at Berkeley, Berkeley
Chung-Yang (Ric) Huang, National Taiwan University, Taipei
Functional dependency is concerned with rewriting a Boolean function f as a function h over a set of base functions {g_1, \ldots, g_n}, i.e., f = h(g_1, \ldots, g_n). It plays an important role in many aspects of electronic design automation (EDA). Prior approaches to the exploration of functional dependency are based on binary decision diagrams (BDDs), which may not be easily scalable to large designs. This paper formulates both single-output and multiple-output functional dependencies as satisfiability (SAT) solving and exploits extensively the capability of a modern SAT solver. Thereby, functional dependency can be detected effectively through incremental SAT solving, and the dependency function h, if it exists, is obtained through Craig interpolation. The proposed method enables 1) scalable detection of functional dependency, 2) fast enumeration of dependency function under a large set of candidate base functions, and 3) potential application to large-scale logic synthesis and formal verification. Experimental results show that the proposed method is far superior to prior work and scales well in dealing with the largest ISCAS and ITC benchmark circuits with up to 200K gates.

[1] J.-H.R. Jiang and R.K. Brayton, "Functional Dependency for Verification Reduction," Proc. Int'l Conf. Computer Aided Verification, pp. 268-280, 2004.
[2] C.-C. Lee, J.-H.R. Jiang, C.-Y. Huang, and A. Mishchenko, "Scalable Exploration of Functional Dependency by Interpolation and Incremental SAT Solving," Proc. Int'l Conf. Computer-Aided Design, pp. 227-233, 2007.
[3] E. Sentovich, H. Toma, and G. Berry, "Latch Optimization in Circuits Generated from High-Level Descriptions," Proc. Int'l Conf. Computer-Aided Design, pp. 428-435, 1996.
[4] B. Lin and A.R. Newton, "Exact Redundant State Registers Removal Based on Binary Decision Diagrams," Proc. Int'l Conf. Very Large Scale Integration, pp. 277-286, 1991.
[5] V. Kravets and P. Kudva, "Implicit Enumeration of Structural Changes in Circuit Optimization," Proc. Design Automation Conf., pp. 438-441, 2004.
[6] A.J. Hu and D.L. Dill, "Reducing BDD Size by Exploiting Functional Dependencies," Proc. Design Automation Conf., pp. 266-271, 1993.
[7] C. Berthet, O. Coudert, and J.-C Madre, "New Ideas on Symbolic Manipulations of Finite State Machines," Proc. Int'l Conf. Computer Design, pp. 224-227, 1990.
[8] C.A.J. van Eijk and J.A.G. Jess, "Exploiting Functional Dependencies in Finite State Machine Verification," Proc. European Design and Test Conf., pp. 9-14, 1996.
[9] E. Gregoire, R. Ostrowski, B. Mazure, and L. Sais, "Automatic Extraction of Functional Dependencies," Proc. Int'l Conf. Theory and Applications of Satisfiability Testing, pp. 122-132, 2004.
[10] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, vol. 35, no. 8, pp. 677-691, Aug. 1986.
[11] M. Moskewicz, C. Madigan, L. Zhang, and S. Malik, "Chaff: Engineering an Efficient SAT Solver," Proc. Design Automation Conf., pp. 530-535, 2001.
[12] N. Eén and N. Sörensson, "An Extensible SAT-Solver," Proc. Int'l Conf. Theory and Applications of Satisfiability Testing, pp. 502-518, 2003.
[13] A. Mishchenko and R. Brayton, "SAT-Based Complete Don't-Care Computation for Network Optimization," Proc. Design, Automation and Test in Europe, pp. 418-423, 2005.
[14] A. Mishchenko, J. Zhang, S. Sinha, J. Burch, R.K. Brayton, and M. Chrzanowska-Jeske, "Using Simulation and Satisfiability to Compute Flexibilities in Boolean Networks," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 25, no. 5, pp. 742-755, May 2006.
[15] W. Craig, "Linear Reasoning: A New Form of the Herbrand-Gentzen Theorem," J. Symbolic Logic, vol. 22, no. 3, pp. 250-268, 1957.
[16] J.A. Robinson, "A Machine-Oriented Logic Based on the Resolution Principle," J. ACM, vol. 12, no. 1, pp. 23-41, 1965.
[17] J. Krajicek, "Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic," J. Symbolic Logic, vol. 62, no. 2, pp. 457-486, June 1997.
[18] P. Pudlak, "Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations," J. Symbolic Logic, vol. 62, no. 3, pp. 981-998, Sept. 1997.
[19] K.L. McMillan, "Interpolation and SAT-Based Model Checking," Proc. Int'l Conf. Computer Aided Verification, pp. 1-13, 2003.
[20] G.S. Tseitin, "On the Complexity of Derivation in Propositional Calculus," Studies in Constructive Mathematics and Mathematical Logic, Part II, pp. 115-125, Consultants Bureau, 1970.
[21] D. Plaisted and S. Greenbaum, "A Structure Preserving Clause form Translation," J. Symbolic Computation, vol. 2, pp. 293-304, 1986.
[22] J. Whittemore, J. Kim, and K. Sakallah, "SATIRE: A New Incremental Satisfiability Engine," Proc. Design Automation Conf., pp. 542-545, 2001.
[23] R. Jhala and K.L. McMillan, "Interpolant-Based Transition Relation Approximation," Proc. Int'l Conf. Computer Aided Verification, pp. 39-51, 2005.
[24] Berkeley Logic Synthesis and Verification Group, ABC: A System for Sequential Synthesis and Verification, http://www.eecs.berkeley.edu/~alanmiabc/, 2005.
[25] R.K. Brayton et al., "VIS: A System for Verification and Synthesis," Proc. Int'l Conf. Computer Aided Verification, pp. 428-432, 1996.
[26] Y. Novikov and R. Brinkmann, "Foundations of Hierarchical SAT-Solving," Proc. Int'l Workshop Boolean Problems, 2004.
[27] A. Mishchenko, R. Brayton, J.-H.R. Jiang, and S. Jang, "SAT-Based Logic Optimization and Resynthesis," Proc. Int'l Workshop Logic and Synthesis, pp. 358-364, 2007.
[28] R.-R Lee, J.-H.R. Jiang, and W.-L Hung, "Bi-Decomposing Large Boolean Functions via Interpolation and Satisfiability Solving," Proc. Design Automation Conf., pp. 636-641, 2008.
[29] H.-P. Lin, J.-H.R. Jiang, and R.-R Lee, "To SAT or Not to SAT: Ashenhurst Decomposition in a Large Scale," Proc. Int'l Conf. Computer-Aided Design, 2008.

Index Terms:
Automatic synthesis, design aids, logic design, optimization.
Citation:
Jie-Hong Roland Jiang, Chih-Chun Lee, Alan Mishchenko, Chung-Yang (Ric) Huang, "To SAT or Not to SAT: Scalable Exploration of Functional Dependency," IEEE Transactions on Computers, vol. 59, no. 4, pp. 457-467, April 2010, doi:10.1109/TC.2010.12
Usage of this product signifies your acceptance of the Terms of Use.