Search

3D integration opens up new opportunities for future multiprocessor chips by enabling fast and highly scalable 3D Network-on-Chip (NoC) topologies. However, in an aim to reduce the cost of Through-silicon via (TSV), partially vertically connected NoCs, in which only a few vertical TSV links are available, have been gaining relevance. To reliably route packets under such conditions, we introduce a lightweight, efficient and highly resilient adaptive routing algorithm targeting partially vertically connected 3D-NoCs named First-Last. It requires a very low number of virtual channels (VCs) to achieve deadlock-freedom (2 VCs in the East and North directions and 1 VC in all other directions), and guarantees packet delivery as long as one healthy TSV connecting all layers is available anywhere in the network. An improved version of our algorithm, named Enhanced-First-Last is also introduced and shown to dramatically improve performance under low TSV availability while still using less virtual channels than state-of-the-art algorithms. A comprehensive evaluation of the cost and performance of our algorithms is performed to demonstrate their merits with respects to existing solutions. [ABSTRACT FROM AUTHOR]

In modern many-core architectures, advanced on-chip networks provide the means of communication for the cores. This greatly complicates the design and verification of the cache coherence protocols deployed by those cores. A common approach to deal with this complexity is to decompose the whole system into the protocol and the network. This decomposition is, however, not always possible. For example, unexpected deadlocks can emerge when a deadlock-free protocol and a deadlock-free network are combined. This paper proposes a compositional methodology: prove properties over a network, prove properties over a protocol, and infer properties over the system as a whole. Our methodology is based on theorems that show that such decomposition is possible by having sufficiently large local buffers at the cores. We apply this methodology to verify several protocols such as MI, MSI, MESI and MEUSI running on top of advanced interconnects with adaptive routing. [ABSTRACT FROM AUTHOR]

Cache coherence plays a major role in manycore systems. The verification of deadlocks is a challenge in particular, because deadlock freedom is an emerging property. Formal methods often decouple verification of the protocol from verification of the communication interconnect. Modern communication fabrics, however, become more advanced and include a network topology, routing, arbitration, synchronization, and more. In this paper, an integrated approach is proposed that allows cross-layer verification of both the cache coherence protocol and the communication fabric all at once. An automated methodology for deriving cross-layer invariants is proposed. These invariants relate the state of the application-layer protocols to en route packets in the communication fabric. Using the invariants, we derive formal proofs of deadlock-freedom for two case studies: a directory-based MI protocol in a 2D mesh, and a ring-based snoopy protocol in a 2D torus. Additionally, we show that our methodology can be used to derive the smallest possible queue sizes that ensure absence of deadlocks. Our methodology is generally applicable and shows promising scalability. [ABSTRACT FROM PUBLISHER]

3D ICs can take advantage of a scalable communication platform, commonly referred to as the Networks-on-Chip (NoC). In the basic form of 3D-NoC, all routers are vertically connected. Partially connected 3D-NoC has emerged because of physical limitations of using vertical links. Routing is of great importance in such partially connected architectures. A high-performance, fault-tolerant and adaptive routing strategy with respect to the communication flow among the cores is crucial while freedom from livelock and deadlock has to be guaranteed. In this paper we introduce a new routing algorithm for partially connected 3D-NoCs. The routing algorithm is adaptive and tolerates the faults on vertical links as compared to the predesigned routing algorithms. Our results show a $40-50\%$ improvement in the fraction of intact inter-level communications when the fault tolerant algorithm is used. This routing algorithm is light-weight and has only one virtual channel along the $Y$ dimension. [ABSTRACT FROM AUTHOR]