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.

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.

TSV-to-TSV coupling is known to be a significant detriment to signal integrity in three-dimensional (3D) IC architectures. Designing a reliable Through-Silicon Via is critical in order to support better performance. This paper explores the challenges brought on by capacitive and inductive TSV-to-TSV coupling in TSV-based 3D ICs. Based on our analyses, we propose two approaches to mitigate these effects. In one approach, a novel coding technique that adjusts the current flow pattern is proposed to mitigate the inductive coupling effects. In another approach an alternative architecture, wrapping around the TSVs, is proposed to greatly reduce the capacitive coupling effect. The efficiency of the proposed coding methods and supporting architectures is demonstrated by comprehensive simulations at both the hardware and system levels.

TSV-based 3D-NoC has been introduced as a viable solution for integrating more cores on a chip, while imposing smaller footprint area and better timing performance as compared to 2D-NoC. However, TSV-to-TSV coupling is increasingly impacting the reliability of 3D-NoCs due to large size of TSVs. Addressing this issue, various resilient approaches have been recently proposed. But they have been evaluated by uniform random distributions fault modelling, which results in 26%-99% inaccuracy. We propose a system-level TSV-to-TSV coupling fault model that models the capacitive coupling effect, considering thermal impact, with circuit-level accuracy. This model can be plugged into any system-level TSV-based 3D-NoC simulator. It is also capable of identifying faulty TSV bundles and evaluating the efficiency of alternative resilient TSV-based 3D-NoC designs at the system-level.

TSV-to-TSV capacitive coupling has large disruptive effects on timing requirements of the circuit. The latency effect of TSV-to-TSV capacitive coupling for different characteristics of a TSV using circuit-level model is presented in this article. Two coding approaches are proposed to mitigate capacitive parasitic effects by adjusting the current flow pattern for any given n × n mesh of TSV arrangement to reduce the number of 8C/7C parasitic capacitance. The experimental results proves the efficacy of the proposed coding methods.

The network-on-chip (NoC) technology allows for integration of a manycore design on a single chip for higher efficiency and scalability. Three-dimensional (3D) NoCs offer several advantages over two-dimensional (2D) NoCs. Through-silicon via (TSV) technology is one of the candidates for implementation of 3D NoCs. TSV reliability analysis is still challenging for 3D NoC designers because of their unique electrical, thermal, and physical characteristics. After providing an overview of common TSV issues, this article aims to define a reliability criterion for NoC and provide a framework for quantifying this reliability as it relates to TSV issues. TSV issues are modeled as a time-invariant failure probability. Also, a reliability criterion for TSV-based NoC is defined. The relationship between NoC reliability and TSV failure is quantified. For the first time, the reliability criterion is reduced to a tractable closed-form expression that requires a single Monte Carlo simulation. Importantly, the Monte Carlo simulation depends only on network geometry. To demonstrate our proposed method, the reliability criterion of a simple 8×8×8 NoC supported by an 8×8×7 network of TSVs is calculated.

Reliability is one of the most challenging problems in the context of three-dimensional network-on-chip (3D NoC) systems. Reliability analysis is prominent for early stages of the manufacturing process in order to prevent costly redesigns of a target system. This article classifies the potential physical faults of a baseline TSV-based 3D NoC architecture by targeting two-dimensional (2D) NoC components and their inter-die connections. In this paper, through-silicon via (TSV) issues, thermal concerns, and single event effect (SEE) are investigated and categorized, in orderto propose evaluation metrics for inspecting the resiliency of 3D NoC designs. A reliability analysis for major source of faults is reported in this article separately based on their mean time to failure (MTTF). TSV failure probability induced by inductive and capacitive coupling is also discussed. Finally, the paper provides a formal reliability analysis on the aggregated faults that affect TSV. This formal analysis is critical for estimating the resiliency of different components in order to mitigate the redundancy cost of fault-tolerant design or to examine the efficiency of any proposed fault-tolerant methods for 3D NoC architectures.

A 3-D multiple-stacked IC has been proposed to support energy efficiency for data center operations as dynamic RAM (DRAM) scaling improves annually. 3-D multiple-stacked IC is a single package containing multiple dies, stacked together, using through-silicon via (TSV) technology. Despite the advantages of 3-D design, fault occurrence rate increases with feature-size reduction of logic devices, which gets worse for 3-D stacked designs. TSV coupling is one of the main reliability issues for 3-D multiple-stacked IC data TSVs. It has large disruptive effects on signal integrity and transmission delay. In this paper, we first characterize the inductance parasitics in contemporary TSVs, and then we analyze and present a classification for inductive coupling cases. Next, we devise a coding algorithm to mitigate the TSV-to-TSV inductive coupling. The coding method controls the current flow direction in TSVs by adjusting the data bit streams at run time to minimize the inductive coupling effects. After performing formal analyses on the efficiency scalability of devised algorithm, an enhanced approach supporting larger bus sizes is proposed. Our experimental results show that the proposed coding algorithm yields significant improvements, while its hardware-implemented encoder results in tangible latency, power consumption, and area.

This paper presents Investigation of Transient Fault Effects in an asynchronous NoC router. The experiment is based on simulation-based fault injection method to assess the fault-tolerant behavior of the asynchronous router. The effort has been accomplished by employing fault injector signal (FIS) in 136 targets. 13600 transient and permanent faults have been injected into the CSP-Verilog model of NoC router. Different fault models such as glitch, cross-talk, SEU, and SET have been applied in this effort to evaluate asynchronous NoC Router. The experimental results have been considered in different aspects to estimate the NoC router's robustness. Although asynchronous designs seem inherently fault-tolerant due to applying handshaking signals, up to 56% of the injected faults result in failure, and about 43% of injected faults are overwritten before turning into errors. Less than 1% of injected faults treat as latent error. Moreover, the failure rate of token generation consumption is higher than token consumption effects.

This paper evaluates fault-tolerant behavior of an NoC router through simulation-based method. A structural-level VHDL environment has been employed to estimate fault injector signal’s (FIS) effects. Different fault models such as dead clause, stuck-then, micro-operation, crosstalk, and SEU have been injected to evaluate the transient faults ’ effects. According to the results, up to 48 % of the injected faults cause system failure and also about 51 % are overwritten before turning into errors. Less than 1 % of injected faults treat as latent errors. The average of fault latency has been investigated as 194ns. Almost 70%, 31%, and 35 % of injected faults are overwritten in buffer, routing unit, and switch components, respectively. Routing unit is also recognized as the most tenuous component. 1.