The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.04 - April (2010 vol.59)
pp: 457-467
Chih-Chun Lee , National Taiwan University, Taipei
Alan Mishchenko , University of California at Berkeley, Berkeley
Chung-Yang (Ric) Huang , National Taiwan University, Taipei
ABSTRACT
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.
INDEX TERMS
Automatic synthesis, design aids, logic design, optimization.
CITATION
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
REFERENCES
[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.
21 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool