{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:58:01Z","timestamp":1759147081731,"version":"3.41.0"},"reference-count":13,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2009,1]]},"abstract":"<jats:p>\n            <jats:italic>Design intent coverage<\/jats:italic>\n            is a formal methodology for analyzing the gap between a formal architectural specification of a design and the formal functional specifications of the component RTL blocks of the design. In this article we extend the design intent coverage methodology to hybrid specifications containing both state-machines and formal properties. We demonstrate the benefits of this extension in two domains of considerable recent interest, namely (a) the use of auxiliary state-machines in formal specifications, and (b) the use of modest sized RTL blocks in the design intent coverage analysis.\n          <\/jats:p>","DOI":"10.1145\/1455229.1455238","type":"journal-article","created":{"date-parts":[[2009,1,29]],"date-time":"2009-01-29T13:48:36Z","timestamp":1233236916000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Design intent coverage revisited"],"prefix":"10.1145","volume":"14","author":[{"given":"Arnab","family":"Sinha","sequence":"first","affiliation":[{"name":"Indian Institute of Technology, Kharagpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pallab","family":"Dasgupta","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology, Kharagpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bhaskar","family":"Pal","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology, Kharagpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sayantan","family":"Das","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology, Kharagpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Prasenjit","family":"Basu","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology, Kharagpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P. P.","family":"Chakrabarti","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology, Kharagpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,1,23]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"1922","article-title":"Design intent coverage\u2014a new paradigm for formal property verification","volume":"25","author":"Basu P.","year":"2006","unstructured":"Basu , P. , Das , S. , Banerjee , A., P. Dasgupta , P. P. C. , Mohan , C. , Fix , L. , and Armoni , R. 2006 . Design intent coverage\u2014a new paradigm for formal property verification . Comput.-Aid. Des. Int. Circ. Syst. 25 , 10, 1922 -- 1934 . Basu, P., Das, S., Banerjee, A., P. Dasgupta, P. P. C., Mohan, C., Fix, L., and Armoni, R. 2006. Design intent coverage\u2014a new paradigm for formal property verification. Comput.-Aid. Des. Int. Circ. Syst. 25, 10, 1922--1934.","journal-title":"Comput.-Aid. Des. Int. Circ. Syst."},{"volume-title":"Proceedings of the Conference on Computer Aided Verification. 66--78","author":"Chockler H.","key":"e_1_2_1_2_1","unstructured":"Chockler , H. , Kupferman , O. , Kurshan , R. P. , and Vardi , Y. M . 2001. A practical approach to coverage in model checking . In Proceedings of the Conference on Computer Aided Verification. 66--78 . Chockler, H., Kupferman, O., Kurshan, R. P., and Vardi, Y. M. 2001. A practical approach to coverage in model checking. In Proceedings of the Conference on Computer Aided Verification. 66--78."},{"volume-title":"Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. 528--542","author":"Chockler H.","key":"e_1_2_1_3_1","unstructured":"Chockler , H. , Kupferman , O. , and Vardi , M. Y . 2001. Coverage metrics for temporal logic model checking . In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. 528--542 . Chockler, H., Kupferman, O., and Vardi, M. Y. 2001. Coverage metrics for temporal logic model checking. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. 528--542."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39724-3_11"},{"key":"e_1_2_1_5_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking. MIT Press.   Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking. MIT Press."},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Das S. Basu P. Dasgupta P. and Chakrabarti P. P. 2006. What lies between design intent coverage and model checking&quest; In Proceedings of the Conference on Design Automation and Test in Europe. European Design and Automation Association Munich Germany 1217--1222.   Das S. Basu P. Dasgupta P. and Chakrabarti P. P. 2006. What lies between design intent coverage and model checking&quest; In Proceedings of the Conference on Design Automation and Test in Europe. European Design and Automation Association Munich Germany 1217--1222.","DOI":"10.1109\/DATE.2006.244051"},{"volume-title":"A Roadmap for Formal Property Verification","author":"Dasgupta P.","key":"e_1_2_1_7_1","unstructured":"Dasgupta , P. 2006. A Roadmap for Formal Property Verification . Springer . Dasgupta, P. 2006. A Roadmap for Formal Property Verification. Springer."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309936"},{"volume-title":"Proceedings of the Conference on Correct Hardware Design and Verification Methods. 280--297","author":"Katz S.","key":"e_1_2_1_9_1","unstructured":"Katz , S. , Grumberg , O. , and Geist , D . 1999. Have i written enough properties&quest;\u201d\u2014a method of comparison between specification and implementation . In Proceedings of the Conference on Correct Hardware Design and Verification Methods. 280--297 . Katz, S., Grumberg, O., and Geist, D. 1999. Have i written enough properties&quest;\u201d\u2014a method of comparison between specification and implementation. In Proceedings of the Conference on Correct Hardware Design and Verification Methods. 280--297."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the Foundations of Computer Science. 46--57","author":"Pnueli A.","year":"1977","unstructured":"Pnueli , A. 1977 . The complexity of propositional linear temporal logics . In Proceedings of the Foundations of Computer Science. 46--57 . Pnueli, A. 1977. The complexity of propositional linear temporal logics. In Proceedings of the Foundations of Computer Science. 46--57."},{"key":"e_1_2_1_11_1","unstructured":"PSL. Property Specification Language (PSL). www.eda.org\/vfv\/docs\/PSL-v1.1.pdf. PSL.  PSL. Property Specification Language (PSL). www.eda.org\/vfv\/docs\/PSL-v1.1.pdf. PSL."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"e_1_2_1_13_1","unstructured":"SVA. SystemVerilog 3.1a Language Reference Manual. www.eda.org\/sv\/SystemVerilog_3.1a.pdf. SVA.  SVA. SystemVerilog 3.1a Language Reference Manual. www.eda.org\/sv\/SystemVerilog_3.1a.pdf. SVA."}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1455229.1455238","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1455229.1455238","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:00Z","timestamp":1750253400000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1455229.1455238"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,1]]}},"alternative-id":["10.1145\/1455229.1455238"],"URL":"https:\/\/doi.org\/10.1145\/1455229.1455238","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2009,1]]},"assertion":[{"value":"2007-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-01-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}