The Community for Technology Leaders
RSS Icon
Issue No.04 - April (2010 vol.59)
pp: 457-467
J.-H.R. Jiang , Dept. of Electr. Eng., Nat. Taiwan Univ., Taipei, Taiwan
Chih-Chun Lee , Dept. of Electr. Eng., Nat. Taiwan Univ., Taipei, Taiwan
A. Mishchenko , Dept. of Electr. Eng. & Comput. Sci., Univ. of California, Berkeley, CA, USA
Chung-Yang Huang , Dept. of Electr. Eng., Nat. Taiwan Univ., Taipei, Taiwan
Functional dependency is concerned with rewriting a Boolean function f as a function h over a set of base functions {g1,,gn}, i.e., f = h(g1,,gn). 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 200 K gates.
logic design, binary decision diagrams, Boolean functions, computability, electronic design automation,dependency function, functional dependency, rewriting a Boolean function, base functions, electronic design automation, binary decision diagrams, single-output functional dependencies, multiple-output functional dependencies, satisfiability, SAT solver, large-scale logic synthesis, formal verification,Boolean functions, Data structures, Interpolation, Data mining, Probability density function, Junctions, Cost accounting,optimization., Automatic synthesis, design aids, logic design
J.-H.R. Jiang, Chih-Chun Lee, A. Mishchenko, Chung-Yang 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
[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,, 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.
38 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool