NDLI: Scalable exploration of functional dependency by interpolation and incremental SAT solving

Content Provider	IEEE Xplore Digital Library
Author	Chih-Chun Lee Jiang, J.-H.R. Chung-Yang Huang Mishchenko, A.
Copyright Year	2007
Description	Author affiliation: Nat. Taiwan Univ., Taipei (Chih-Chun Lee; Jiang, J.-H.R.; Chung-Yang Huang)
Abstract	Functional dependency is concerned with rewriting a Boolean function f as a function h over a set of base functions $\{g_{1},$ ..., $g_{n}),$ i.e. f = $h(g_{1},$ ..., $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 200 K gates.
Starting Page	227
Ending Page	233
File Size	1606011
Page Count	7
File Format	PDF
ISBN	9781424413812
ISSN	10923152
DOI	10.1109/ICCAD.2007.4397270
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2007-11-04
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Interpolation Boolean functions Data structures Binary decision diagrams Electronic design automation and methodology Formal verification Circuit synthesis Space technology Logic design Explosions
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Computer Science Applications Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Scalable exploration of functional dependency by interpolation and incremental SAT solving (2006)

To sat ot not to sat: scalable. (2010).

Scalable exploration of functional dependency by interpolation and incremental SAT solving

Scalable Exploration of Functional Dependency by Interpolation and (2007)

To SAT or not to SAT: Ashenhurst decomposition in a large scale

Formal verification of digital circuits

Design automation with mixtures of proof strategies for propositional logic

Formal verification of the Pentium/sup /spl reg//4 floating-point multiplier

Binary decision diagrams and beyond: enabling technologies for formal verification

Scalable exploration of functional dependency by interpolation and incremental SAT solving

Similar Documents

Scalable exploration of functional dependency by interpolation and incremental SAT solving (2006)

To sat ot not to sat: scalable. (2010).

Scalable exploration of functional dependency by interpolation and incremental SAT solving

Scalable Exploration of Functional Dependency by Interpolation and (2007)

To SAT or not to SAT: Ashenhurst decomposition in a large scale

Formal verification of digital circuits

Design automation with mixtures of proof strategies for propositional logic

Formal verification of the Pentium/sup /spl reg//4 floating-point multiplier

Binary decision diagrams and beyond: enabling technologies for formal verification

Scalable exploration of functional dependency by interpolation and incremental SAT solving