{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T10:41:08Z","timestamp":1761648068433},"reference-count":54,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"8","license":[{"start":{"date-parts":[[2013,8,1]],"date-time":"2013-08-01T00:00:00Z","timestamp":1375315200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2013,8]]},"DOI":"10.1109\/tcad.2013.2252055","type":"journal-article","created":{"date-parts":[[2013,7,15]],"date-time":"2013-07-15T18:03:55Z","timestamp":1373911435000},"page":"1274-1287","source":"Crossref","is-referenced-by-count":5,"title":["Formal Guarantees for Localized Bug Fixes"],"prefix":"10.1109","volume":"32","author":[{"given":"Srobona","family":"Mitra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ansuman","family":"Banerjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pallab","family":"Dasgupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Priyankar","family":"Ghosh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harish","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","first-page":"120","article-title":"Smart simulation using collaborative formal and simulation engines","author":"ho","year":"2000","journal-title":"Proc ICCAD"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2007.30"},{"key":"ref33","author":"swamy","year":"1996","journal-title":"Incremental Methods for Formal Verification and Logic Synthesis"},{"key":"ref32","first-page":"458","article-title":"Incremental formal design verification","author":"swamy","year":"1994","journal-title":"Proc ICCAD"},{"key":"ref31","author":"sokolsky","year":"1996","journal-title":"Efficient Graph-Based Algorithms for Model Checking in the Modal Mu-calculus"},{"key":"ref30","first-page":"351","article-title":"Incremental model checking in the modal mu-calculus","author":"sokolsky","year":"1994","journal-title":"Proc CAV"},{"key":"ref37","first-page":"144","article-title":"An incremental approach to model checking progress properties","author":"bradley","year":"2011","journal-title":"Proc FMCAD"},{"key":"ref36","first-page":"70","article-title":"SAT-Based model checking without unrolling","author":"bradley","year":"2011","journal-title":"Proc VMCAI"},{"key":"ref35","first-page":"98","article-title":"Incremental and complete bounded model checking for full PLTL","author":"heljanko","year":"2005","journal-title":"Proc CAV"},{"key":"ref34","first-page":"135","article-title":"Incremental formal verification of hardware","author":"chockler","year":"2011","journal-title":"Proc FMCAD"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2005.1560184"},{"key":"ref27","first-page":"204","article-title":"Debugging sequential circuits using Boolean satisfiability","author":"ali","year":"2004","journal-title":"Proc ICCAD"},{"key":"ref29","first-page":"1","article-title":"Incremental LTL model checking","author":"cohen","year":"2003","journal-title":"Proc Workshop Semantics Verification Hardw Softw Syst"},{"key":"ref2","year":"0","journal-title":"SystemVerilog 3 1a Language Reference Manual"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2008.212"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/92.311641"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/127601.127647"},{"key":"ref21","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/s100090100069","article-title":"Program slicing for VHDL","author":"clarke","year":"2002","journal-title":"Proc STTT"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2006.5"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0019419"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2006.882511"},{"key":"ref25","author":"chang","year":"2007","journal-title":"Functional Design Errors in Digital Circuits Diagnosis Correction and Repair"},{"key":"ref50","first-page":"298","article-title":"Program slicing of hardware description languages","author":"clarke","year":"1999","journal-title":"Proc CHARME"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.04.017"},{"key":"ref54","author":"ou","year":"2007","journal-title":"Hardware description language program slicing and way to reduce bounded model checking search overhead"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1109\/ICVD.2004.1260983"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-006-0022-x"},{"key":"ref10","year":"0","journal-title":"The Verilog PLI Handbook"},{"key":"ref11","year":"0","journal-title":"zChaff SAT Solver"},{"key":"ref40","first-page":"376","article-title":"On Combining formal and informal verification","author":"yuan","year":"1997","journal-title":"Proc CAV"},{"key":"ref12","author":"aziz","year":"1997","journal-title":"Examples of HW Verification Using VIS"},{"key":"ref13","year":"0","journal-title":"NuSMV A New Symbolic Model Checker"},{"key":"ref14","year":"0","journal-title":"VIS A Formal Verification Tool from Colorado University"},{"key":"ref15","year":"0","journal-title":"Magellan - Hybrid RTL Formal Verification"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277207"},{"key":"ref17","first-page":"30","article-title":"Automating the diagnosis and the rectification of design errors with priam","author":"madre","year":"1989","journal-title":"Proc IEEE ICCAD"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/EURDAC.1992.246202"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/EURDAC.1993.410646"},{"key":"ref4","year":"0","journal-title":"OpenSPARC T1 Microarchitecture Specification Part-819-6650-11 February 2009 Revision B"},{"key":"ref3","year":"0","journal-title":"OpenSPARC T1"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882319"},{"key":"ref5","year":"0","journal-title":"SystemVerilog from Accellera"},{"key":"ref8","year":"0","journal-title":"VCS"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/93542.93576"},{"key":"ref49","first-page":"132","article-title":"Program Slicing on VHDL Descriptions and Its Applications","author":"iwaihara","year":"1996","journal-title":"Proc APCHDL"},{"key":"ref9","year":"0","journal-title":"Synopsys"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0050-0"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(98)00086-X"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010248"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"ref41","author":"hazra","year":"2012","journal-title":"Cohesive Coverage Management Leveraging Formal Test Plans"},{"key":"ref44","first-page":"98","article-title":"Incremental verification by abstraction","author":"lakhnech","year":"2001","journal-title":"Proc TACAS"},{"key":"ref43","first-page":"154","article-title":"Counterexample-guided abstraction refinement","author":"clarke","year":"2000","journal-title":"Proc CAV"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/43\/6558853\/06558891.pdf?arnumber=6558891","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,29]],"date-time":"2021-11-29T20:40:26Z","timestamp":1638218426000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6558891\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,8]]},"references-count":54,"journal-issue":{"issue":"8"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2013.2252055","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"value":"0278-0070","type":"print"},{"value":"1937-4151","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,8]]}}}