{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T02:22:06Z","timestamp":1725502926485},"reference-count":23,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012,11]]},"DOI":"10.1109\/hldvt.2012.6418236","type":"proceedings-article","created":{"date-parts":[[2013,1,30]],"date-time":"2013-01-30T22:50:54Z","timestamp":1359586254000},"page":"1-8","source":"Crossref","is-referenced-by-count":0,"title":["Sequential equivalence checking of hard instances with targeted inductive invariants and efficient filtering strategies"],"prefix":"10.1109","author":[{"given":"Huy","family":"Nguyen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael S.","family":"Hsiao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","first-page":"288","article-title":"Static logic implication with application to fast redundancy identification","author":"zhao","year":"0","journal-title":"Proc IEEE VLSI Test Symp 1997"},{"journal-title":"Sequential Equivalence Checking Benchmarks","year":"0","key":"22"},{"key":"17","first-page":"733","article-title":"SEChecker: A Sequential Equivalence Checking Framework Based on Kth Invariants","author":"lu","year":"2009","journal-title":"IEEE Trans Very Large Scale Integration Systems"},{"journal-title":"ABC A System for Sequential Synthesis and Verification","year":"2006","key":"23"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1109\/VLSID.2007.80"},{"key":"15","article-title":"Detection of Equivalent State Variables in Finite State Machine Verification","author":"eijk","year":"0","journal-title":"Proc Int Wkshp Logic & Synthesis 1995"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1109\/12.859539"},{"key":"13","first-page":"108","article-title":"Checking Safety Properties Using Induction and a SAT-Solver","author":"sheeran","year":"0","journal-title":"Proc Int Conf Formal Methods in CAD 2000"},{"key":"14","first-page":"14","article-title":"Bounded Model Checking and Induction: From Refutation to Verification","author":"moura","year":"0","journal-title":"Proc Int Conf Computer-Aided Verification 2003"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1999.781333"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382542"},{"key":"21","first-page":"163","article-title":"A graph traversal based framework for sequential logic implication with an application to c-cycle redundancy identification","author":"zhao","year":"0","journal-title":"Proc Int Conf VLSI Design 2001"},{"key":"3","first-page":"1","article-title":"Speeding up Bounded Sequential Equivalence Checking with Crosstime Frame State-pair Constraints from Data Learning","author":"chang","year":"0","journal-title":"International Test Conf 2009"},{"key":"20","first-page":"1597","article-title":"Using Global Structural Relationships of Signals to Accelerate SAT-based Combinational Equivalence checking","author":"arora","year":"2004","journal-title":"Journal of Universal Computer Science"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1109\/ATS.2010.81"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147098"},{"key":"10","first-page":"250","article-title":"Applying SAT Methods in Unbounded Symbolic Model Checking","author":"mcmillan","year":"0","journal-title":"Proc Int Conf Computer-Aided Verification 2002"},{"key":"7","first-page":"1170","article-title":"A compositional approach to the combination of combinational and sequential equivalence checking of circuits without known reset states","author":"bjesse","year":"0","journal-title":"Proc Design Aut and Test in Europe Conf 2007"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/43.180261"},{"key":"5","article-title":"Inductively Findinga Reachable State Space Over-Approximation","author":"case","year":"0","journal-title":"Proc Int Wkshp Logic & Synthesis 2006"},{"key":"4","article-title":"Ichecker: An efficient checker for inductive invariants","author":"lu","year":"0","journal-title":"Proc IEEE Int'l High-level Design Validation and Test Workshop 2006"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"journal-title":"An Extensible SAT-solver [Ver 1 2]","year":"2003","author":"een","key":"8"}],"event":{"name":"2012 IEEE International High Level Design Validation and Test Workshop (HLDVT)","start":{"date-parts":[[2012,11,9]]},"location":"Huntington Beach, CA, USA","end":{"date-parts":[[2012,11,10]]}},"container-title":["2012 IEEE International High Level Design Validation and Test Workshop (HLDVT)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/6412847\/6418230\/06418236.pdf?arnumber=6418236","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,21]],"date-time":"2017-03-21T20:50:00Z","timestamp":1490129400000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6418236\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,11]]},"references-count":23,"URL":"https:\/\/doi.org\/10.1109\/hldvt.2012.6418236","relation":{},"subject":[],"published":{"date-parts":[[2012,11]]}}}