{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T15:54:51Z","timestamp":1791302091407,"version":"4.1.0"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032411594","type":"print"},{"value":"9783032411600","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T00:00:00Z","timestamp":1791331200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T00:00:00Z","timestamp":1791331200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2027]]},"DOI":"10.1007\/978-3-032-41160-0_21","type":"book-chapter","created":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T15:01:56Z","timestamp":1791298916000},"page":"330-350","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Periscope: Extending the\u00a0Scope of\u00a0Pre-silicon Assertion-Based Verification with\u00a0Runtime Monitor Feedback"],"prefix":"10.1007","author":[{"given":"Tommy","family":"Tracy II","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yasas","family":"Seneviratne","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kumaresh","family":"Nandagopal","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Deebakkarthi","family":"Chinnasame Rani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew","family":"Dwyer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Brad","family":"Bingham","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kevin","family":"Skadron","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,10,7]]},"reference":[{"key":"21_CR1","unstructured":"Advanced Micro Devices, Inc.: AMD Alveo U250 Data Center Accelerator Card. https:\/\/www.amd.com\/en\/products\/accelerators\/alveo\/u250\/a-u250-a64g-pq-g.html"},{"key":"21_CR2","unstructured":"AMD: Vivado Design Suite User Guide (2022). https:\/\/www.amd.com, version 2022.1"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Bai, Y., Hamad, G.B., Suhaib, S., Ren, H.: Assertionforge: Enhancing formal verification assertion generation with structured representation of specifications and RTL. In: 2025 IEEE Int. Conference on LLM-Aided Design (ICLAD, pp. 85\u201392. IEEE (2025)","DOI":"10.1109\/ICLAD65226.2025.00009"},{"key":"21_CR4","unstructured":"Balkind, J., et al.: OpenPiton research platform. https:\/\/github.com\/PrincetonUniversity\/openpiton. Accessed 11 Sept 2019"},{"key":"21_CR5","unstructured":"Bienia, C.: Benchmarking Modern Multiprocessors, Princeton University (2011). Ph.D. thesis"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Bosio, A., Germiniani, S., Pravadelli, G., Traiola, M.: Exploiting assertions mining and fault analysis to guide RTL-level approximation. In: 2023 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp.\u00a01\u20132. IEEE (2023)","DOI":"10.23919\/DATE56975.2023.10136949"},{"key":"21_CR7","doi-asserted-by":"publisher","unstructured":"Boul\u00e9, M., Zilic, Z.: Generating Hardware Assertion Checkers. Springer Netherlands, Dordrecht (2008). https:\/\/doi.org\/10.1007\/978-1-4020-8586-4, http:\/\/link.springer.com\/10.1007\/978-1-4020-8586-4","DOI":"10.1007\/978-1-4020-8586-4"},{"key":"21_CR8","unstructured":"Cadence Design Systems, Inc.: Jasper RTL Apps. https:\/\/www.cadence.com\/en_US\/home\/tools\/system-design-and-verification\/formal-and-static-verification\/jasper-verification-platform.html, cadence Jasper RTL Apps page; describes integration of JasperGold technology"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Che, S., Sheaffer, J.W., Boyer, M., Szafaryn, L.G., Wang, L., Skadron, K.: A characterization of the Rodinia benchmark suite with comparison to contemporary CMP workloads. In: IEEE International Symposium on Workload Characterization (IISWC\u201910), pp. 1\u201311. IEEE (2010)","DOI":"10.1109\/IISWC.2010.5650274"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Chen, J., Bai, Y., Hao, D., Zhang, L., Zhang, L., Xie, B.: How do assertions impact coverage-based test-suite reduction? In: 2017 IEEE International Conference on Software Testing, Verification and Validation (ICST), pp. 418\u2013423. IEEE (2017)","DOI":"10.1109\/ICST.2017.45"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Danese, A., Bertacco, V., Pravadelli, G.: Symbolic assertion mining for security validation. In: 2018 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 1550\u20131555. IEEE (2018)","DOI":"10.23919\/DATE.2018.8342262"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Danese, A., Riva, N.D., Pravadelli, G.: A-team: Automatic template-based assertion miner. In: Proceedings of the 54th Annual Design Automation Conference 2017, pp.\u00a01\u20136 (2017)","DOI":"10.1145\/3061639.3062206"},{"issue":"23","key":"21_CR13","doi-asserted-by":"publisher","first-page":"4745","DOI":"10.3390\/electronics14234745","volume":"14","author":"MO Faruque","year":"2025","unstructured":"Faruque, M.O., Jamieson, P., Patooghy, A., Badawy, A.H.A.: Unleashing ghost: an LLM-powered framework for automated hardware trojan design. Electronics 14(23), 4745 (2025)","journal-title":"Electronics"},{"key":"21_CR14","doi-asserted-by":"publisher","unstructured":"Fey, G., Drechsler, R.: Robustness and usability in modern design flows. Springer Netherlands (2008). https:\/\/doi.org\/10.1007\/978-1-4020-6536-1","DOI":"10.1007\/978-1-4020-6536-1"},{"key":"21_CR15","unstructured":"Foster, H., Siemens, E.: Wilson research group functional verification study 2020. Retrieved on June 4, \u00a02026 (2020)"},{"key":"21_CR16","unstructured":"Foster, H., Siemens, E.: 2024 Wilson Research Group FPGA functional verification trend report. Retrieved on June 4, \u00a02026 (2024)"},{"issue":"2","key":"21_CR17","first-page":"728","volume":"10","author":"S Germiniani","year":"2020","unstructured":"Germiniani, S., Danese, A., Pravadelli, G.: Automatic generation of assertions for detection of firmware vulnerabilities through alignment of symbolic sequences. IEEE Trans. Emerg. Top. Comput. 10(2), 728\u2013739 (2020)","journal-title":"IEEE Trans. Emerg. Top. Comput."},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Germiniani, S., Nicoletti, D., Pravadelli, G.: Invited talk: Pros and cons of assertion mining. In: 2024 IEEE 25th Latin American Test Symposium (LATS), pp. 1\u20132. IEEE (2024)","DOI":"10.1109\/LATS62223.2024.10534611"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Germiniani, S., Nicoletti, D., Pravadelli, G.: A baseline framework for the qualification of LTL specification miners. In: 2025 Design, Automation & Test in Europe Conference (DATE), pp.\u00a01\u20137. IEEE (2025)","DOI":"10.23919\/DATE64628.2025.10992993"},{"issue":"11","key":"21_CR20","doi-asserted-by":"publisher","first-page":"4277","DOI":"10.1109\/TCAD.2022.3197525","volume":"41","author":"S Germiniani","year":"2022","unstructured":"Germiniani, S., Pravadelli, G.: Harm: a hint-based assertion miner. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(11), 4277\u20134288 (2022)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"21_CR21","doi-asserted-by":"publisher","unstructured":"Hangal, S., Narayanan, S., Chandra, N., Chakravorty, S.: IODINE: a tool to automatically infer dynamic invariants for hardware designs. In: Proceedings. 42nd Design Automation Conference, 2005. pp. 775\u2013778 (Jun 2005). https:\/\/doi.org\/10.1109\/DAC.2005.193920, https:\/\/ieeexplore.ieee.org\/document\/1510440\/, iSSN: 0738-100X","DOI":"10.1109\/DAC.2005.193920"},{"issue":"6","key":"21_CR22","doi-asserted-by":"publisher","first-page":"952","DOI":"10.1109\/TCAD.2013.2241176","volume":"32","author":"S Hertz","year":"2013","unstructured":"Hertz, S., Sheridan, D., Vasudevan, S.: Mining hardware assertions with guidance from static analysis. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 32(6), 952\u2013965 (2013)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Iman, M.R.H., Jervan, G., Ghasempouri, T.: ARTmine: Automatic association rule mining with temporal behavior for hardware verification. In: 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp.\u00a01\u20136. IEEE (2024)","DOI":"10.23919\/DATE58400.2024.10546742"},{"key":"21_CR24","doi-asserted-by":"publisher","unstructured":"Jenihhin, M., Raik, J., Ubar, R., Chepurov, A.: On reusability of verification assertions for testing. In: 2008 11th International Biennial Baltic Electronics Conference, pp. 151\u2013154 (Oct 2008). https:\/\/doi.org\/10.1109\/BEC.2008.4657501, https:\/\/ieeexplore.ieee.org\/document\/4657501\/, iSSN: 2382-820X","DOI":"10.1109\/BEC.2008.4657501"},{"key":"21_CR25","unstructured":"Keng, B., Veneris, A.: Automated debugging of missing input constraints in a formal verification environment. Formal Methods Comput.-Aided Design (FMCAD), 101\u2013105 (2012) IEEE"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Lemieux, C., Park, D., Beschastnikh, I.: General LTL specification mining (T). In: 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 81\u201392. IEEE (2015)","DOI":"10.1109\/ASE.2015.71"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"Lustig, D., Pellauer, M., Martonosi, M.: PipeCheck: Specifying and verifying microarchitectural enforcement of memory consistency models. In: 47th Annual IEEE\/ACM International Symposium on Microarchitecture, pp. 635\u2013646. IEEE (2014)","DOI":"10.1109\/MICRO.2014.38"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Mali, B., Maddala, K., Gupta, V., Reddy, S., Karfa, C., Karri, R.: Chiraag: Chatgpt informed rapid and automated assertion generation. In: 2024 IEEE Computer Society Annual Symposium on VLSI (ISVLSI), pp. 680\u2013683. IEEE (2024)","DOI":"10.1109\/ISVLSI61997.2024.00130"},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"Manerkar, Y.A., Lustig, D., Martonosi, M., Pellauer, M.: RTLCheck: Verifying the memory consistency of RTL designs. In: Proceedings of the 50th Annual IEEE\/ACM International Symposium on Microarchitecture, pp. 463\u2013476 (2017)","DOI":"10.1145\/3123939.3124536"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Orenes-Vera, M., Manocha, A., Wentzlaff, D., Martonosi, M.: Autosva: Democratizing formal verification of RTL module interactions. In: 2021 58th ACM\/IEEE Design Automation Conference (DAC), pp. 535\u2013540. IEEE (2021)","DOI":"10.1109\/DAC18074.2021.9586118"},{"key":"21_CR31","unstructured":"Richard M.: Stallman and the GCC Developer Community: Using the GNU Compiler Collection. Free Software Foundation. https:\/\/gcc.gnu.org\/onlinedocs\/gcc\/, gCC manual"},{"issue":"6","key":"21_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3696108","volume":"29","author":"S Sanjaya","year":"2024","unstructured":"Sanjaya, S., Witharana, H., Mishra, P.: Assertion-based validation using clustering and dynamic refinement of hardware checkers. ACM Trans. Design Autom. Electron. Syst. 29(6), 1\u201322 (2024)","journal-title":"ACM Trans. Design Autom. Electron. Syst."},{"key":"21_CR33","unstructured":"Snyder, W., Wasson, P., Galbi, D., Lore, G., et al: Verilator. https:\/\/github.com\/verilator\/verilator"},{"key":"21_CR34","doi-asserted-by":"publisher","unstructured":"Tracy, T., Tabajara, L.M., Vardi, M., Skadron, K.: Runtime Verification on FPGAs with LTLf Specifications. In: 2020 Formal Methods in Computer Aided Design (FMCAD). pp. 36\u201346 (2020).https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_10","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_10"},{"key":"21_CR35","doi-asserted-by":"crossref","unstructured":"Trippel, C.: Specification and formal verification of hardware-software contracts for high-assurance computer architectures. Computer 58(8), 86\u201391 (Aug2025)","DOI":"10.1109\/MC.2025.3573841"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Trippel, C., Lustig, D., Martonosi, M.: Checkmate: automated synthesis of hardware exploits and security litmus tests. In: 51st Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO), pp. 947\u2013960. IEEE (2018)","DOI":"10.1109\/MICRO.2018.00081"},{"key":"21_CR37","doi-asserted-by":"crossref","unstructured":"Vasudevan, S., Sheridan, D., Patel, S., Tcheng, D., Tuohy, B., Johnson, D.: Goldmine: Automatic assertion generation using data mining and static analysis. In: 2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010), pp. 626\u2013629. IEEE (2010)","DOI":"10.1109\/DATE.2010.5457129"},{"key":"21_CR38","doi-asserted-by":"publisher","unstructured":"Wang, L.C., Abadir, M., Krishnamurthy, N.: Automatic generation of assertions for formal verification of PowerPC\/sup TM \/microprocessor arrays using symbolic trajectory evaluation. In: Proceedings 1998 Design and Automation Conference. 35th DAC. (Cat. No.98CH36175), pp. 534\u2013537. DAC-98, IEEE (1998). https:\/\/doi.org\/10.1109\/dac.1998.724529, http:\/\/dx.doi.org\/10.1109\/DAC.1998.724529","DOI":"10.1109\/dac.1998.724529"},{"key":"21_CR39","unstructured":"Waterman, A., Asanov\u00edc, K.: The RISC-V Instruction Set Manual, Volume II: Privileged Architecture. Tech. rep., RISC-V Foundation (2017). https:\/\/docs.riscv.org\/reference\/isa\/v1.10\/_attachments\/riscv-privileged.pdf"},{"key":"21_CR40","unstructured":"Waterman, A., Asanov\u00edc, K.: The RISC-V Instruction Set Manual, Volume I: User-Level ISA. Tech. rep., RISC-V Foundation (2019). https:\/\/docs.riscv.org\/reference\/isa\/v20191213\/_attachments\/riscv-unprivileged.pdf, user-Level ISA Version 2.3"},{"issue":"1","key":"21_CR41","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3565801","volume":"19","author":"H Witharana","year":"2023","unstructured":"Witharana, H., Jayasena, A., Whigham, A., Mishra, P.: Automated generation of security assertions for RTL models. ACM J. Emerg. Technol. Comput. Syst. 19(1), 1\u201327 (2023)","journal-title":"ACM J. Emerg. Technol. Comput. Syst."},{"issue":"11s","key":"21_CR42","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3510578","volume":"54","author":"H Witharana","year":"2022","unstructured":"Witharana, H., Lyu, Y., Charles, S., Mishra, P.: A survey on assertion-based hardware verification. ACM Comput. Surv. (CSUR) 54(11s), 1\u201333 (2022)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"21_CR43","doi-asserted-by":"crossref","unstructured":"Wu, X., et al.: Shift-left techniques in electronic design automation: a survey. ACM Comput. Surv. (2025)","DOI":"10.1145\/3819588"},{"key":"21_CR44","doi-asserted-by":"crossref","unstructured":"Xie, T., Notkin, D.: Mutually enhancing test generation and specification inference. In: International Workshop on Formal Approaches to Software Testing, pp. 60\u201369. Springer (2003)","DOI":"10.1007\/978-3-540-24617-6_5"},{"key":"21_CR45","doi-asserted-by":"crossref","unstructured":"Yan, Z., Fang, W., Li, M., Li, M., Liu, S., Xie, Z., Zhang, H.: AssertLLM: Generating hardware verification assertions from design specifications via multi-LLMs. In: Proceedings of the 30th Asia and South Pacific Design Automation Conference, pp. 614\u2013621 (2025)","DOI":"10.1145\/3658617.3697756"},{"key":"21_CR46","doi-asserted-by":"crossref","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 283\u2013294 (2011)","DOI":"10.1145\/1993498.1993532"},{"key":"21_CR47","doi-asserted-by":"publisher","unstructured":"Zaruba, F., Benini, L.: The cost of application-class processing: energy and performance analysis of a Linux-Ready 1.7-GHz 64-Bit RISC-V Core in 22-nm FDSOI technology. IEEE Trans. Very Large Scale Integr. (VLSI) Syst. 27(11), 2629\u20132640 (Nov 2019). https:\/\/doi.org\/10.1109\/TVLSI.2019.2926114","DOI":"10.1109\/TVLSI.2019.2926114"},{"key":"21_CR48","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Mesbah, A.: Assertions are strongly correlated with test suite effectiveness. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pp. 214\u2013224 (2015)","DOI":"10.1145\/2786805.2786858"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-41160-0_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T15:02:04Z","timestamp":1791298924000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-41160-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,10,7]]},"ISBN":["9783032411594","9783032411600"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-41160-0_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,10,7]]},"assertion":[{"value":"7 October 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Runtime Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kingston","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 October 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 October 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rv2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rv2026.smithengineering.queensu.ca\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}