{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:32:11Z","timestamp":1750221131213,"version":"3.41.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2019,2,13]],"date-time":"2019-02-13T00:00:00Z","timestamp":1550016000000},"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":[[2019,3,31]]},"abstract":"<jats:p>\n            The emerging\n            <jats:italic>Die-stacking<\/jats:italic>\n            technology enables DRAM to be used as a cache to break the \u201cMemory Wall\u201d problem. Recent studies have proposed to use DRAM as a victim cache in both CPU and GPU memory hierarchies to improve performance. DRAM caches are large in size and, hence, when realized as a victim cache, non-inclusive design is preferred. This non-inclusive design adds significant differences to the conventional DRAM cache design in terms of its probe, fill, and writeback policies. Design and verification of a victim DRAM cache can be much more complex than that of a conventional DRAM cache. Hence, without rigorous modeling and formal verification, ensuring the correctness of such a system can be difficult.\n          <\/jats:p>\n          <jats:p>The major focus of this work is to show how formal modeling is applied to design and verify a victim DRAM cache. In this approach, we identify the agents in the victim DRAM cache design and model them in terms of interacting state machines. We derive a set of properties from the specifications of a victim cache and encode them using Linear Temporal Logic. The properties are then proven using symbolic and bounded model checking. Finally, we discuss how these properties are related to the dataflow paths in a victim DRAM cache.<\/jats:p>","DOI":"10.1145\/3306491","type":"journal-article","created":{"date-parts":[[2019,2,14]],"date-time":"2019-02-14T19:36:17Z","timestamp":1550172977000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Modeling and Verification of a Victim DRAM Cache"],"prefix":"10.1145","volume":"24","author":[{"given":"Debiprasanna","family":"Sahoo","sequence":"first","affiliation":[{"name":"Indian Institute of Technology Bhubaneswar, Arugul, Bhubaneswar, Odisha, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Swaraj","family":"Sha","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Bhubaneswar, Arugul, Bhubaneswar, Odisha, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manoranjan","family":"Satpathy","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Bhubaneswar, Arugul, Bhubaneswar, Odisha, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Madhu","family":"Mutyam","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Madras, Chennai, Tamil Nadu, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Ramesh","sequence":"additional","affiliation":[{"name":"General Motors R8D, Michigan, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Partha","family":"Roop","sequence":"additional","affiliation":[{"name":"University of Auckland, Auckland, New Zealand"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,2,13]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/3168451.3168470"},{"key":"e_1_2_1_2_1","volume-title":"Bounded model checking. Advances in Computers","author":"Biere A.","year":"2003","unstructured":"A. Biere , A. Cimatti , Edmund M. Clarke , Ofer Strichman , and Yunshan Zhu . 2003. Bounded model checking. Advances in Computers ( 2003 ). A. Biere, A. Cimatti, Edmund M. Clarke, Ofer Strichman, and Yunshan Zhu. 2003. Bounded model checking. Advances in Computers (2003)."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2006.18"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-010-0092-y"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2749469.2750387"},{"volume-title":"Proceedings of the 49th International Symposium on Microarchitecture (MICRO\u201916)","author":"Chou C.","key":"e_1_2_1_6_1","unstructured":"C. Chou , A. Jaleel , and M. K. Qureshi . 2016. CANDY: Enabling coherent DRAM caches for multi-node systems . In Proceedings of the 49th International Symposium on Microarchitecture (MICRO\u201916) . IEEE, 1--13. C. Chou, A. Jaleel, and M. K. Qureshi. 2016. CANDY: Enabling coherent DRAM caches for multi-node systems. In Proceedings of the 49th International Symposium on Microarchitecture (MICRO\u201916). IEEE, 1--13."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30494-4_27"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2010.31"},{"key":"e_1_2_1_10_1","unstructured":"L. de Moura S. Owre and N. Shankar. 2003. The SAL Language Manual. Technical Report. CSL Tech report SRI-CSL-01-02.  L. de Moura S. Owre and N. Shankar. 2003. The SAL Language Manual. Technical Report. CSL Tech report SRI-CSL-01-02."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734088"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026276129010"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 8th International Conference on Computer Aided Verification. Springer-Verlag","author":"Dill D. L.","year":"1996","unstructured":"D. L. Dill . 1996 . The Murphi verification system . In Proceedings of the 8th International Conference on Computer Aided Verification. Springer-Verlag , Berlin, 390--393. D. L. Dill. 1996. The Murphi verification system. In Proceedings of the 8th International Conference on Computer Aided Verification. Springer-Verlag, Berlin, 390--393."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39724-3_22"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2014.36"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2014.10"},{"key":"e_1_2_1_17_1","first-page":"1","article-title":"MCXplore: Automating the validation process of DRAM memory controller designs","volume":"37","author":"Hassan M.","year":"2018","unstructured":"M. Hassan and H. Patel . 2018 . MCXplore: Automating the validation process of DRAM memory controller designs . IEEE Trans. Comput.-Aid. Des. Integr. Circ. Syst. 37 , 5 (2018), 1 -- 14 . M. Hassan and H. Patel. 2018. MCXplore: Automating the validation process of DRAM memory controller designs. IEEE Trans. Comput.-Aid. Des. Integr. Circ. Syst. 37, 5 (2018), 1--14.","journal-title":"IEEE Trans. Comput.-Aid. Des. Integr. Circ. Syst."},{"volume-title":"Proceedings of the 49th International Symposium on Microarchitecture (MICRO\u201916)","author":"Huang C. C.","key":"e_1_2_1_18_1","unstructured":"C. C. Huang , R. Kumar , M. Elver , B. Grot , and V. Nagarajan . 2016. C3D: Mitigating the NUMA bottleneck via coherent DRAM caches . In Proceedings of the 49th International Symposium on Microarchitecture (MICRO\u201916) . IEEE, 1--12. C. C. Huang, R. Kumar, M. Elver, B. Grot, and V. Nagarajan. 2016. C3D: Mitigating the NUMA bottleneck via coherent DRAM caches. In Proceedings of the 49th International Symposium on Microarchitecture (MICRO\u201916). IEEE, 1--12."},{"volume-title":"Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis (SC\u201916)","author":"Huang C. C.","key":"e_1_2_1_19_1","unstructured":"C. C. Huang , V. Nagarajan , and A. Joshi . 2016. DCA: A DRAM-cache-Aware DRAM controller . In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis (SC\u201916) . IEEE, 887--897. C. C. Huang, V. Nagarajan, and A. Joshi. 2016. DCA: A DRAM-cache-Aware DRAM controller. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis (SC\u201916). IEEE, 887--897."},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the International Symposium on Circuits and Systems (ISCAS\u201901)","volume":"5","author":"Ivanov L.","unstructured":"L. Ivanov and R. Nunna . 2001. Modeling and verification of cache coherence protocols . In Proceedings of the International Symposium on Circuits and Systems (ISCAS\u201901) , Vol. 5 . L. Ivanov and R. Nunna. 2001. Modeling and verification of cache coherence protocols. In Proceedings of the International Symposium on Circuits and Systems (ISCAS\u201901), Vol. 5."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2014.51"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2485922.2485957"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03845-7_15"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325162"},{"key":"e_1_2_1_25_1","unstructured":"Stephen Junkins. 2014. The Compute Architecture of Intel Processor Graphics Gen7.5.  Stephen Junkins. 2014. The Compute Architecture of Intel Processor Graphics Gen7.5."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2010.38"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2008.4547694"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/307988.307989"},{"volume-title":"Proceedings of the 10th International Conference on Design Technology of Integrated Systems in Nanoscale Era (DTIS\u201915)","author":"Khalifa K.","key":"e_1_2_1_29_1","unstructured":"K. Khalifa and K. Salah . 2015. Implementation and verification of a generic universal memory controller based on UVM . In Proceedings of the 10th International Conference on Design Technology of Integrated Systems in Nanoscale Era (DTIS\u201915) . IEEE, Los Alamitos, CA, 1--2. K. Khalifa and K. Salah. 2015. Implementation and verification of a generic universal memory controller based on UVM. In Proceedings of the 10th International Conference on Design Technology of Integrated Systems in Nanoscale Era (DTIS\u201915). IEEE, Los Alamitos, CA, 1--2."},{"volume-title":"Proceedings of the 20th International Symposium on High Performance Computer Architecture (HPCA\u201914)","author":"Kim Y.","key":"e_1_2_1_30_1","unstructured":"Y. Kim , J. Lee , J. E. Jo , and J. Kim . 2014. GPUdmm: A high-performance and memory-oblivious GPU architecture using dynamic memory management . In Proceedings of the 20th International Symposium on High Performance Computer Architecture (HPCA\u201914) . IEEE, 546--557. Y. Kim, J. Lee, J. E. Jo, and J. Kim. 2014. GPUdmm: A high-performance and memory-oblivious GPU architecture using dynamic memory management. In Proceedings of the 20th International Symposium on High Performance Computer Architecture (HPCA\u201914). IEEE, 546--557."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/L-CA.2013.19"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663345"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127908.1127991"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3126908.3126931"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2155620.2155673"},{"volume-title":"Symbolic Model Checking","author":"McMillan Kenneth L.","key":"e_1_2_1_38_1","unstructured":"Kenneth L. McMillan . 1993. Symbolic Model Checking . Kluwer Academic . Kenneth L. McMillan. 1993. Symbolic Model Checking. Kluwer Academic."},{"volume-title":"Correct Hardware Design and Verification Methods","author":"McMillan Kenneth L.","key":"e_1_2_1_39_1","unstructured":"Kenneth L. McMillan . 2001. Parameterized verification of the FLASH cache coherence protocol by compositional model checking . In Correct Hardware Design and Verification Methods . Springer , 179--195. Kenneth L. McMillan. 2001. Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In Correct Hardware Design and Verification Methods. Springer, 179--195."},{"volume-title":"Proceedings of the 21st International Symposium on High Performance Computer Architecture (HPCA\u201915)","author":"Meswani M. R.","key":"e_1_2_1_40_1","unstructured":"M. R. Meswani , S. Blagodurov , D. Roberts , J. Slice , M. Ignatowski , and G. H. Loh . 2015. Heterogeneous memory architectures: A HW\/SW approach for mixing die-stacked and off-package memories . In Proceedings of the 21st International Symposium on High Performance Computer Architecture (HPCA\u201915) . IEEE, 126--136. M. R. Meswani, S. Blagodurov, D. Roberts, J. Slice, M. Ignatowski, and G. H. Loh. 2015. Heterogeneous memory architectures: A HW\/SW approach for mixing die-stacked and off-package memories. In Proceedings of the 21st International Symposium on High Performance Computer Architecture (HPCA\u201915). IEEE, 126--136."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858792"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2008.2007462"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357178"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.406955"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/248621.248624"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2012.30"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/VLSID.2016.88"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCA.2018.2865552"},{"volume-title":"Proceedings of the 23rd Asia and South Pacific-Design Automation Conference (ASP-DAC\u201918)","author":"Sahoo D.","key":"e_1_2_1_49_1","unstructured":"D. Sahoo , S. Sha , M. Satpathy , M. Mutyam , and L. N. Bhuyan . 2018. CAMO: A novel cache management organization for GPGPUs . In Proceedings of the 23rd Asia and South Pacific-Design Automation Conference (ASP-DAC\u201918) . IEEE. D. Sahoo, S. Sha, M. Satpathy, M. Mutyam, and L. N. Bhuyan. 2018. CAMO: A novel cache management organization for GPGPUs. In Proceedings of the 23rd Asia and South Pacific-Design Automation Conference (ASP-DAC\u201918). IEEE."},{"key":"e_1_2_1_50_1","first-page":"11","article-title":"Formal modeling and verification of controllers for a family of DRAM caches","volume":"37","author":"Sahoo D.","year":"2018","unstructured":"D. Sahoo , S. Sha , M. Satpathy , M. Mutyam , S. Ramesh , and P. Roop . 2018 . Formal modeling and verification of controllers for a family of DRAM caches . IEEE Trans. Comput.-Aid. Des. Integr. Circ. Syst. 37 , 11 (Nov. 2018), 2485--2496. D. Sahoo, S. Sha, M. Satpathy, M. Mutyam, S. Ramesh, and P. Roop. 2018. Formal modeling and verification of controllers for a family of DRAM caches. IEEE Trans. Comput.-Aid. Des. Integr. Circ. Syst. 37, 11 (Nov. 2018), 2485--2496.","journal-title":"IEEE Trans. Comput.-Aid. Des. Integr. Circ. Syst."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2016.25"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.589235"},{"key":"e_1_2_1_53_1","volume-title":"GPU Technology Conference (GTC), NVIDIA (2017","author":"Wolfe M.","year":"2017","unstructured":"M. Wolfe . 2017 . The future of GPU data management . GPU Technology Conference (GTC), NVIDIA (2017 ). http:\/\/on-demand.gputechconf.com\/gtc\/2017\/presentation\/s7628-Michael-Wolfe-GPU.pdf. M. Wolfe. 2017. The future of GPU data management. GPU Technology Conference (GTC), NVIDIA (2017). http:\/\/on-demand.gputechconf.com\/gtc\/2017\/presentation\/s7628-Michael-Wolfe-GPU.pdf."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3079856.3080243"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3306491","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3306491","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:24Z","timestamp":1750208544000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3306491"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,13]]},"references-count":52,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,3,31]]}},"alternative-id":["10.1145\/3306491"],"URL":"https:\/\/doi.org\/10.1145\/3306491","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2019,2,13]]},"assertion":[{"value":"2018-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-02-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}