Subscribe

Issue No.04 - April (2010 vol.59)

pp: 457-467

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

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2010.12

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

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.12REFERENCES

- [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.- [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.- [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.- [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. |