Formal Modeling and Verification of a Victim DRAM Cache
| Autor: | S. Ramesh, Swaraj Sha, Manoranjan Satpathy, Debiprasanna Sahoo, Partha S. Roop, Madhu Mutyam |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
010302 applied physics
Model checking Hardware_MEMORYSTRUCTURES Correctness Finite-state machine Dataflow business.industry Computer science 02 engineering and technology 01 natural sciences Computer Graphics and Computer-Aided Design 020202 computer hardware & architecture Computer Science Applications Linear temporal logic Embedded system 0103 physical sciences 0202 electrical engineering electronic engineering information engineering Cache Electrical and Electronic Engineering business Formal verification Dram |
| Zdroj: | ACM Transactions on Design Automation of Electronic Systems. 24:1-23 |
| ISSN: | 1557-7309 1084-4309 |
| Popis: | The emerging Die-stacking technology enables DRAM to be used as a cache to break the “Memory Wall” 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. 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|