Efficient Statistical Model Checking of Hardware Circuits With Multiple Failure Regions

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.