## Files in this item

FilesDescriptionFormat

application/pdf

UILU-ENG-09-2218 CRHC-09-09.pdf (347kB)
body of reportPDF

application/pdf

09-2218 front matter.pdf (44kB)
front matter of reportPDF

## Description

 Title: SHARPE: Variation-Aware Formal Statistical Timing Analysis in RTL Author(s): Kumar, Jayanand Asok; Vasudevan, Shobha Subject(s): Probabilistic model checking Statistical delay distribution RTL timing Static analysis 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. At the system (higher) level of design, however, timing estimation/verification is not performed. The design at the Register Transfer Level (RTL) is unaware of the underlying statistics and timing variations. It is desirable to have variation awareness'' at the higher level, and estimate block level delay distributions early in the design cycle, to evaluate design choices quickly and minimize post-synthesis simulation costs. In this paper, we introduce SHARPE, a rigorous, systematic timing analysis/verification methodology and tool flow to find statistical delay invariants in RTL. 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. Issue Date: 2009-12 Publisher: Coordinated Science Laboratory, University of Illinois at Urbana-Champaign Series/Report: Coordinated Science Laboratory Report no. UILU-ENG-09-2218, CRHC-09-09 Genre: Technical Report Type: Text Language: English URI: http://hdl.handle.net/2142/99567 Date Available in IDEALS: 2018-03-30
﻿