Statistical model checking (SMC) is a simulation-based approach for verifying the statistical properties of large, complex systems. If a large number of low-probability events (rare events) is required to be simulated, SMC is extremely time-consuming. In this paper, we present a methodology to accelerate the SMC of hardware circuits by generating rare events with a higher frequency. Unlike existing techniques, our methodology can be applied to circuits with multiple rare-event regions. We first sample the circuit uniformly to quickly generate a set of rare events. We employ variational Bayes, a variational inference technique used in machine learning, to infer the distribution of the rare events in the circuit. We then bias the statistical distribution toward these rare event regions. Finally, we employ the SMC using the biased distribution and adjust for the bias that we introduce. The use of variational Bayes enables our methodology to distinguish between multiple rare event regions in the circuit. We demonstrate the effectiveness of our biasing approach on two real-world hardware circuits. We consider the analog (i.e., continuous-time) behavior of these circuits. For an SRAM memory cell, which has a single failure region, we show that our approach provides around 31× speedup over regular SMC while verifying whether the failure rate is less than 10-4. For a successive approximation ADC circuit, which has multiple failure regions, we demonstrate a speedup of 42× while verifying whether the failure rate is less than 10-5.

Because of complexity of analog circuits, their verification presents many challenges. We propose a runtime verification algorithm to verify design properties of nonlinear analog circuits. Our algorithm is based on performing exploratory simulations in the state-time space using the Time-augmented Rapidly Exploring Random Tree (TRRT) algorithm. The proposed runtime verification methodology consists of i) incremental construction of the TRRT to explore the state-time space and ii) use of an incremental online monitoring algorithm to check whether or not the incremented TRRT satisfies or violates specification properties at each iteration. In comparison to the Monte Carlo simulations, for providing the same state-space coverage, we utilize a logarithmic order of memory and time.

Variations in timing can occur due to multiple sources on a chip such as process variations and variations in input patterns. It is desirable to have variation awareness at the register transfer level (RTL), and estimate block level delay distributions early in the design cycle, to evaluate design choices quickly and minimize postsynthesis simulation costs. In previous work, we introduced statistical high-level analysis and rigorous performance estimation (SHARPE), a rigorous, systematic methodology to verify design correctness in RTL in the presence of variations. We described SHARPE in the context of computing statistical delay invariants with respect to input variations. We treated the RTL source code as a program and used static program analysis techniques to compute probabilities. We modeled the probabilistic RTL modules as discrete time Markov chains that are then checked formally for probabilistic invariants using PRISM, a probabilistic model checker. In this paper, we extend SHARPE to perform timing verification in RTL in the context of process variations. We achieved this by obtaining a set of process variation-aware RTL delay models and correspondingly modifying the existing steps in SHARPE. We illustrate SHARPE on the RTL description of the datapath of OR1200, an open source embedded processor. We also apply SHARPE to other data-intensive RTL designs such as nontrivial components of communication systems and a few benchmark designs.

Dynamic power management (DPM) schemes, such as power gating, are important runtime strategies for saving power in multicore architectures. Safety and efficiency are probabilistic properties which need to be verified in order to evaluate a DPM scheme. In this work, we employ statistical model checking to verify probabilistic properties on Register Transfer Level (RTL) descriptions of multicores. Statistical model checking performs a system-level verification of the DPM scheme by simulating several sample paths of the entire RTL design until the verification results lie within tolerable bounds of error. We illustrate our approach on the RTL of OpenSPARC T2, a publicly available industry-strength multicore processor. We verify the safety and efficiency properties of several power gating schemes by considering the power manageable blocks in the floating-point graphics unit.

We present a methodology to generate goal-oriented test cases for verifying nonlinear analog circuits. We use a learning-based approach to identify the goal regions in circuit's state space. We use the information that we learn to guide the growth of Rapidly-exploring Random Trees (RRTs) towards these goal regions. Compared to previous approaches for test generation, our methodology generates several test cases of the circuit that are more concentrated in the relevant operating regions. We demonstrate the effectiveness of our approach on typical case studies. We show that our methodology can be used to generate test cases for undesirable behavior that was previously hard to detect.

In present day technology, the design of reliable systems must factor in temporal degradation due to aging effects such as Negative Bias Temperature Instability (NBTI). In this paper, we present a methodology to estimate delay degradation early at the Register Transfer Level (RTL). We statically analyze the RTL source code to determine signal correlations. We then determine probability distributions of RTL signals formally by using probabilistic model checking. Finally, we propagate these signal probabilities through delay macromodels and estimate the delay degradation. We demonstrate our methodology on several benchmarks RTL designs. We estimate the degradation with <10% error and up to 18.2x speedup in runtime as compared to estimation using gate-level simulations.

Sources of noise such as quantization, introduce randomness into register transfer level (RTL) designs of complex systems. In previous work, we introduced a formal approach to compute the performance metrics for these designs with high confidence. We defined the performance metrics as properties in a probabilistic temporal logic. We then used probabilistic model checking to verify these properties for RTL and thereby guarantee the statistical performance. In this work, we enhance our previous approach in order to include the effects of permanent and transient faults that may be present in the lower levels of hardware implementation. We then formally analyze the vulnerability of performance of RTL designs to faults that are present at different locations. If a performance requirement is not met, we employ probabilistic model checking with a diagnostic property that can be used to identify the broad cause of performance degradation. In this work, we describe our entire approach by considering RTL designs corresponding to multiple-input-multiple-output (MIMO) communication systems. We illustrate our enhanced approach on the Viterbi decoder which is a nontrivial component of MIMO system designs.

Sources of noise such as quantization, introduce randomness into Register Transfer Level (RTL) designs of Multiple Input Multiple Output (MIMO) systems. Performance of these MIMO RTL designs is typically quantified by metrics averaged over simulations. In this paper, we introduce a formal approach to compute these metrics with high confidence. We define best, bounded and average case performance metrics as properties in a probabilistic temporal logic. We then use probabilistic model checking to verify these properties for MIMO RTL and thereby guarantee the statistical performance. If a property fails, we show a characterization of error. However, probabilistic model checking is known to encounter the problem of state space explosion. With respect to the properties of interest, we show sound and efficient reductions that significantly improve the scalability of our approach. We illustrate our approach on different non-trivial components of MIMO system designs.