{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,17]],"date-time":"2025-12-17T08:43:38Z","timestamp":1765961018502,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":53,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,10,14]],"date-time":"2017-10-14T00:00:00Z","timestamp":1507939200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","award":["HR0011-13-3-0002"],"award-info":[{"award-number":["HR0011-13-3-0002"]}],"id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1117147"],"award-info":[{"award-number":["CCF-1117147"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,10,14]]},"DOI":"10.1145\/3123939.3124536","type":"proceedings-article","created":{"date-parts":[[2017,11,20]],"date-time":"2017-11-20T14:31:12Z","timestamp":1511188272000},"page":"463-476","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["RTLcheck"],"prefix":"10.1145","author":[{"given":"Yatin A.","family":"Manerkar","sequence":"first","affiliation":[{"name":"Princeton University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Lustig","sequence":"additional","affiliation":[{"name":"NVIDIA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Margaret","family":"Martonosi","sequence":"additional","affiliation":[{"name":"Princeton University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Pellauer","sequence":"additional","affiliation":[{"name":"NVIDIA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,10,14]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Jones","author":"Aagaard Mark","year":"2001","unstructured":"Mark Aagaard , Byron Cook , Nancy A. Day , and Robert B . Jones . 2001 . A Framework for Microprocessor Correctness Statements. In Correct Hardware Design and Verification Methods (CHARME) . 433--448. Mark Aagaard, Byron Cook, Nancy A. Day, and Robert B. Jones. 2001. A Framework for Microprocessor Correctness Statements. In Correct Hardware Design and Verification Methods (CHARME). 433--448."},{"key":"e_1_3_2_1_2_1","volume-title":"Third International Conference, FMCAD","author":"Aagaard Mark","year":"2000","unstructured":"Mark Aagaard , Robert B. Jones , Thomas F. Melham , John W. O'Leary , and Carl-Johan H. Seger . 2000. A Methodology for Large-Scale Hardware Verification. In Formal Methods in Computer-Aided Design , Third International Conference, FMCAD 2000 . 263--282. Mark Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, and Carl-Johan H. Seger. 2000. A Methodology for Large-Scale Hardware Verification. In Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000. 263--282."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694391"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_1_5_1","unstructured":"ARM. 2011. Cortex-A9 MPCore programmer advice notice read-after-read hazards. ARM Reference 761319. (2011). http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.uan0004a\/UAN0004A_a9_read_read.pdf. ARM. 2011. Cortex-A9 MPCore programmer advice notice read-after-read hazards. ARM Reference 761319. (2011). http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.uan0004a\/UAN0004A_a9_read_read.pdf."},{"key":"e_1_3_2_1_6_1","unstructured":"ARM. 2017. ARM Architecture Reference Manual ARMv8 for ARMv8-A architecture profile. (2017). https:\/\/static.docs.arm.com\/ddi0487\/b\/DDI0487B_a_armv8_arm.pdf ARM. 2017. ARM Architecture Reference Manual ARMv8 for ARMv8-A architecture profile. (2017). https:\/\/static.docs.arm.com\/ddi0487\/b\/DDI0487B_a_armv8_arm.pdf"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103717"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1555754.1555785"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062353"},{"key":"e_1_3_2_1_12_1","unstructured":"Cadence Design Systems Inc. 2015. JasperGold Apps User's Guide. (2015). Cadence Design Systems Inc. 2015. JasperGold Apps User's Guide. (2015)."},{"key":"e_1_3_2_1_13_1","unstructured":"Cadence Design Systems Inc. 2016. JasperGold Engine Selection Guide. (2016). Cadence Design Systems Inc. 2016. JasperGold Engine Selection Guide. (2016)."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-07139-8","volume-title":"SVA: The Power of Assertions in SystemVerilog","author":"Cerny Eduard","year":"2015","unstructured":"Eduard Cerny , Surrendra Dudani , John Havlicek , Dmitry Korchemny , 2015 . SVA: The Power of Assertions in SystemVerilog . Springer . Eduard Cerny, Surrendra Dudani, John Havlicek, Dmitry Korchemny, et al. 2015. SVA: The Power of Assertions in SystemVerilog. Springer."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250662.1250697"},{"key":"e_1_3_2_1_16_1","unstructured":"comododragon. 2016. Stores are not working. (2016). https:\/\/github.com\/ucb-bar\/vscale\/issues\/13. comododragon. 2016. Stores are not working. (2016). https:\/\/github.com\/ucb-bar\/vscale\/issues\/13."},{"key":"e_1_3_2_1_17_1","unstructured":"The Coq development team. 2004. The Coq proof assistant reference manual version 8.0. LogiCal Project. http:\/\/coq.inria.fr The Coq development team. 2004. The Coq proof assistant reference manual version 8.0. LogiCal Project. http:\/\/coq.inria.fr"},{"key":"e_1_3_2_1_18_1","unstructured":"The diy development team. 2012. A don't (diy) tutorial version 5.01. http:\/\/diy.inria.fr\/doc\/index.html The diy development team. 2012. A don't (diy) tutorial version 5.01. http:\/\/diy.inria.fr\/doc\/index.html"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2744921"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830775"},{"volume-title":"Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures. In 2016 IEEE Symposium on Security and Privacy (SP). 38--55","author":"Guanciale R.","key":"e_1_3_2_1_22_1","unstructured":"R. Guanciale , H. Nemati , C. Baumann , and M. Dam . 2016 . Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures. In 2016 IEEE Symposium on Security and Privacy (SP). 38--55 . R. Guanciale, H. Nemati, C. Baumann, and M. Dam. 2016. Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures. In 2016 IEEE Symposium on Security and Privacy (SP). 38--55."},{"key":"e_1_3_2_1_23_1","volume-title":"Broadwell CPUs.","author":"Hachman Mark","year":"2014","unstructured":"Mark Hachman . 2014. Intel finds specialized TSX enterprise bug on Haswell , Broadwell CPUs. ( 2014 ). http:\/\/www.pcworld.com\/article\/2464880\/intel-finds-specialized-tsx-enterprise-bug-on-haswell-broadwell-cpus.html. Mark Hachman. 2014. Intel finds specialized TSX enterprise bug on Haswell, Broadwell CPUs. (2014). http:\/\/www.pcworld.com\/article\/2464880\/intel-finds-specialized-tsx-enterprise-bug-on-haswell-broadwell-cpus.html."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/998680.1006710"},{"key":"e_1_3_2_1_25_1","unstructured":"IBM. 2013. Power ISA Version 2.07. (2013). IBM. 2013. Power ISA Version 2.07. (2013)."},{"key":"e_1_3_2_1_26_1","volume-title":"IEEE Standard for Property Specification Language (PSL)","author":"IEEE.","year":"1850","unstructured":"IEEE. 2010. IEEE Standard for Property Specification Language (PSL) . IEEE Std 1850 -2010 (Revision of IEEE Std 1850-2005) (April 2010). IEEE. 2010. IEEE Standard for Property Specification Language (PSL). IEEE Std 1850-2010 (Revision of IEEE Std1850-2005) (April 2010)."},{"key":"e_1_3_2_1_27_1","volume-title":"IEEE Standard for SystemVerilog-Unified Hardware Design, Specification, and Verification Language","author":"IEEE.","year":"1800","unstructured":"IEEE. 2013. IEEE Standard for SystemVerilog-Unified Hardware Design, Specification, and Verification Language . IEEE Std 1800 -2012 (Revision of IEEE Std 1800-2009) (Feb 2013), 1--1315. IEEE. 2013. IEEE Standard for SystemVerilog-Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800-2012 (Revision of IEEE Std 1800-2009) (Feb 2013), 1--1315."},{"key":"e_1_3_2_1_28_1","unstructured":"Intel. 2013. Intel 64 and IA-32 Architectures Software Developer's Manual. (2013). http:\/\/www.intel.com\/content\/dam\/www\/public\/us\/en\/documents\/manuals\/64-ia-32-architectures-software-developer-manual-325462.pdf Intel. 2013. Intel 64 and IA-32 Architectures Software Developer's Manual. (2013). http:\/\/www.intel.com\/content\/dam\/www\/public\/us\/en\/documents\/manuals\/64-ia-32-architectures-software-developer-manual-325462.pdf"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_1_30_1","unstructured":"Yunsup Lee Albert Ou and Albert Magyar. 2015. Z-Scale: Tiny 32-bit RISC-V Systems. (2015). https:\/\/riscv.org\/wp-content\/uploads\/2015\/06\/riscv-zscale-workshop-june2015.pdf. Yunsup Lee Albert Ou and Albert Magyar. 2015. Z-Scale: Tiny 32-bit RISC-V Systems. (2015). https:\/\/riscv.org\/wp-content\/uploads\/2015\/06\/riscv-zscale-workshop-june2015.pdf."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2014.38"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872399"},{"key":"e_1_3_2_1_33_1","unstructured":"Daniel Lustig Caroline Trippel Yatin A. Manerkar Margaret Martonosi and Michael Pellauer. 2017. Check Research Tools and Papers. (2017). http:\/\/check.cs.princeton.edu\/. Daniel Lustig Caroline Trippel Yatin A. Manerkar Margaret Martonosi and Michael Pellauer. 2017. Check Research Tools and Papers. (2017). http:\/\/check.cs.princeton.edu\/."},{"key":"e_1_3_2_1_34_1","unstructured":"Albert Magyar. 2016. Verilog version of Z-scale. (2016). https:\/\/github.com\/ucb-bar\/vscale. Albert Magyar. 2016. Verilog version of Z-scale. (2016). https:\/\/github.com\/ucb-bar\/vscale."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830782"},{"key":"e_1_3_2_1_36_1","volume-title":"Counterexamples and Proof Loophole for the C\/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. CoRR abs\/1611.01507","author":"Manerkar Yatin A.","year":"2016","unstructured":"Yatin A. Manerkar , Caroline Trippel , Daniel Lustig , Michael Pellauer , and Margaret Martonosi . 2016. Counterexamples and Proof Loophole for the C\/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. CoRR abs\/1611.01507 ( 2016 ). http:\/\/arxiv.org\/abs\/1611.01507 Yatin A. Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. 2016. Counterexamples and Proof Loophole for the C\/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. CoRR abs\/1611.01507 (2016). http:\/\/arxiv.org\/abs\/1611.01507"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2007.70243"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2005.1487886"},{"key":"e_1_3_2_1_41_1","volume-title":"End-to-End Verification of Processors with ISA-Formal. In 28th International Conference on Computer Aided Verification (CAV).","author":"Reid Alastair","year":"2016","unstructured":"Alastair Reid , Rick Chen , Anastasios Deligiannis , David Gilday , David Hoyes , Will Keen , Ashan Pathirane , Owen Shepherd , Peter Vrabel , and Ali Zaidi . 2016 . End-to-End Verification of Processors with ISA-Formal. In 28th International Conference on Computer Aided Verification (CAV). Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, and Ali Zaidi. 2016. End-to-End Verification of Processors with ISA-Formal. In 28th International Conference on Computer Aided Verification (CAV)."},{"key":"e_1_3_2_1_42_1","unstructured":"RISC-V Foundation. 2015. RISC-V in Verilog. (2015). https:\/\/riscv.org\/2015\/09\/risc-v-in-verilog\/. RISC-V Foundation. 2015. RISC-V in Verilog. (2015). https:\/\/riscv.org\/2015\/09\/risc-v-in-verilog\/."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908114"},{"key":"e_1_3_2_1_46_1","unstructured":"SPARC. 1994. SPARC Architecture Manual version 9. (1994). SPARC. 1994. SPARC Architecture Manual version 9. (1994)."},{"key":"e_1_3_2_1_47_1","volume-title":"International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS).","author":"Stewart Daryl","year":"2014","unstructured":"Daryl Stewart , David Gilday , Daniel Nevill , and Thomas Roberts . 2014 . Processor memory system verification using DOGReL: a language for specifying end-to-end properties . In International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS). Daryl Stewart, David Gilday, Daniel Nevill, and Thomas Roberts. 2014. Processor memory system verification using DOGReL: a language for specifying end-to-end properties. In International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS)."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/2893529.2893557"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037719"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391469.1391535"},{"key":"e_1_3_2_1_51_1","volume-title":"Modular Deductive Verification of Multiprocessor Hardware Designs. In 27th International Conference on Computer Aided Verification (CAV).","author":"Vijayaraghavan Muralidaran","year":"2015","unstructured":"Muralidaran Vijayaraghavan , Adam Chlipala , Arvind, and Nirav Dave . 2015 . Modular Deductive Verification of Multiprocessor Hardware Designs. In 27th International Conference on Computer Aided Verification (CAV). Muralidaran Vijayaraghavan, Adam Chlipala, Arvind, and Nirav Dave. 2015. Modular Deductive Verification of Multiprocessor Hardware Designs. In 27th International Conference on Computer Aided Verification (CAV)."},{"key":"e_1_3_2_1_52_1","unstructured":"Mark Walton. 2016. Intel Skylake bug causes PCs to freeze during complex workloads. (2016). https:\/\/arstechnica.com\/gadgets\/2016\/01\/intel-skylake-bug-causes-pcs-to-freeze-during-complex-workloads\/. Mark Walton. 2016. Intel Skylake bug causes PCs to freeze during complex workloads. (2016). https:\/\/arstechnica.com\/gadgets\/2016\/01\/intel-skylake-bug-causes-pcs-to-freeze-during-complex-workloads\/."},{"volume-title":"Practical Assertion-based Formal Verification for SoC Designs. In 2005 International Symposium on System-on-Chip. 58--61","author":"Yeung Ping","key":"e_1_3_2_1_53_1","unstructured":"Ping Yeung and K. Larsen . 2005 . Practical Assertion-based Formal Verification for SoC Designs. In 2005 International Symposium on System-on-Chip. 58--61 . Ping Yeung and K. Larsen. 2005. Practical Assertion-based Formal Verification for SoC Designs. In 2005 International Symposium on System-on-Chip. 58--61."}],"event":{"name":"MICRO-50: The 50th Annual IEEE\/ACM International Symposium on Microarchitecture","sponsor":["SIGMICRO ACM Special Interest Group on Microarchitectural Research and Processing","IEEE-CS\\DATC IEEE Computer Society"],"location":"Cambridge Massachusetts","acronym":"MICRO-50"},"container-title":["Proceedings of the 50th Annual IEEE\/ACM International Symposium on Microarchitecture"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3123939.3124536","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3123939.3124536","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3123939.3124536","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:31Z","timestamp":1750217431000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3123939.3124536"}},"subtitle":["verifying the memory consistency of RTL designs"],"short-title":[],"issued":{"date-parts":[[2017,10,14]]},"references-count":53,"alternative-id":["10.1145\/3123939.3124536","10.1145\/3123939"],"URL":"https:\/\/doi.org\/10.1145\/3123939.3124536","relation":{},"subject":[],"published":{"date-parts":[[2017,10,14]]},"assertion":[{"value":"2017-10-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}