Title :
Variation-Conscious Formal Timing Verification in RTL
Author :
Kumar, Jayanand Asok ; Vasudevan, Shobha
Author_Institution :
Dept. of Electr. & Comput. Eng., Univ. of Illinois at Urbana-Champaign, Urbana, IL, USA
Abstract :
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 data path of OR1200, an open source embedded processor. We demonstrate the enhanced scalability of SHARPE by applying compositional reasoning for probabilistic model checking.
Keywords :
Markov processes; integrated circuit design; microprocessor chips; OR1200; PRISM; RTL; SHARPE; circuit level; discrete time Markov chains; embedded processor; formal timing verification; open source; register transfer level; static program analysis; timing variations; Very large scale integration;
Conference_Titel :
VLSI Design (VLSI Design), 2011 24th International Conference on
Conference_Location :
Chennai
Print_ISBN :
978-1-61284-327-8
Electronic_ISBN :
1063-9667
DOI :
10.1109/VLSID.2011.48