Variation-conscious formal timing verification in RTL

Variations in timing can occur due to multiple sources on a chip. Many circuit level statistical techniques are used to analyze timing in the presence of these sources of variation. 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 post-synthesis simulation costs. We introduce SHARPE, a rigorous, systematic methodology to verify design correctness in RTL in the presence of variations. In this paper, we describe SHARPE in the context of computing statistical delay invariants in the presence of input variations. We treat the RTL source code as a program and use static program analysis techniques to compute probabilities. We model the probabilistic RTL modules as Discrete Time Markov Chains (DTMCs) that are then checked formally for probabilistic invariants using PRISM, a probabilistic model checker. Our technique is illustrated on the RTL description of the datapath of OR1200, an open source embedded processor. We demonstrate the enhanced scalability of SHARPE by applying compositional reasoning for probabilistic model checking.