Variation-conscious formal timing verification in RTL

Jayanand Asok Kumar, Shobha Vasudevan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 datapath of OR1200, an open source embedded processor. We demonstrate the enhanced scalability of SHARPE by applying compositional reasoning for probabilistic model checking.

Original languageEnglish (US)
Title of host publicationProceedings - 24th International Conference on VLSI Design, VLSI Design 2011, Held Jointly with 10th International Conference on Embedded Systems
Pages58-63
Number of pages6
DOIs
StatePublished - Mar 25 2011
Event24th International Conference on VLSI Design, VLSI Design 2011, Held Jointly with 10th International Conference on Embedded Systems - Chennai, India
Duration: Jan 2 2011Jan 7 2011

Publication series

NameProceedings of the IEEE International Conference on VLSI Design
ISSN (Print)1063-9667

Other

Other24th International Conference on VLSI Design, VLSI Design 2011, Held Jointly with 10th International Conference on Embedded Systems
CountryIndia
CityChennai
Period1/2/111/7/11

Fingerprint

Model checking
Markov processes
Scalability
Networks (circuits)
Costs
Statistical Models

ASJC Scopus subject areas

  • Hardware and Architecture
  • Electrical and Electronic Engineering

Cite this

Kumar, J. A., & Vasudevan, S. (2011). Variation-conscious formal timing verification in RTL. In Proceedings - 24th International Conference on VLSI Design, VLSI Design 2011, Held Jointly with 10th International Conference on Embedded Systems (pp. 58-63). [5718778] (Proceedings of the IEEE International Conference on VLSI Design). https://doi.org/10.1109/VLSID.2011.48

Variation-conscious formal timing verification in RTL. / Kumar, Jayanand Asok; Vasudevan, Shobha.

Proceedings - 24th International Conference on VLSI Design, VLSI Design 2011, Held Jointly with 10th International Conference on Embedded Systems. 2011. p. 58-63 5718778 (Proceedings of the IEEE International Conference on VLSI Design).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Kumar, JA & Vasudevan, S 2011, Variation-conscious formal timing verification in RTL. in Proceedings - 24th International Conference on VLSI Design, VLSI Design 2011, Held Jointly with 10th International Conference on Embedded Systems., 5718778, Proceedings of the IEEE International Conference on VLSI Design, pp. 58-63, 24th International Conference on VLSI Design, VLSI Design 2011, Held Jointly with 10th International Conference on Embedded Systems, Chennai, India, 1/2/11. https://doi.org/10.1109/VLSID.2011.48
Kumar JA, Vasudevan S. Variation-conscious formal timing verification in RTL. In Proceedings - 24th International Conference on VLSI Design, VLSI Design 2011, Held Jointly with 10th International Conference on Embedded Systems. 2011. p. 58-63. 5718778. (Proceedings of the IEEE International Conference on VLSI Design). https://doi.org/10.1109/VLSID.2011.48
Kumar, Jayanand Asok ; Vasudevan, Shobha. / Variation-conscious formal timing verification in RTL. Proceedings - 24th International Conference on VLSI Design, VLSI Design 2011, Held Jointly with 10th International Conference on Embedded Systems. 2011. pp. 58-63 (Proceedings of the IEEE International Conference on VLSI Design).
@inproceedings{e4a4ed771cfd4277b84a9305f36fa399,
title = "Variation-conscious formal timing verification in RTL",
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 datapath of OR1200, an open source embedded processor. We demonstrate the enhanced scalability of SHARPE by applying compositional reasoning for probabilistic model checking.",
author = "Kumar, {Jayanand Asok} and Shobha Vasudevan",
year = "2011",
month = "3",
day = "25",
doi = "10.1109/VLSID.2011.48",
language = "English (US)",
isbn = "9780769543482",
series = "Proceedings of the IEEE International Conference on VLSI Design",
pages = "58--63",
booktitle = "Proceedings - 24th International Conference on VLSI Design, VLSI Design 2011, Held Jointly with 10th International Conference on Embedded Systems",

}

TY - GEN

T1 - Variation-conscious formal timing verification in RTL

AU - Kumar, Jayanand Asok

AU - Vasudevan, Shobha

PY - 2011/3/25

Y1 - 2011/3/25

N2 - 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 datapath of OR1200, an open source embedded processor. We demonstrate the enhanced scalability of SHARPE by applying compositional reasoning for probabilistic model checking.

AB - 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 datapath of OR1200, an open source embedded processor. We demonstrate the enhanced scalability of SHARPE by applying compositional reasoning for probabilistic model checking.

UR - http://www.scopus.com/inward/record.url?scp=79952858287&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79952858287&partnerID=8YFLogxK

U2 - 10.1109/VLSID.2011.48

DO - 10.1109/VLSID.2011.48

M3 - Conference contribution

SN - 9780769543482

T3 - Proceedings of the IEEE International Conference on VLSI Design

SP - 58

EP - 63

BT - Proceedings - 24th International Conference on VLSI Design, VLSI Design 2011, Held Jointly with 10th International Conference on Embedded Systems

ER -