SHARPE: Variation-Aware Formal Statistical Timing Analysis in RTL

Kumar, Jayanand Asok; Vasudevan, Shobha

Permalink

https://hdl.handle.net/2142/99567 Copy

Description

Title

SHARPE: Variation-Aware Formal Statistical Timing Analysis in RTL

Author(s)

• Kumar, Jayanand Asok
• Vasudevan, Shobha

Issue Date

2009-12

Keyword(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.

Publisher

Coordinated Science Laboratory, University of Illinois at Urbana-Champaign

Series/Report Name or Number

Coordinated Science Laboratory Report no. UILU-ENG-09-2218, CRHC-09-09

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/99567

Owning Collections