Files in this item



application/pdfUILU-ENG-09-2218 CRHC-09-09.pdf (347kB)
body of reportPDF


application/pdf09-2218 front matter.pdf (44kB)
front matter of reportPDF


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
Date Available in IDEALS:2018-03-30

This item appears in the following Collection(s)

Item Statistics