{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:48:50Z","timestamp":1759146530495},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,3,20]],"date-time":"2015-03-20T00:00:00Z","timestamp":1426809600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Electron Test"],"published-print":{"date-parts":[[2015,4]]},"DOI":"10.1007\/s10836-015-5514-8","type":"journal-article","created":{"date-parts":[[2015,3,18]],"date-time":"2015-03-18T22:44:34Z","timestamp":1426718674000},"page":"167-180","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Reusing RTL Assertion Checkers for Verification of SystemC TLM Models"],"prefix":"10.1007","volume":"31","author":[{"given":"Nicola","family":"Bombieri","sequence":"first","affiliation":[]},{"given":"Franco","family":"Fummi","sequence":"additional","affiliation":[]},{"given":"Valerio","family":"Guarnieri","sequence":"additional","affiliation":[]},{"given":"Graziano","family":"Pravadelli","sequence":"additional","affiliation":[]},{"given":"Francesco","family":"Stefanni","sequence":"additional","affiliation":[]},{"given":"Tara","family":"Ghasempouri","sequence":"additional","affiliation":[]},{"given":"Michele","family":"Lora","sequence":"additional","affiliation":[]},{"given":"Giovanni","family":"Auditore","sequence":"additional","affiliation":[]},{"given":"Mirella Negro","family":"Marcigaglia","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,3,20]]},"reference":[{"key":"5514_CR1","doi-asserted-by":"crossref","unstructured":"Abarbanel Y, Beer I, Glushovsky L, Keidar S, Wolfsthal Y (2000) FoCs: automatic generation of simulation checkers from formal specifications. In: Proceedings of CAV, pp 538\u2013 542","DOI":"10.1007\/10722167_40"},{"key":"5514_CR2","unstructured":"Accellera (2004) Property specification language reference manual. http:\/\/www.accellera.org"},{"key":"5514_CR3","doi-asserted-by":"crossref","unstructured":"Bombieri N, Deganello N, Fummi F (2008) Integrating RTL IPs into TLM designs through automatic transactor generation. In: Proceedings of ACM\/IEEE DATE, pp 15\u201320","DOI":"10.1109\/DATE.2008.4484653"},{"key":"5514_CR4","doi-asserted-by":"crossref","unstructured":"Bombieri N, Fummi F, Pravadelli G (2006) On the evaluation of transactor-based verification for reusing TLM assertions and testbenches at RTL. In: Proceedings of ACM\/IEEE DATE,pp 1\u20136","DOI":"10.1109\/DATE.2006.243898"},{"key":"5514_CR5","doi-asserted-by":"crossref","unstructured":"Bombieri N, Fummi F, Pravadelli G (2007) Incremental ABV for functional validation of TL-to-RTL design refinement. In: Proceedings of ACM\/IEEE DATE, pp 882\u2013 887","DOI":"10.1109\/DATE.2007.364404"},{"issue":"12","key":"5514_CR6","doi-asserted-by":"crossref","first-page":"1730","DOI":"10.1109\/TC.2010.187","volume":"60","author":"N Bombieri","year":"2011","unstructured":"Bombieri N, Fummi F, Pravadelli G (2011) Automatic abstraction of RTL IPs into equivalent TLM descriptions. IEEE Trans Comput 60(12):1730\u20131743","journal-title":"IEEE Trans Comput"},{"issue":"2","key":"5514_CR7","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1109\/MDT.2007.48","volume":"24","author":"N Bombieri","year":"2007","unstructured":"Bombieri N, Fummi F, Pravadelli G, Fedeli A (2007) Hybrid, incremental assertion-based verification for TLM design flows. IEEE Design and Test 24(2):140\u2013152","journal-title":"IEEE Design and Test"},{"key":"5514_CR8","doi-asserted-by":"crossref","unstructured":"Bombieri N, Fummi F, Pravadelli G, Marques-Silva J (2007) Towards Equivalence Checking Between TLM and RTL Models. In: Proceedings of ACM\/IEEE MEMOCODE, pp 113\u2013 122","DOI":"10.1109\/MEMCOD.2007.371236"},{"key":"5514_CR9","doi-asserted-by":"crossref","unstructured":"Boul\u00e9 M, Zilic Z (2008) Generating hardware assertion checkers: for hardware verification, emulation, post-fabrication debugging and on-line monitoring. Springer","DOI":"10.1007\/978-1-4020-8586-4"},{"key":"5514_CR10","doi-asserted-by":"crossref","unstructured":"Cai L, Gajski D (2003) Transaction Level Modelling: An Overview. In: IEEE\/ACM CODES+ISSS, pp 19\u201324","DOI":"10.1145\/944645.944651"},{"key":"5514_CR11","unstructured":"Carbon Design Systems Carbon Model Studio. http:\/\/carbondesignsystems.com\/"},{"key":"5514_CR12","doi-asserted-by":"crossref","unstructured":"Chen M, Mishra P (2013) Assertion-based functional consistency checking between TLM and RTL models. In: Proceedings of IEEE VLSID, pp 320\u2013325","DOI":"10.1109\/VLSID.2013.208"},{"key":"5514_CR13","doi-asserted-by":"crossref","unstructured":"Clarke E M, Emerson E A, Sifakis J (2009) Model checking: algorithmic verification and debugging. Commun ACM 52(11)","DOI":"10.1145\/1592761.1592781"},{"issue":"4","key":"5514_CR14","first-page":"792","volume":"41","author":"S Das","year":"2006","unstructured":"Das S, Roberts D, Lee S, Pant S, Blaauw D, Austin T, Flautner K, Mudge T (2006). A self-tuning DVS processor using delay-error detection and correction 41(4):792\u2013 804","journal-title":"A self-tuning DVS processor using delay-error detection and correction"},{"key":"5514_CR15","doi-asserted-by":"crossref","unstructured":"Ecker W, Esen V, Hull M (2007) Implementation of a transaction level assertion framework in SystemC. In: Proceedings of IEEE\/ACM DATE pp 894\u2013899","DOI":"10.1109\/DATE.2007.364406"},{"key":"5514_CR16","doi-asserted-by":"crossref","unstructured":"Ecker W, Esen V, Hull M (2006) Execution semantics and formalism for multi-abstraction TLM assertions, pp 93\u2013102","DOI":"10.1109\/MEMCOD.2006.1695910"},{"key":"5514_CR17","doi-asserted-by":"crossref","unstructured":"Ecker W, Esen V, Hull M (2006) Requirements and concepts for transaction level assertions. In: Proceedings of IEEE ICCD, pp 286\u2013293","DOI":"10.1109\/ICCD.2006.4380830"},{"key":"5514_CR18","doi-asserted-by":"crossref","unstructured":"Ecker W, Esen V, Steininger T, Velten M, Hull M (2006) Specification Language for Transaction Level Assertions. In: Proceedings of IEEE HLDVT, pp 77\u201384","DOI":"10.1109\/HLDVT.2006.319967"},{"key":"5514_CR19","unstructured":"EDALab HIFSuite. http:\/\/www.hifsuite.com\/"},{"key":"5514_CR20","doi-asserted-by":"crossref","unstructured":"Ferro L, Pierre L, Ledru Y, du Bousquet L (2008) Generation of test programs for the assertion-based verification of TLM models. In: Proceedings of IEEE IDT, pp 237\u2013242","DOI":"10.1109\/IDT.2008.4802505"},{"key":"5514_CR21","doi-asserted-by":"crossref","unstructured":"Ferro L, Pierre L (2010) Formal semantics for PSL modelling layer and application to the verification of transactional models. In: Proceedings of ACM\/IEEE DATE, pp 1207\u2013 1212","DOI":"10.1109\/DATE.2010.5456991"},{"key":"5514_CR22","unstructured":"Ferro L, Laurence (2009) ISIS: runtime verification of TLM platforms. In: Proceedings of FDL, pp 1\u20136"},{"key":"5514_CR23","doi-asserted-by":"crossref","unstructured":"Fujita M (2005) Equivalence checking between behavioral and RTL descriptions with virtual controllers and datapaths. ACM TODAES 10(4):610\u2013626","DOI":"10.1145\/1109118.1109121"},{"key":"5514_CR24","doi-asserted-by":"crossref","unstructured":"Ghofrani A, Javahery F, Navabi Z (2010) Assertion based verification in TLM. In: Proceedings of IEEE EWDTS, pp 509\u2013 513","DOI":"10.1109\/EWDTS.2010.5742077"},{"key":"5514_CR25","doi-asserted-by":"crossref","unstructured":"Grosse D, Le H, Drechsler R (2010) Proving transaction and system-level properties of untimed SystemC TLM designs. In: Proceedings of IEEE\/ACM MEMOCODE, pp 113\u2013 122","DOI":"10.1109\/MEMCOD.2010.5558643"},{"issue":"1","key":"5514_CR26","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1109\/TVLSI.2005.863187","volume":"14","author":"A Habibi","year":"2006","unstructured":"Habibi A, Tahar S (2006) Design and verification of SystemC transaction-level models. IEEE Trans VLSI Syst 14(1):57\u201367","journal-title":"IEEE Trans VLSI Syst"},{"key":"5514_CR27","unstructured":"IBM FoCs property checkers generator. https:\/\/www.research.ibm.com\/haifa\/projects\/verification\/focs\/start.html"},{"key":"5514_CR28","unstructured":"IEEE standard systemC language reference manual (2006). http:\/\/ieeexplore.ieee.org"},{"key":"5514_CR29","doi-asserted-by":"crossref","unstructured":"Kallel M, Lahbib Y, Tourki R, Baganne A (2009) Aspect-based ABV for SystemC transaction level models. In: Proceedings of IEEE ICM, pp 304\u2013307","DOI":"10.1109\/ICM.2009.5418623"},{"key":"5514_CR30","doi-asserted-by":"crossref","unstructured":"Kallel M, Lahbib Y, Tourki R, Baganne A (2010) Verification of SystemC transaction level models using an aspect-oriented and generic approach. In: Proceedings of IEEE DTIS, pp 1\u20136","DOI":"10.1109\/DTIS.2010.5487605"},{"key":"5514_CR31","doi-asserted-by":"crossref","unstructured":"Kasuya A, Tesfaye T (2007) Verification methodologies in a TLM-to-RTL design flow. In: Proceedings of ACM\/IEEE DAC, pp 199\u2013204","DOI":"10.1109\/DAC.2007.375152"},{"issue":"4-5","key":"5514_CR32","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1016\/j.compeleceng.2005.04.001","volume":"31","author":"Y Lahbib","year":"2005","unstructured":"Lahbib Y, Kamdem R, Benalycherif M-l, Tourki R (2005) An automatic ABV methodology enabling PSL assertions across SLD flow for SOCs modelled in SystemC. Comput Electr Eng 31(4-5):282\u2013302","journal-title":"Comput Electr Eng"},{"key":"5514_CR33","doi-asserted-by":"crossref","unstructured":"Lahbib Y, Ghrab M-A, Hechkel M, Ghenassia F, Tourki R (2006) A new synchronization policy between PSL checkers and SystemC designs at transaction level. In: Proceedings of IEEE DTIS, pp 85\u201390","DOI":"10.1109\/DTIS.2006.1708698"},{"key":"5514_CR34","doi-asserted-by":"crossref","unstructured":"Mathur A, Krishnaswamy V (2007) Design for Verification in System-level Models and RTL. In: Proceedings of IEEE\/ACM DAC, pp 193\u2013198","DOI":"10.1109\/DAC.2007.375151"},{"key":"5514_CR35","doi-asserted-by":"crossref","unstructured":"Pierre L, Amor ZBH (2013) Automatic refinement of requirements for verification throughout the SoC design flow. In: Proceedings of ACM\/IEEE CODES+ISSS, pp 1\u201310","DOI":"10.1109\/CODES-ISSS.2013.6659016"},{"issue":"10","key":"5514_CR36","doi-asserted-by":"crossref","first-page":"1346","DOI":"10.1109\/TC.2008.74","volume":"57","author":"L Pierre","year":"2008","unstructured":"Pierre L, Ferro L (2008) A Tractable and Fast Method for Monitoring SystemC TLM Specifications. IEEE Trans Comput 57(10):1346\u20131356","journal-title":"IEEE Trans Comput"},{"key":"5514_CR37","doi-asserted-by":"crossref","unstructured":"Pierre L, Ferro L (2010) Enhancing the assertion-based verification of TLM designs with reentrancy. In: Proceedings of ACM\/IEEE MEMOCODE, pp 103\u2013112","DOI":"10.1109\/MEMCOD.2010.5558642"},{"key":"5514_CR38","doi-asserted-by":"crossref","unstructured":"Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: FM 2006: formal methods. Springer, pp 573\u2013586","DOI":"10.1007\/11813040_38"},{"key":"5514_CR39","doi-asserted-by":"crossref","unstructured":"Smith DJ (1996) VHDL & Verilog compared & contrasted - plus modelled example written in VHDL, Verilog and C. In: Proceedings of ACM\/IEEE DAC, pp 771\u2013 776","DOI":"10.1145\/240518.240664"},{"key":"5514_CR40","unstructured":"Xiong Z, Bian J, Zhao Y (2010) An assertion-based verification method for SystemC TLM. In: Proceedings of IEEE ICCCAS, pp 842\u2013846"}],"container-title":["Journal of Electronic Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-015-5514-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10836-015-5514-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-015-5514-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:04:47Z","timestamp":1559253887000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10836-015-5514-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,20]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,4]]}},"alternative-id":["5514"],"URL":"https:\/\/doi.org\/10.1007\/s10836-015-5514-8","relation":{},"ISSN":["0923-8174","1573-0727"],"issn-type":[{"value":"0923-8174","type":"print"},{"value":"1573-0727","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,20]]}}}