Formal probabilistic timing verification in RTL

Jayanand Asok Kumar, Shobha Vasudevan

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish (US)
Article number6504532
Pages (from-to)788-801
Number of pages14
JournalIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Issue number5
StatePublished - May 1 2013


  • Average case design
  • formal methods
  • probabilistic model checking
  • register transfer level (RTL) timing analysis

ASJC Scopus subject areas

  • Software
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Formal probabilistic timing verification in RTL'. Together they form a unique fingerprint.

Cite this