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.

GPGPUs are now commonly used as co-processors of CPUs for the computation of data parallel and throughputintensive algorithms. However, memory available in GPGPUs is limited for many applications of interest; there is a continuous demand for increased memory of such applications. Several techniques like multi-steaming or pinned memory are frequently employed to mitigate these issues to some extent. However, these techniques either suffer from latency overhead or increase programming complexity. GPUdmm uses GPU DRAM as a cache of CPU; key problems in this design are inefficient memory access data-path and tag access overhead. In this context, we present CAMO, a novel cache memory organization for GPGPUs which addresses the limitations of pinned memory technique and GPUdmm. First, it uses GPU DRAM as a victim cache of LLC that improves the performance by delivering data faster to the SMs. Second, it uses ATCache, a CPU based DRAM cache tag management technique. ATCache reduces the number of DRAM cache accesses. We implement CAMO within the GPGPU-Sim framework and show that its average performance - when compared with pinned memory - increases by a factor of 1.87x and the peak performance growth being 4.67x. In addition, CAMO outperforms GPUdmm on an average by a factor of 15.9% and maximum speedup by a factor of 80%.

Die-stacking technology enables the use of a high density DRAM as a cache. Major processor vendors have recently started using these stacked DRAM modules as the last level cache of their products. These stacked DRAM modules provide high bandwidth with relatively low latency compared to the off-package DRAM modules. Recent studies on DRAM caches propose several variants to optimize performance and power of the systems. However, none of the existing works discuss its design and verification aspect. DRAM cache controller (DCC) design is significantly complex in comparison to a conventional DRAM-based main memory controller. This is because it involves controlling both the timing aspect of DRAM system as well as the functional aspect of cache. Therefore, without rigorous modeling and verification of such designs, it would be difficult to ensure correctness. In the current research, we focus on the design and verification issues of DCC. We select a common variant of DRAM cache and build a formal model of its controller in terms of interacting state machines; we term the common variant as the baseline and its model as the base model. We then verify safety, liveness, and timing properties of this variant using model checking. Next, we demonstrate how the formal models and the associated properties of other variants of DCCs can be derived from the base model in a systematic way. Analyzing the individual DRAM cache variations, we observe that most of the variants exhibit product-line characteristics.