{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:15:00Z","timestamp":1750306500550,"version":"3.41.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2016,1,28]],"date-time":"2016-01-28T00:00:00Z","timestamp":1453939200000},"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":[[2016,1,28]]},"abstract":"<jats:p>\n            Assertion-based verification (ABV) for IP blocks given as synchronous RTL (register transfer level) descriptions has now widely gained acceptance. The challenge addressed here is ABV for\n            <jats:italic>systems on chip<\/jats:italic>\n            (SoC) modeled at the system level in SystemC TLM (Transactional Level Modeling). Requirements to be verified at this level of abstraction usually express temporal constraints on the interactions and communications in the SoC. We use the IEEE standard language PSL to formalize these temporal assertions which represent properties on communication actions and their parameters.\n            <jats:italic>Auxiliary variables<\/jats:italic>\n            are often indispensable for this formalization, but their use may induce semantic issues. This article discusses this matter, analyzes various existing approaches and proposes a summary of their advantages and shortcomings. They are also compared to our syntactic and semantic framework, implemented in a verification tool. The proposed operational semantics has the advantages of being simple and intuitive while supporting both global and local auxiliary variables. Experimental results on industrial case studies illustrate its applicability.\n          <\/jats:p>","DOI":"10.1145\/2811260","type":"journal-article","created":{"date-parts":[[2016,2,1]],"date-time":"2016-02-01T20:37:54Z","timestamp":1454359074000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Auxiliary Variables in Temporal Specifications"],"prefix":"10.1145","volume":"21","author":[{"given":"Laurence","family":"Pierre","sequence":"first","affiliation":[{"name":"TIMA Laboratory, Univ. Grenoble Alpes, CNRS, Grenoble cedex -- France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,1,28]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_21"},{"key":"e_1_2_1_2_1","unstructured":"B. Candaele. 2005. SoC Design for Avanced Applications. http:\/\/www.ics.ele.tue.nl\/dsd\/dsd2005\/files\/DSD05ThalesSept1rstPorto.pdf.  B. Candaele. 2005. SoC Design for Avanced Applications. http:\/\/www.ics.ele.tue.nl\/dsd\/dsd2005\/files\/DSD05ThalesSept1rstPorto.pdf."},{"volume-title":"Proceedings of FMCAD'04","author":"Claessen K.","key":"e_1_2_1_3_1","unstructured":"K. Claessen and J. Martensson . 2004. An operational semantics for weak PSL . In Proceedings of FMCAD'04 . K. Claessen and J. Martensson. 2004. An operational semantics for weak PSL. In Proceedings of FMCAD'04."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISQED.2005.32"},{"volume-title":"Proceedings of MEMOCODE'06","author":"Ecker W.","key":"e_1_2_1_5_1","unstructured":"W. Ecker , V. Esen , and M. Hull . 2006. Execution semantics and formalisms for multi-abstraction TLM assertions . In Proceedings of MEMOCODE'06 . W. Ecker, V. Esen, and M. Hull. 2006. Execution semantics and formalisms for multi-abstraction TLM assertions. In Proceedings of MEMOCODE'06."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1266366.1266559"},{"key":"e_1_2_1_7_1","unstructured":"C. Eisner and D. Fisman. 2006. A Practical Introduction to PSL. Springer.   C. Eisner and D. Fisman. 2006. A Practical Introduction to PSL. Springer."},{"volume-title":"Proceedings of FMCAD'08","author":"Eisner C.","key":"e_1_2_1_8_1","unstructured":"C. Eisner and D. Fisman . 2008. Augmenting a regular expression-based temporal logic with local variables . In Proceedings of FMCAD'08 . C. Eisner and D. Fisman. 2008. Augmenting a regular expression-based temporal logic with local variables. In Proceedings of FMCAD'08."},{"volume-title":"Proceedings of DATE'10","author":"Ferro L.","key":"e_1_2_1_10_1","unstructured":"L. Ferro and L. Pierre . 2010. Formal semantics for PSL modeling layer and application to the verification of transactional models . In Proceedings of DATE'10 . L. Ferro and L. Pierre. 2010. Formal semantics for PSL modeling layer and application to the verification of transactional models. In Proceedings of DATE'10."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1561\/1000000013"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"H. Foster A. Krolnik and D. Lacey. 2003. Assertion-Based Design. Kluwer Academic Pub.   H. Foster A. Krolnik and D. Lacey. 2003. Assertion-Based Design. Kluwer Academic Pub.","DOI":"10.1007\/978-1-4419-9228-4"},{"key":"e_1_2_1_13_1","unstructured":"Mark Glasser. 2006. Applying Transaction-Level Models for Design and Testbenches. SOC Central.  Mark Glasser. 2006. Applying Transaction-Level Models for Design and Testbenches. SOC Central."},{"key":"e_1_2_1_14_1","unstructured":"Richard Goering. 2006. Transaction models offer new deal for EDA. EETimes http:\/\/www.eetimes.com\/showArticle.jhtml?articleID&equals;181503693.  Richard Goering. 2006. Transaction models offer new deal for EDA. EETimes http:\/\/www.eetimes.com\/showArticle.jhtml?articleID&equals;181503693."},{"key":"e_1_2_1_15_1","unstructured":"T. Gr\u00f6tker S. Liao G. Martin and S. Swan. 2002. System Design with SystemC. Kluwer Academic Pub.   T. Gr\u00f6tker S. Liao G. Martin and S. Swan. 2002. System Design with SystemC. Kluwer Academic Pub."},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of DVCon'05","author":"Havlicek John","year":"2005","unstructured":"John Havlicek and Yaron Wolfsthal . 2005 . PSL and SVA: Two standard assertion languages addressing complementary engineering needs . In Proceedings of DVCon'05 . John Havlicek and Yaron Wolfsthal. 2005. PSL and SVA: Two standard assertion languages addressing complementary engineering needs. In Proceedings of DVCon'05."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1278480.1278500"},{"volume-title":"Proceedings of DATE'06","author":"Morin-Allory K.","key":"e_1_2_1_19_1","unstructured":"K. Morin-Allory and D. Borrione . 2006. Proven correct monitors from PSL specifications . In Proceedings of DATE'06 . K. Morin-Allory and D. Borrione. 2006. Proven correct monitors from PSL specifications. In Proceedings of DATE'06."},{"key":"e_1_2_1_20_1","unstructured":"D. Pidan and S. Ruah. 2009. Design verification using directives having local variables (Patent US 2009\/0216513 A1).  D. Pidan and S. Ruah. 2009. Design verification using directives having local variables (Patent US 2009\/0216513 A1)."},{"volume-title":"Proceedings of MEMOCODE'10","author":"Pierre L.","key":"e_1_2_1_21_1","unstructured":"L. Pierre and L. Ferro . 2010. Enhancing the assertion-based verification of TLM designs with reentrancy . In Proceedings of MEMOCODE'10 . L. Pierre and L. Ferro. 2010. Enhancing the assertion-based verification of TLM designs with reentrancy. In Proceedings of MEMOCODE'10."},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"L. Pierre and L. Ferro. 2011. Dynamic verification of SystemC transactional models (Chapter 22). In Model-Based Testing for Embedded Systems. CRC Press. http:\/\/www-tima.imag.fr\/vds\/Isis\/.  L. Pierre and L. Ferro. 2011. Dynamic verification of SystemC transactional models (Chapter 22). In Model-Based Testing for Embedded Systems. CRC Press. http:\/\/www-tima.imag.fr\/vds\/Isis\/.","DOI":"10.1201\/b11321-23"},{"volume-title":"Proceedings of the IEEE International Symposium on Industrial Embedded Systems (SIES'12)","author":"Pierre L.","key":"e_1_2_1_23_1","unstructured":"L. Pierre , L. Ferro , Z. Bel Hadj Amor, P Bourgon, and J. Qu\u00e9vremont. 2012. Integrating PSL properties into SystemC transactional modeling: Application to the verification of a modem SoC . In Proceedings of the IEEE International Symposium on Industrial Embedded Systems (SIES'12) . L. Pierre, L. Ferro, Z. Bel Hadj Amor, P Bourgon, and J. Qu\u00e9vremont. 2012. Integrating PSL properties into SystemC transactional modeling: Application to the verification of a modem SoC. In Proceedings of the IEEE International Symposium on Industrial Embedded Systems (SIES'12)."},{"volume-title":"IEEE Standard for Property Specification Language (PSL)","author":"PSL.","key":"e_1_2_1_24_1","unstructured":"PSL. 2005. IEEE Std 1850--2005 , IEEE Standard for Property Specification Language (PSL) . IEEE. PSL. 2005. IEEE Std 1850--2005, IEEE Standard for Property Specification Language (PSL). IEEE."},{"volume-title":"IEEE Standard for Property Specification Language (PSL)","author":"PSL.","key":"e_1_2_1_25_1","unstructured":"PSL. 2010. IEEE Std 1850--2010 , IEEE Standard for Property Specification Language (PSL) . IEEE. PSL. 2010. IEEE Std 1850--2010, IEEE Standard for Property Specification Language (PSL). IEEE."},{"volume-title":"IEEE Standard for System Verilog: Unified Hardware Design, Specification and Verification Language","author":"SVA.","key":"e_1_2_1_26_1","unstructured":"SVA. 2005. IEEE Std 1800--2005 , IEEE Standard for System Verilog: Unified Hardware Design, Specification and Verification Language . IEEE. SVA. 2005. IEEE Std 1800--2005, IEEE Standard for System Verilog: Unified Hardware Design, Specification and Verification Language. IEEE."},{"volume-title":"IEEE Standard for System Verilog: Unified Hardware Design, Specification and Verification Language","author":"SVA.","key":"e_1_2_1_27_1","unstructured":"SVA. 2009. IEEE Std 1800--2009 , IEEE Standard for System Verilog: Unified Hardware Design, Specification and Verification Language . IEEE. SVA. 2009. IEEE Std 1800--2009, IEEE Standard for System Verilog: Unified Hardware Design, Specification and Verification Language. IEEE."},{"volume-title":"IEEE Standard System C Language Reference Manual","author":"C.","key":"e_1_2_1_28_1","unstructured":"System C. 2011. IEEE Std 1666--2011 , IEEE Standard System C Language Reference Manual . IEEE. SystemC. 2011. IEEE Std 1666--2011, IEEE Standard System C Language Reference Manual. IEEE."},{"volume-title":"Proceedings of MEMOCODE'10","author":"Tabakov D.","key":"e_1_2_1_29_1","unstructured":"D. Tabakov and M. Vardi . 2010. Monitoring temporal SystemC Properties . In Proceedings of MEMOCODE'10 . D. Tabakov and M. Vardi. 2010. Monitoring temporal SystemC Properties. In Proceedings of MEMOCODE'10."}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2811260","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2811260","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:49Z","timestamp":1750225729000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2811260"}},"subtitle":["Semantic and Practical Analysis for System-Level Requirements"],"short-title":[],"issued":{"date-parts":[[2016,1,28]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,1,28]]}},"alternative-id":["10.1145\/2811260"],"URL":"https:\/\/doi.org\/10.1145\/2811260","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2016,1,28]]},"assertion":[{"value":"2015-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-01-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}