Scaling probabilistic timing verification of hardware using abstractions in design source code

Jayanand Asok Kumar, Lingyi Liu, Shobha Vasudevan

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

Abstract

Sources of randomness such as physical process variations and input pattern variations make hardware timing a statistical measure. It is desirable to verify statistical timing properties at the higher levels of design such as the Register Transfer Level (RTL). The RTL design can be modeled as a Discrete Time Markov Chain (DTMC) and probabilistic model checking then applied to verify that the DTMC satisfies a desired timing specification. However, we find that such an approach does not scale beyond 10 10 states. In this paper, we introduce an abstraction methodology to scale this approach to large designs. Instead of considering the entire space of data values that can be assigned to the design input variables, we perform a value-based interval abstraction by considering only those intervals of input values that are relevant to a given timing property. We employ symbolic execution on the RTL source code to automatically derive such intervals for the design inputs, with respect to a given timing property. We use these intervals to construct smaller abstract DTMCs and thereby make the corresponding probabilistic model checking problems more tractable. We show that our abstraction is sound since we do not remove any probabilistic behavior that is relevant to the property of interest. We demonstrate the effectiveness of our technique using multiple designs used in communication systems such as FFT, filters and several modules of a real world H.264 decoder. We use our technique to successfully verify timing of an H.264 module, for which the concrete model contains more that 10 80 states, by constructing an abstract model with approximately only 10 10 states.

Original languageEnglish (US)
Title of host publication2011 Formal Methods in Computer-Aided Design, FMCAD 2011
Pages196-205
Number of pages10
StatePublished - Dec 1 2011
Event2011 Formal Methods in Computer-Aided Design, FMCAD 2011 - Austin, TX, United States
Duration: Oct 30 2011Nov 2 2011

Publication series

Name2011 Formal Methods in Computer-Aided Design, FMCAD 2011

Other

Other2011 Formal Methods in Computer-Aided Design, FMCAD 2011
CountryUnited States
CityAustin, TX
Period10/30/1111/2/11

Fingerprint

Hardware
Model checking
Markov processes
Fast Fourier transforms
Communication systems
Acoustic waves
Specifications
Statistical Models

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Computer Graphics and Computer-Aided Design

Cite this

Kumar, J. A., Liu, L., & Vasudevan, S. (2011). Scaling probabilistic timing verification of hardware using abstractions in design source code. In 2011 Formal Methods in Computer-Aided Design, FMCAD 2011 (pp. 196-205). [6148897] (2011 Formal Methods in Computer-Aided Design, FMCAD 2011).

Scaling probabilistic timing verification of hardware using abstractions in design source code. / Kumar, Jayanand Asok; Liu, Lingyi; Vasudevan, Shobha.

2011 Formal Methods in Computer-Aided Design, FMCAD 2011. 2011. p. 196-205 6148897 (2011 Formal Methods in Computer-Aided Design, FMCAD 2011).

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

Kumar, JA, Liu, L & Vasudevan, S 2011, Scaling probabilistic timing verification of hardware using abstractions in design source code. in 2011 Formal Methods in Computer-Aided Design, FMCAD 2011., 6148897, 2011 Formal Methods in Computer-Aided Design, FMCAD 2011, pp. 196-205, 2011 Formal Methods in Computer-Aided Design, FMCAD 2011, Austin, TX, United States, 10/30/11.
Kumar JA, Liu L, Vasudevan S. Scaling probabilistic timing verification of hardware using abstractions in design source code. In 2011 Formal Methods in Computer-Aided Design, FMCAD 2011. 2011. p. 196-205. 6148897. (2011 Formal Methods in Computer-Aided Design, FMCAD 2011).
Kumar, Jayanand Asok ; Liu, Lingyi ; Vasudevan, Shobha. / Scaling probabilistic timing verification of hardware using abstractions in design source code. 2011 Formal Methods in Computer-Aided Design, FMCAD 2011. 2011. pp. 196-205 (2011 Formal Methods in Computer-Aided Design, FMCAD 2011).
@inproceedings{3dabfba4c129498480cbdc68e3bb0a92,
title = "Scaling probabilistic timing verification of hardware using abstractions in design source code",
abstract = "Sources of randomness such as physical process variations and input pattern variations make hardware timing a statistical measure. It is desirable to verify statistical timing properties at the higher levels of design such as the Register Transfer Level (RTL). The RTL design can be modeled as a Discrete Time Markov Chain (DTMC) and probabilistic model checking then applied to verify that the DTMC satisfies a desired timing specification. However, we find that such an approach does not scale beyond 10 10 states. In this paper, we introduce an abstraction methodology to scale this approach to large designs. Instead of considering the entire space of data values that can be assigned to the design input variables, we perform a value-based interval abstraction by considering only those intervals of input values that are relevant to a given timing property. We employ symbolic execution on the RTL source code to automatically derive such intervals for the design inputs, with respect to a given timing property. We use these intervals to construct smaller abstract DTMCs and thereby make the corresponding probabilistic model checking problems more tractable. We show that our abstraction is sound since we do not remove any probabilistic behavior that is relevant to the property of interest. We demonstrate the effectiveness of our technique using multiple designs used in communication systems such as FFT, filters and several modules of a real world H.264 decoder. We use our technique to successfully verify timing of an H.264 module, for which the concrete model contains more that 10 80 states, by constructing an abstract model with approximately only 10 10 states.",
author = "Kumar, {Jayanand Asok} and Lingyi Liu and Shobha Vasudevan",
year = "2011",
month = "12",
day = "1",
language = "English (US)",
isbn = "9781467308960",
series = "2011 Formal Methods in Computer-Aided Design, FMCAD 2011",
pages = "196--205",
booktitle = "2011 Formal Methods in Computer-Aided Design, FMCAD 2011",

}

TY - GEN

T1 - Scaling probabilistic timing verification of hardware using abstractions in design source code

AU - Kumar, Jayanand Asok

AU - Liu, Lingyi

AU - Vasudevan, Shobha

PY - 2011/12/1

Y1 - 2011/12/1

N2 - Sources of randomness such as physical process variations and input pattern variations make hardware timing a statistical measure. It is desirable to verify statistical timing properties at the higher levels of design such as the Register Transfer Level (RTL). The RTL design can be modeled as a Discrete Time Markov Chain (DTMC) and probabilistic model checking then applied to verify that the DTMC satisfies a desired timing specification. However, we find that such an approach does not scale beyond 10 10 states. In this paper, we introduce an abstraction methodology to scale this approach to large designs. Instead of considering the entire space of data values that can be assigned to the design input variables, we perform a value-based interval abstraction by considering only those intervals of input values that are relevant to a given timing property. We employ symbolic execution on the RTL source code to automatically derive such intervals for the design inputs, with respect to a given timing property. We use these intervals to construct smaller abstract DTMCs and thereby make the corresponding probabilistic model checking problems more tractable. We show that our abstraction is sound since we do not remove any probabilistic behavior that is relevant to the property of interest. We demonstrate the effectiveness of our technique using multiple designs used in communication systems such as FFT, filters and several modules of a real world H.264 decoder. We use our technique to successfully verify timing of an H.264 module, for which the concrete model contains more that 10 80 states, by constructing an abstract model with approximately only 10 10 states.

AB - Sources of randomness such as physical process variations and input pattern variations make hardware timing a statistical measure. It is desirable to verify statistical timing properties at the higher levels of design such as the Register Transfer Level (RTL). The RTL design can be modeled as a Discrete Time Markov Chain (DTMC) and probabilistic model checking then applied to verify that the DTMC satisfies a desired timing specification. However, we find that such an approach does not scale beyond 10 10 states. In this paper, we introduce an abstraction methodology to scale this approach to large designs. Instead of considering the entire space of data values that can be assigned to the design input variables, we perform a value-based interval abstraction by considering only those intervals of input values that are relevant to a given timing property. We employ symbolic execution on the RTL source code to automatically derive such intervals for the design inputs, with respect to a given timing property. We use these intervals to construct smaller abstract DTMCs and thereby make the corresponding probabilistic model checking problems more tractable. We show that our abstraction is sound since we do not remove any probabilistic behavior that is relevant to the property of interest. We demonstrate the effectiveness of our technique using multiple designs used in communication systems such as FFT, filters and several modules of a real world H.264 decoder. We use our technique to successfully verify timing of an H.264 module, for which the concrete model contains more that 10 80 states, by constructing an abstract model with approximately only 10 10 states.

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

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

M3 - Conference contribution

SN - 9781467308960

T3 - 2011 Formal Methods in Computer-Aided Design, FMCAD 2011

SP - 196

EP - 205

BT - 2011 Formal Methods in Computer-Aided Design, FMCAD 2011

ER -