Full metadata record
DC FieldValueLanguage
dc.contributor.authorChang, Chia-Ling(Lynn)en_US
dc.contributor.authorWen, Charles H. -P.en_US
dc.contributor.authorBhadra, Jayantaen_US
dc.date.accessioned2014-12-08T15:19:58Z-
dc.date.available2014-12-08T15:19:58Z-
dc.date.issued2009en_US
dc.identifier.isbn978-1-4244-4868-5en_US
dc.identifier.issn1089-3539en_US
dc.identifier.urihttp://hdl.handle.net/11536/14145-
dc.description.abstractA learning-and-filtering algorithm is proposed to uncover cross-timeframe state-pair constraints for speeding up SAT solving of bounded sequential equivalence checking (BSEC) problems. First, relaxed Boolean functions for flip-flop states at respective timeframes are learned from a small number of simulation data to derive the initial set of the state-pair candidates. Next, each candidate is examined and removed if both values in such a candidate have coordinately appeared during the simulation. Then, the validity of the remaining candidates is checked against the corresponding augmented circuit. Last, only the true constraints are annotated to the BSEC problems to facilitate SAT solving All benchmark circuits are synthesized under 10 configurations to produce different BSEC problems. Experimental results show that the new SAT solving runs 2-order faster in average compared to using MiniSAT 2.0 only Moreover, given a time bound, the total number of timeframes can increase by 8X-20X on 4 larger circuits after applying the proposed framework.en_US
dc.language.isoen_USen_US
dc.titleSpeeding up Bounded Sequential Equivalence Checking with Cross-Timeframe State-Pair Constraints from Data Learningen_US
dc.typeArticleen_US
dc.identifier.journalITC: 2009 INTERNATIONAL TEST CONFERENCEen_US
dc.citation.spage444en_US
dc.citation.epage451en_US
dc.contributor.department電子工程學系及電子研究所zh_TW
dc.contributor.departmentDepartment of Electronics Engineering and Institute of Electronicsen_US
dc.identifier.wosnumberWOS:000279591000049-
Appears in Collections:Conferences Paper