SHARPE: Statistical High level Analysis and Performance Estimation
Variations in process due to shrinking chip geometries and input pattern variations have contributed significantly to the stochastic nature of contemporary chips. Such variations could translate to variations in delay which in turn can result in incorrect values being occasionally latched by the memory elements. Although the stochastic nature is addressed at the lower levels of the hardware design cycle, the higher levels of design, such as Register Transfer Level (RTL), are analyzed without awareness of the underlying statistics.
Traditional RTL verification treats RTL designs as non-probabilistic systems and asks qualitative queries such as "Does the hardware always provide correct input/output functionality?". However, recent "better-than-worst case" RTL design trends exhibit a willingness to tolerate less-than-100% correctness in the presence of variations in exchange for higher average performance. In such cases, it is desirable to have a methodology that answer queries such as "What is the probability that the design provides correct input/output functionality?" which yield quantitative estimates that are more meaningful to the designer than simple Yes/No answers.
SHARPE is a methodolgy that introduces statistical reasoning in the RTL verification paradigm by incorporating empirical statistical evidence from the lower levels of design. In SHARPE, RTL designs are represented using statistical models and a probabilistic model checking tool (PRISM) is then used to compute quantitative performance estimates. The use of formal verification makes the SHARPE analysis rigorous and high in confidence as compared to simulation-based techniques that are almost always incomplete.
SHARPE is broad in scope and can be applied to provide formal statistical estimates for a diverse range of performance metrics in the presence of different sources of variations. At present, the following applications have been identified for SHARPE:
- Variation-conscious formal timing verification in RTL
- RTL timing degradation analysis in the presence of NBTI aging effects
- BER performance guarantees for MIMO RTL designs
- Vulnerability analysis for RTL designs in the presence of physical faults
Variation-conscious formal timing verification in RTL: The flagship application of SHARPE is to check statistical timing invariance at the higher levels of system design in the presence of input pattern variations. RTL source code is treated as a program and static program analysis techniques are employed in order to compute signal probabilities. The probabilistic RTL modules are then modeled as Discrete Time Markov Chains (DTMCs). Delay macromodels are obtained from the gate level that are used to annotate the states of the RTL DTMC model with cost functions. A probabilistic model checker is then used to check the probability of an RTL block meeting timing. SHARPE is demonstrated on the RTL description of the datapath of OR1200, an open-source embedded processor. SHARPE results are found to be in good agreement with those obtained using a large number of gate-level simulations.
SHARPE provides quick and early estimates of delay distributions of RTL blocks, thereby facilitating better design choices and reducing the overhead in post-synthesis simulation methods. Commercial CAD tools that perform static timing analysis for RTL designs do not provide statistical timing estimates. To the best of our knowledge, SHARPE is the only existing methodology for probabilistic timing analysis in RTL.
SHARPE is being extended to include process variations as the primary source of variation in timing.
Compositional reasoning: Probabilistic model checking tools are well known to face the problem of state-space explosion. Therefore, the SHARPE methodology is feasible only for small RTL designs (less than 10^10 states). A compositional reasoning approach is employed in which a single infeasible instance of model checking is solved by decomposing it into an equivalent set of smaller feasible instances. Thereby, the scalability of SHARPE is significantly improved. For example, SHARPE with compostional reasoning can compute the statistical delay for a 64-bit adder that has more than 10^40 states.
RTL timing degradation analysis in the presence of NBTI aging effects: Timing constraints for a circuit are determined using timing analyses that assume device parameters at the time of manufacturing. As the circuit operates over an extended period of time, it has been observed that the delay at the circuit output degrades, i.e., the circuit "slows" down. Such degradation may result in a violation of the timing constraints, rendering the circuit useless. Therefore, the change in the device parameters over the circuit's lifetime needs to be included in timing analysis at various stages of design.
Negative Bias Temperature Instability (NBTI) effects have been found to be a significant cause for timing degradation in circuits. NBTI effects are stochastic in nature since they strongly depend on signal probabilities. There are several analytical tehcniques at the lower levels of implementation that can compute timing degradation as a function of signal probabilities. However, currently, there is no such technique at the RT level.
In an ongoing project with Texas Instruments, SHARPE is being extended to estimate RTL timing degradation due to NBTI effects. SHARPE can potentially be used to devise a new NBTI-aware design flow that starts at the RTL stage.
BER performance guarantees for MIMO RTL designs: Source of noise such as quantization, introduce randomness into RTL designs of wireless communication systems. The performance of such systems is typically quantified using a metric called Bit Error Rate (BER). BER is an average measure of the probability with which a transmitted data bit is decoded in error. Multiple Input Multiple Output (MIMO) systems are wireless communication systems that are designed to meet stringent BER requirements.
MIMO systems are complex and comprise a large number of digital components implemented at the RT Level. The process of making MIMO RTL designs meet the BER requirements is both time and resource-intensive. This is due to other criteria, such as area and power, that also need to be met. Therefore, it is desirable to have a methodology where performance estimation of MIMO RTL can be performed quickly and with a high degree of confidence.
SHARPE is used for computing BER performance for MIMO RTL designs. Conventionally, BER is estimated with reasonable accuracy by simulating the MIMO RTL over many cycles. For example, in order to compute a BER of 10^-5 accurately, atleast 10^7 simulation cycles are required. In comparison, SHARPE estimates are quick and high in confidence.
SHARPE is applied to several non-trivial components of a MIMO design, such as a Viterbi decoder and a MIMO detector.
Vulnerability analysis for RTL designs in the presence of physical faults: The hardware realization of an RTL design is subject to physical faults that are either permanent of transient in nature. The adverse effects of such faults can be mitigated by employing fault-protection circuitry at locations that are susceptible to faults. In order to minimize the hardware overhead, it is desirable to identify locations at which the occurrence of faults significantly degrades RTL performance and employ protection schemes only at these locations.
Fault models can be included in DTMC in order to represent "faulty" RTL designs. SHARPE can then be used to rigorously analyze the effects of faults at different locations in the hardware. In the context of MIMO RTL designs, SHARPE verifies whether the BER performance is within an acceptable range even in the presence of faults. If the BER fails to meet a specification, SHARPE is extended to provide an error diagnosis in order to characterize the cause of the failure. An important aspect of this approach is that error diagnosis is performed entirely in "software" without the use of hardware "checkers".