Formal Probabilistic Timing Verification in RTL

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.