{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:55:18Z","timestamp":1773194118342,"version":"3.50.1"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319216676","type":"print"},{"value":"9783319216683","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21668-3_7","type":"book-chapter","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T15:08:53Z","timestamp":1436800133000},"page":"109-127","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["Modular Deductive Verification of Multiprocessor Hardware Designs"],"prefix":"10.1007","author":[{"given":"Muralidaran","family":"Vijayaraghavan","sequence":"first","affiliation":[]},{"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[]},{"family":"Arvind","sequence":"additional","affiliation":[]},{"given":"Nirav","family":"Dave","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"7_CR1","unstructured":"Arvind, Nikhil, R.S., Rosenband, D.L., Dave, N.: High-level synthesis: an essential ingredient for designing complex ASICs. In: Proceedings of ICCAD 2004, San Jose, CA (2004)"},{"issue":"3","key":"7_CR2","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1109\/40.768501","volume":"19","author":"Arvind","year":"1999","unstructured":"Arvind, Shen, X.: Using term rewriting systems to design and verify processors. Micro, IEEE 19(3), 36\u201346 (1999)","journal-title":"Micro, IEEE"},{"key":"7_CR3","unstructured":"Augustsson, L., Schwarz, J., Nikhil, R.S.: Bluespec Language definition, Sandburst Corp (2001)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/11560548_25","volume-title":"Correct Hardware Design and Verification Methods","author":"R Bhattacharya","year":"2005","unstructured":"Bhattacharya, R., German, S.M., Gopalakrishnan, G.C.: Symbolic partial order reduction for rule based transition systems. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 332\u2013335. Springer, Heidelberg (2005)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11691617_15","volume-title":"Model Checking Software","author":"R Bhattacharya","year":"2006","unstructured":"Bhattacharya, R., German, S.M., Gopalakrishnan, G.C.: Exploiting symmetry and transactions for partial order reduction of rule based specifications. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 252\u2013270. Springer, Heidelberg (2006)"},{"key":"7_CR6","unstructured":"Bluespec Inc, Waltham, M.A.: Bluespec SystemVerilog Version 3.8 Reference Guide, November 2004"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-642-39799-8_14","volume-title":"Computer Aided Verification","author":"T Braibant","year":"2013","unstructured":"Braibant, T., Chlipala, A.: Formal verification of hardware synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 213\u2013228. Springer, Heidelberg (2013)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification","author":"JR Burch","year":"1994","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) Computer Aided Verification. LNCS, pp. 68\u201380. Springer, Heidelberg (1994)"},{"key":"7_CR9","unstructured":"Cain, H.W., Lipasti, M.H.: Memory ordering: a value-based approach. In: Proceedings of the 31st Annual International Symposium on Computer Architecture, 2004, pp. 90\u2013101, June 2004"},{"issue":"2","key":"7_CR10","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1109\/MDT.2005.30","volume":"22","author":"C Chang","year":"2005","unstructured":"Chang, C., Wawrzynek, J., Brodersen, R.W.: Bee2: a high-end reconfigurable computing system. Des. Test Comput. IEEE 22(2), 114\u2013125 (2005)","journal-title":"Des. Test Comput. IEEE"},{"issue":"1","key":"7_CR11","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s10703-010-0092-y","volume":"36","author":"Y Xiaofang Chen","year":"2010","unstructured":"Xiaofang Chen, Y., Yang, G.G., Chou, C.-T.: Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols. Form. Methods Syst. Des. 36(1), 37\u201364 (2010)","journal-title":"Form. Methods Syst. Des."},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Chou, C.-T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Formal Methods in Computer Aided Design, pp. 382\u2013398. Springer (2004)","DOI":"10.1007\/978-3-540-30494-4_27"},{"key":"7_CR13","unstructured":"Dave, N., Ng, M.C., Arvind.: Automatic synthesis of cache-coherence protocol processors using bluespec. In: Proceedings of Formal Methods and Models for Codesign, MEMOCODE, Verona, Italy (2005)"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Computer Aided Verification","author":"G Delzanno","year":"2000","unstructured":"Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification. LNCS, vol. 1855, pp. 53\u201368. Springer, Heidelberg (2000)"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: Proceedings of the IEEE 1992 International Conference on Computer Design: VLSI in Computers and Processors, ICCD 1992, pp. 522\u2013525, October 1992","DOI":"10.1109\/ICCD.1992.276232"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-540-39724-3_22","volume-title":"Correct Hardware Design and Verification Methods","author":"EA Emerson","year":"2003","unstructured":"Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 247\u2013262. Springer, Heidelberg (2003)"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Hoe, J.C., Arvind.: Synthesis of operation-centric hardware descriptions. In: Proceedings of ICCAD 2000, pp. 511\u2013518, San Jose, CA (2000)","DOI":"10.1109\/ICCAD.2000.896524"},{"key":"7_CR18","unstructured":"Hoe, J.C., Arvind.: Operation-centric hardware description and synthesis. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 23(9), 1277\u20131288 (2004)"},{"key":"7_CR19","unstructured":"Norris Ip, C., Dill, D.L., Mitchell, J.C.: State reduction methods for automatic formal verification (1996)"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/3-540-44585-4_40","volume-title":"Computer Aided Verification","author":"R Jhala","year":"2001","unstructured":"Jhala, R., McMillan, K.L.: Microarchitecture verification by compositional model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 396\u2013410. Springer, Heidelberg (2001)"},{"issue":"2","key":"7_CR21","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1023\/A:1022969405325","volume":"22","author":"R Joshi","year":"2003","unstructured":"Joshi, R., Lamport, L., Matthews, J., Tasiran, S., Tuttle, M.R., Yuan, Y.: Checking cache-coherence protocols with TLA $${}^{\\text{+ }}$$ . Formal Methods Syst. Des. 22(2), 125\u2013131 (2003)","journal-title":"Formal Methods Syst. Des."},{"key":"7_CR22","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-642-02658-4_32","volume-title":"Computer Aided Verification","author":"R Kaivola","year":"2009","unstructured":"Kaivola, R., Ghughal, R., Narasimhan, N., Telfer, A., Whittemore, J., Pandav, S., Slobodov\u00e1, A., Taylor, C., Frolov, V., Reeber, E., et al.: Replacing testing with formal verification in $${\\rm Intel}^{\\textregistered }$$ $${\\rm Core}^{\\rm tm}$$ i7 processor execution engine validation. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, vol. 5643, pp. 414\u2013429. Springer, Heidelberg (2009)"},{"key":"7_CR23","unstructured":"Khan, A., Vijayaraghavan, M., Boyd-Wickizer, S., Arvind: Fast and cycle-accurate modeling of a multicore processor. In: 2012 IEEE International Symposium on Performance Analysis of Systems & Software, pp. 178\u2013187, New Brunswick, NJ, USA, April 1\u20133, 2012"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Kuskin, J., Ofelt, D., Heinrich, M., Heinlein, J., Simoni, R., Gharachorloo, K., Chapin, J., Nakahira, D., Baxter, J., Horowitz, M.A., Gupta, A.M., Rosenblum, M., Hennessy, J.: The stanford FLASH multiprocessor. In: Proceedings of the 21st Annual International Symposium on Computer Architecture, pp. 302\u2013313, April 1994","DOI":"10.1145\/192007.192056"},{"issue":"9","key":"7_CR25","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"100","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 100(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"7_CR26","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Manolios, P., Srinivasan, S.K.: Automatic verification of safety and liveness for pipelined machines using WEB refinement. ACM Trans. Des. Autom. Electron. Syst. 45:1\u201345:19 (2008)","DOI":"10.1145\/1367045.1367054"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/3-540-44798-9_17","volume-title":"Correct Hardware Design and Verification Methods","author":"KL McMillan","year":"2001","unstructured":"McMillan, K.L.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 179\u2013195. Springer, Heidelberg (2001)"},{"key":"7_CR29","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"1998","unstructured":"McMillan, K.L.: Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification, pp. 110\u2013121. Springer, Heidelberg (1998)"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/3-540-48153-2_17","volume-title":"Correct Hardware Design and Verification Methods","author":"KL McMillan","year":"1999","unstructured":"McMillan, K.L.: Verification of infinite state systems by compositional model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 219\u2013237. Springer, Heidelberg (1999)"},{"key":"7_CR31","unstructured":"McMillan, K.L., Schwalbe, J.: Formal verification of the Gigamax cache consistency protocol. In: Proceedings of the International Symposium on Shared Memory Multiprocessing, pp. 111\u2013134 (1992)"},{"key":"7_CR32","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/BFb0028728","volume-title":"Computer Aided Verification","author":"JS Moore","year":"1998","unstructured":"Moore, J.S.: An ACL2 proof of write invalidate cache coherence. In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification. LNCS, vol. 1427, pp. 29\u201338. Springer, Heidelberg (1998)"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Park, S., Dill, D.L.: Verification of FLASH cache coherence protocol by aggregation of distributed transactions. In: Proceedings of the 8th Annual ACM Symposium on Parallel Algorithms and Architectures, pp. 288\u2013296. ACM Press (1996)","DOI":"10.1145\/237502.237573"},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"Shen, X., Arvind, Rudolph, L.: Commit-reconcile & fences (CRF): a new memory model for architects and compiler writers. In: Proceedings of the 26th annual international symposium on Computer architecture, pp. 150\u2013161. IEEE Computer Society (1999)","DOI":"10.1145\/307338.300992"},{"key":"7_CR35","doi-asserted-by":"crossref","unstructured":"Talupur, M., Tuttle, M.R.: Going with the flow: parameterized verification using message flows. In: Formal Methods in Computer-Aided Design, FMCAD 2008, pp. 1\u20138, November 2008","DOI":"10.1109\/FMCAD.2008.ECP.14"},{"issue":"1","key":"7_CR36","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1109\/12.368009","volume":"44","author":"PJ Windley","year":"1995","unstructured":"Windley, P.J.: Formal modeling and verification of microprocessors. IEEE Trans. Comput. 44(1), 54\u201372 (1995)","journal-title":"IEEE Trans. Comput."},{"key":"7_CR37","doi-asserted-by":"crossref","unstructured":"Zhang, M., Bingham, J.D., Erickson, J., Sorin, D.J.: Pvcoherence: designing flat coherence protocols for scalable verification. In: 20th IEEE International Symposium on High Performance Computer Architecture, HPCA 2014, pp. 392\u2013403. IEEE Computer Society, Orlando, FL, USA, February 15\u201319 (2014)","DOI":"10.1109\/HPCA.2014.6835949"},{"key":"7_CR38","doi-asserted-by":"crossref","unstructured":"Zhang, M., Lebeck, A.R., Sorin. D.J.: Fractal coherence: scalably verifiable cache coherence. In: Proceedings of the 2010 43rd Annual IEEE\/ACM International Symposium on Microarchitecture, MICRO \u201943, pp. 471\u2013482. IEEE Computer Society, Washington, DC, USA (2010)","DOI":"10.1109\/MICRO.2010.11"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21668-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T04:46:09Z","timestamp":1748493969000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21668-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216676","9783319216683"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"14 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}