{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:38:07Z","timestamp":1750307887150,"version":"3.41.0"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2008,9,1]],"date-time":"2008-09-01T00:00:00Z","timestamp":1220227200000},"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":[[2008,9]]},"abstract":"<jats:p>\n            Formal specifications of interface protocols between a design-under-test and its environment mostly consist of two types of correctness requirements, namely (a) a set of invariants that applies throughout the protocol execution and (b) a set of\n            <jats:italic>context-triggered<\/jats:italic>\n            properties that applies only when the protocol state belongs to a specific set of contexts. To model such requirements, an increasingly popular design choice in the assertion IP design community has been the use of abstract\n            <jats:italic>context state machines<\/jats:italic>\n            and state-oriented properties. In this paper, we formalize this modeling style and present algorithms for verifying such specifications. Specifically, we present a purely formal approach and a semi-formal approach for verifying such specifications. We demonstrate the use of this design style in modeling some of the industry standard protocol descriptions and present encouraging results.\n          <\/jats:p>","DOI":"10.1145\/1391962.1391970","type":"journal-article","created":{"date-parts":[[2008,10,7]],"date-time":"2008-10-07T12:48:29Z","timestamp":1223383709000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Auxiliary state machines + context-triggered properties in verification"],"prefix":"10.1145","volume":"13","author":[{"given":"Ansuman","family":"Banerjee","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":"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":[[2008,10,3]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"B\u00f6rger E. and St\u00e4rk R. 2003. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag.   B\u00f6rger E. and St\u00e4rk R. 2003. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag.","DOI":"10.1007\/978-3-642-18216-7"},{"volume-title":"Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'99)","author":"Biere A.","key":"e_1_2_1_2_1","unstructured":"Biere , A. , Cimatti , A. , Clarke , E. M. , and Zhu , Y . 1999. Symbolic model checking without bdds . In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'99) . Springer-Verlag, 193--207. Biere, A., Cimatti, A., Clarke, E. M., and Zhu, Y. 1999. Symbolic model checking without bdds. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'99). Springer-Verlag, 193--207."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/647765.735860"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/127601.127702"},{"volume-title":"Proceedings of the ASIC Conference. 27--31","author":"Chauhan P.","key":"e_1_2_1_5_1","unstructured":"Chauhan , P. , Clarke , E. M. , Lu , Y. , and Wang , D . 1999. Verifying Ip-core based system-on-chip designs . In Proceedings of the ASIC Conference. 27--31 . Chauhan, P., Clarke, E. M., Lu, Y., and Wang, D. 1999. Verifying Ip-core based system-on-chip designs. In Proceedings of the ASIC Conference. 27--31."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/157485.164555"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"volume-title":"A Roadmap for Formal Property Verification","author":"Dasgupta P.","key":"e_1_2_1_8_1","unstructured":"Dasgupta , P. 2006. A Roadmap for Formal Property Verification . Springer-Verlag . Dasgupta, P. 2006. A Roadmap for Formal Property Verification. Springer-Verlag."},{"volume-title":"Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'00)","author":"Govindaraju S. G.","key":"e_1_2_1_9_1","unstructured":"Govindaraju , S. G. and Dill , D. L . 2000. Counterexample-guided choice of projections in approximate symbolic model checking . In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'00) . IEEE Press, 115--119. Govindaraju, S. G. and Dill, D. L. 2000. Counterexample-guided choice of projections in approximate symbolic model checking. In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'00). IEEE Press, 115--119."},{"volume-title":"Proceedings of the 10th International Conference on Computer Aided Verification (CAV'98)","author":"Kaufmann M.","key":"e_1_2_1_10_1","unstructured":"Kaufmann , M. , Martin , A. , and Pixley , C . 1998. Design constraints in symbolic model checking . In Proceedings of the 10th International Conference on Computer Aided Verification (CAV'98) . Springer-Verlag, 477--487. Kaufmann, M., Martin, A., and Pixley, C. 1998. Design constraints in symbolic model checking. In Proceedings of the 10th International Conference on Computer Aided Verification (CAV'98). Springer-Verlag, 477--487."},{"volume-title":"Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'05)","author":"Nguyen M. D.","key":"e_1_2_1_11_1","unstructured":"Nguyen , M. D. , Stoffel , D. , Wedler , M. , and Kunz , W . 2005. Transition-by-transition fsm traversal for reachability analysis in bounded model checking . In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'05) . IEEE Computer Society, 1068--1075. Nguyen, M. D., Stoffel, D., Wedler, M., and Kunz, W. 2005. Transition-by-transition fsm traversal for reachability analysis in bounded model checking. In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'05). IEEE Computer Society, 1068--1075."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-007-0036-3"},{"volume-title":"Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'01)","author":"Shimizu K.","key":"e_1_2_1_14_1","unstructured":"Shimizu , K. , Dill , D. L. , and Chou , C . -T. 2001. A specification methodology by a collection of compact properties as applied to the intel\u00ae itaniumtm processor bus protocol . In Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'01) . Springer-Verlag, 340--354. Shimizu, K., Dill, D. L., and Chou, C.-T. 2001. A specification methodology by a collection of compact properties as applied to the intel\u00ae itaniumtm processor bus protocol. In Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'01). Springer-Verlag, 340--354."},{"volume-title":"Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD'00)","author":"Shimizu K.","key":"e_1_2_1_15_1","unstructured":"Shimizu , K. , Dill , D. L. , and Hu , A. J . 2000. Monitor-based formal specification of pci . In Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD'00) . Springer-Verlag, 335--353. Shimizu, K., Dill, D. L., and Hu, A. J. 2000. Monitor-based formal specification of pci. In Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD'00). Springer-Verlag, 335--353."},{"volume-title":"Proceedings of the Conference on Design, Automation and Test in Europe (DATE'06)","author":"Shyam S.","key":"e_1_2_1_16_1","unstructured":"Shyam , S. and Bertacco , V . 2006. Distance-guided hybrid verification with guido . In Proceedings of the Conference on Design, Automation and Test in Europe (DATE'06) . European Design and Automation Association, 1211--1216. Shyam, S. and Bertacco, V. 2006. Distance-guided hybrid verification with guido. In Proceedings of the Conference on Design, Automation and Test in Europe (DATE'06). European Design and Automation Association, 1211--1216."},{"key":"e_1_2_1_17_1","volume-title":"Cudd: CU decision diagram package, release 2.3.0, User's Manual.","author":"Somenzi F.","year":"1998","unstructured":"Somenzi , F. 1998 . Cudd: CU decision diagram package, release 2.3.0, User's Manual. Somenzi, F. 1998. Cudd: CU decision diagram package, release 2.3.0, User's Manual."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2003.812320"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1391962.1391970","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1391962.1391970","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:47:13Z","timestamp":1750258033000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1391962.1391970"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,9]]},"references-count":18,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2008,9]]}},"alternative-id":["10.1145\/1391962.1391970"],"URL":"https:\/\/doi.org\/10.1145\/1391962.1391970","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2008,9]]},"assertion":[{"value":"2007-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-10-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}