Extracting logic circuit structure from conjunctive normal form descriptions

Zhaohui Fu, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

18 Scopus citations

Abstract

Boolean Satisfiability is seeing increasing use as a decision procedure in Electronic Design Automation (EDA) and other domains. Most applications encode their domain specific constraints in Conjunctive Normal Form (CNF), which is accepted as input by most efficient contemporary SAT solvers [1-3]. However, such translation may have information loss. For example, when a circuit is encoded into CNF, structural information such as gate orientation, logic paths, signal observability, etc. is lost. However, recent research [4-6] shows that a substantial amount of the lost information can be restored in circuit form. This paper presents an efficient algorithm (CNF2CKT) for extracting circuit information from CNF instances. CNF2CKT is optimal in the sense that it extracts a maximum acyclic combinational circuit from any given CNF using the logic gates pre-specified in a library. The extracted circuit structure is valuable in various ways, particularly when the CNF is not encoded from the circuit, or the circuit description is not readily available. As an example, we show that the extracted circuit structure can be used to derive Circuit Observability Don't Cares [7] for speeding up CNF-SAT [8].

Original languageEnglish (US)
Title of host publicationProceedings - 20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems
Pages37-42
Number of pages6
DOIs
StatePublished - Dec 1 2007
Event20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems, VLSID'07 - Bangalore, India
Duration: Jan 6 2007Jan 10 2007

Other

Other20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems, VLSID'07
CountryIndia
CityBangalore
Period1/6/071/10/07

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Extracting logic circuit structure from conjunctive normal form descriptions'. Together they form a unique fingerprint.

  • Cite this

    Fu, Z., & Malik, S. (2007). Extracting logic circuit structure from conjunctive normal form descriptions. In Proceedings - 20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems (pp. 37-42). [4092020] https://doi.org/10.1109/VLSID.2007.81