Scalable exploration of functional dependency by interpolation and incremental SAT solving

ABSTRACT

Functional dependency is concerned with rewriting a Boolean function f as a function h over a set of base functions {g₁, ..., g_n}, i.e. f = h(g₁, ..., g_n). It plays an important role in many aspects of electronic design automation (EDA), ranging from logic synthesis to formal verification. 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 proposes a novel reformulation that extensively exploits the capability of modern satisfiability (SAT) solvers. Thereby, functional dependency is detected effectively through incremental SAT solving, and the dependency function h, if it exists, is obtained through Craig interpolation. The main strengths of the proposed approach include: (1) fast detection of functional dependency with modest memory consumption and thus scalable to large designs, (2) a full capacity to handle a large set of base functions and thus discovering dependency whenever exists, and (3) potential application to large-scale logic optimization and verification reduction. Experimental results show the proposed method is far superior to prior work and scales well in dealing with the largest ISCAS89 and ITC99 benchmark circuits with up to 200K gates.

REFERENCES

• 1: J.-H. R. Jiang and R. K. Brayton. Functional dependency for verification reduction. In Proc. CAV, pp. 268--280, 2004.
• 2: Ellen M. Sentovich , Horia Toma , Gérard Berry, Latch optimization in circuits generated from high-level descriptions, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.428-435, November 10-14, 1996, San Jose, California, United States
• 3: B. Lin and A. R. Newton. Exact redundant state registers removal based on binary decision diagrams. In Proc. Int'l Conf. Very Large Scale Integration, pp. 277--286, 1991.
• 4: Victor N. Kravets , Prabhakar Kudva, Implicit enumeration of structural changes in circuit optimization, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996691]
• 5: Alan J. Hu , David L. Dill, Reducing BDD size by exploiting functional dependencies, Proceedings of the 30th international conference on Design automation, p.266-271, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164888]
• 6: C. Berthet, O. Coudert, and J.-C. Madre. New ideas on symbolic manipulations of finite state machines. In Proc. ICCD, pp. 224--227, 1990.
• 7: C. A. J. Van Eijk , J. A. G. Jess, Exploiting Functional Dependencies in Finite State Machine Verification, Proceedings of the 1996 European conference on Design and Test, p.9, March 11-14, 1996
• 8: E. Gregoire, R. Ostrowski, B. Mazure, and L. Sais. Automatic extraction of functional dependencies. In Proc. SAT, 2004.
• 9: Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
• 10: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 11: N. Eén and N. Sörensson. An extensible SAT-solver. In Proc. SAT, pp. 502--518, 2003.
• 12: Alan Mishchenko , Robert K. Brayton, SAT-Based Complete Don't-Care Computation for Network Optimization, Proceedings of the conference on Design, Automation and Test in Europe, p.412-417, March 07-11, 2005 [doi>10.1109/DATE.2005.264]
• 13: 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. on CAD, vol. 25, no. 5, pp. 742--755, 2006.
• 14: W. Craig. Linear reasoning: A new form of the Herbrand-Gentzen theorem. J. Symbolic Logic, 22(3):250--268, 1957.
• 15: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 16: J. Krajicek. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symbolic Logic, 62(2):457--486, June 1997.
• 17: P. Pudlak. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbolic Logic, 62(3):981--998, September 1997.
• 18: K. L. McMillan. Interpolation and SAT-based model checking. In Proc. CAV, pp. 1--13, 2003.
• 19: G. Tseitin. On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, pp. 466--483, 1970.
• 20: David A. Plaisted , Steven Greenbaum, A structure-preserving clause form translation, Journal of Symbolic Computation, v.2 n.3, p.293-304, Sept. 1986 [doi>10.1016/S0747-7171(86)80028-1]
• 21: Jesse Whittemore , Joonyoung Kim , Karem Sakallah, SATIRE: a new incremental satisfiability engine, Proceedings of the 38th conference on Design automation, p.542-545, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379019]
• 22: R. Jhala and K. L. McMillan, "Interpolant-based transition relation approximation". Proc. CAV, pp. 39--51, 2005.
• 23: Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification. Release 51205. http://www.eecs.berkeley.edu/~alanmi/abc/
• 24: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
• 25: Y. Novikov and R. Brinkmann. Foundations of Hierarchical SAT-Solving. In Proc. Int'l Workshop on Boolean Problems, 2004.
• 26: A. Mishchenko, R. Brayton, J.-H. R. Jiang, and S. Jang. SAT-based logic optimization and resynthesis. In Proc. IWLS, pp. 358--364, 2007.