{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:55Z","timestamp":1761611335607},"reference-count":56,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"11","license":[{"start":{"date-parts":[[2013,11,1]],"date-time":"2013-11-01T00:00:00Z","timestamp":1383264000000},"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,11]]},"DOI":"10.1109\/tcad.2013.2267454","type":"journal-article","created":{"date-parts":[[2013,10,16]],"date-time":"2013-10-16T18:03:30Z","timestamp":1381946610000},"page":"1801-1813","source":"Crossref","is-referenced-by-count":12,"title":["POWER-TRUCTOR: An Integrated Tool Flow for Formal Verification and Coverage of Architectural Power Intent"],"prefix":"10.1109","volume":"32","author":[{"given":"Aritra","family":"Hazra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajdeep","family":"Mukherjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pallab","family":"Dasgupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ajit","family":"Pal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kevin M.","family":"Harer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ansuman","family":"Banerjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Subhankar","family":"Mukherjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/DDECS.2009.5012137"},{"key":"ref38","year":"2008","journal-title":"An Industrial Formal Verification Tool from Synopsys"},{"key":"ref33","author":"keating","year":"2008","journal-title":"Low Power Methodology Manual (LPMM)?For System-on-Chip Design"},{"key":"ref32","author":"jadcherla","year":"2009","journal-title":"Verification Methodology Manual for Low Power (VMM-LP)"},{"key":"ref31","year":"2005","journal-title":"Incisive Unified Simulator From Cadence Design System"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2006.8"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2009.5185383"},{"key":"ref36","year":"2008","journal-title":"Low Power Design"},{"key":"ref35","author":"vivolo","year":"2008","journal-title":"Synopsys' Low Power Solution Synopsys White Paper"},{"key":"ref34","first-page":"53","article-title":"Power assertions and coverage for improving quality of low power verification and closure of power intent","author":"khan","year":"2008","journal-title":"Proc DVCON"},{"key":"ref28","year":"2006","journal-title":"IEEE 1364?2005 Standard Verilog Hardware Description Language"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837469"},{"key":"ref29","year":"2010","journal-title":"Incisive Formal Verifier From Cadence Design Systems"},{"key":"ref2","first-page":"59","article-title":"Assertion-based verification for power-cycled system-on-chip","author":"anderson","year":"2008","journal-title":"Proc DVCON"},{"key":"ref1","year":"2011","journal-title":"Advanced Configuration and Power Interface (Revision 5 0)"},{"key":"ref20","first-page":"288","article-title":"Functional verification of low power designs at RTL","volume":"lncs 4644","author":"crone","year":"2007","journal-title":"Proc Workshop Power Timing Model Optimization Simulation (PATMOS)"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2010.5496647"},{"key":"ref21","author":"hsu","year":"2008","journal-title":"Eclypse Low Power Solution Clock Tree Synthesis Synopsys White Paper"},{"key":"ref24","year":"2008","journal-title":"Tool From Mentor Graphics"},{"key":"ref23","article-title":"Design for Power Gating?And what UPF can, and cannot, do for you","author":"flynn","year":"2009","journal-title":"Proc SNUG"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2011.2180548"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2012.6165024"},{"key":"ref50","author":"roy","year":"2000","journal-title":"Low-Power CMOS VLSI Circuit Design"},{"key":"ref51","author":"snyder","year":"2008","journal-title":"Formal Verification Checks IC Power Reduction Features"},{"key":"ref56","author":"wilson","year":"2008","journal-title":"A Turn-Off Power Management Complicates Life for Verification Engineers (EDN)"},{"key":"ref55","year":"2008","journal-title":"Unified Power Format 2 0 Standard [Draft Version]?IEEE Draft Standard for Design and Verification of Low Power Integrated Circuits"},{"key":"ref54","year":"0","journal-title":"A Power-Performance Analysis Simulator From IBM"},{"key":"ref53","year":"2004","journal-title":"SystemVerilog LRM 3 1a by Accellera"},{"key":"ref52","year":"2007","journal-title":"Early Power Estimation Tool From Atrenta"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1147\/rd.475.0653"},{"key":"ref11","author":"komar","year":"2007","journal-title":"Formal validation of low-power designs Cadence Designer Network Silicon Valley"},{"key":"ref40","first-page":"262","article-title":"Enhanced LEON3 low power IP core for DSM technologies","author":"marcinek","year":"2009","journal-title":"Proc 14th Int Conf Mixed Design Integr Circuits Syst (MIXDES'07)"},{"key":"ref12","year":"2007","journal-title":"Complete Low-Power Flow Using CPF to Capture Power Intent Internal Paper"},{"key":"ref13","year":"2007","journal-title":"Architecting Designing Implementing and Verifying Low-Power Digital Integrated Circuits White Paper"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-2325-3"},{"key":"ref15","first-page":"742","article-title":"Experiences of low power design implementation and verification","author":"chen","year":"2008","journal-title":"Proc ASP-DAC"},{"key":"ref16","article-title":"Low power verification methodology for DSP core using SVTB","author":"cherukuri","year":"2009","journal-title":"Proc SNUG"},{"key":"ref17","first-page":"3","article-title":"Upping verification productivity of low power designs","author":"chidolue","year":"2008","journal-title":"Proc DVCON"},{"key":"ref18","author":"clarke","year":"2000","journal-title":"Model checking"},{"key":"ref19","first-page":"570","article-title":"SatAbs: SAT-based predicate abstraction for ANSI-C","volume":"lncs 3440","author":"clarke","year":"2005","journal-title":"Proc TACAS"},{"key":"ref4","article-title":"Kick starting power aware verification at the RTL","author":"bailey","year":"2008","journal-title":"Proc EDA Tech Forum (Presentation)"},{"key":"ref3","author":"bailey","year":"2007","journal-title":"Low power design specification from RTL to GDSII (EETimes-India)"},{"key":"ref6","first-page":"11","article-title":"To retain or not to retain: How do I verify the state elements of my low power design","author":"bailey","year":"2008","journal-title":"Proc DVCON"},{"key":"ref5","author":"bailey","year":"2007","journal-title":"Low Power Design and Verification Techniques"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-2355-0"},{"key":"ref7","author":"bamford","year":"2007","journal-title":"Verification of low power designs using CPF (CDNLive)"},{"key":"ref49","article-title":"Challenges of multivoltage verification on a complex low-power design","author":"ram","year":"2008","journal-title":"Proc SNUG"},{"key":"ref9","first-page":"228","article-title":"Low power verification methodology using UPF","author":"bembaron","year":"2009","journal-title":"Proc DVCON"},{"key":"ref46","year":"2008","journal-title":"Power forward initiative A Practical Guide for Low Power Design?An Experience With CPF"},{"key":"ref45","year":"2009","journal-title":"Comprehensive Voltage-Aware Simulator from Synopsys"},{"key":"ref48","year":"2011","journal-title":"Tool From Mentor Graphics"},{"key":"ref47","year":"2005","journal-title":"Property Specification Language"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/VLSID.2013.209"},{"key":"ref41","author":"miller","year":"2008","journal-title":"Early Power Analysis with CPF (EETimes-India)"},{"key":"ref44","year":"2009","journal-title":"Static Voltage-Aware Simulator from Synopsys"},{"key":"ref43","first-page":"42","article-title":"Static and formal verification of power aware designs at the RTL using UPF","author":"mukherjee","year":"2008","journal-title":"Proc DVCON"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/43\/6634535\/06634589.pdf?arnumber=6634589","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,29]],"date-time":"2021-11-29T20:40:27Z","timestamp":1638218427000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6634589\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":56,"journal-issue":{"issue":"11"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2013.2267454","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"value":"0278-0070","type":"print"},{"value":"1937-4151","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,11]]}}}