Automatic compositional reasoning for probabilistic model checking of hardware designs

Jayanand Asok Kumar, Shobha Vasudevan

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

Abstract

Adaptive techniques like voltage and frequency scaling, process variations and the randomness of input data contribute significantly to the statistical aspect of contemporary hardware designs. Therefore, the performance metrics of such designs are also statistical in nature. In previous work, we have employed probabilistic model checking to rigorously evaluate the statistical performance of hardware designs. In this paper, we present an automatic compositional reasoning technique to improve the scalability of probabilistic model checking of hardware systems. We partition the set of system observables into disjoint subsets and use them to structurally decompose the system into smaller components. We employ an assume-guarantee form of reasoning and analyze the space of environmental constraints using a value-based case splitting approach. We split the space of values of all the observables of one component into separate value-based cases. We provide an argument for the correctness of our technique. We illustrate the effectiveness of our technique by making probabilistic model checking feasible for evaluating performance metrics such as delay and Bit Error Rate (BER) of non-trivial hardware designs that we use as case studies. For example, we are able to determine the statistical delay of a 64-bit adder design with over 1040 states. We use PRISM as the probabilistic model checking engine in all our experiments.

Original languageEnglish (US)
Title of host publicationProceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010
Pages143-152
Number of pages10
DOIs
StatePublished - Dec 2 2010
Event7th International Conference on the Quantitative Evaluation of Systems, QEST 2010 - Williamsburg, VA, United States
Duration: Sep 15 2010Sep 18 2010

Publication series

NameProceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010

Other

Other7th International Conference on the Quantitative Evaluation of Systems, QEST 2010
CountryUnited States
CityWilliamsburg, VA
Period9/15/109/18/10

Fingerprint

Model checking
Hardware
Adders
Bit error rate
Scalability
Statistical Models
Engines
Electric potential
Experiments

ASJC Scopus subject areas

  • Control and Systems Engineering

Cite this

Kumar, J. A., & Vasudevan, S. (2010). Automatic compositional reasoning for probabilistic model checking of hardware designs. In Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010 (pp. 143-152). [5600395] (Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010). https://doi.org/10.1109/QEST.2010.25

Automatic compositional reasoning for probabilistic model checking of hardware designs. / Kumar, Jayanand Asok; Vasudevan, Shobha.

Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010. 2010. p. 143-152 5600395 (Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010).

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

Kumar, JA & Vasudevan, S 2010, Automatic compositional reasoning for probabilistic model checking of hardware designs. in Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010., 5600395, Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010, pp. 143-152, 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010, Williamsburg, VA, United States, 9/15/10. https://doi.org/10.1109/QEST.2010.25
Kumar JA, Vasudevan S. Automatic compositional reasoning for probabilistic model checking of hardware designs. In Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010. 2010. p. 143-152. 5600395. (Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010). https://doi.org/10.1109/QEST.2010.25
Kumar, Jayanand Asok ; Vasudevan, Shobha. / Automatic compositional reasoning for probabilistic model checking of hardware designs. Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010. 2010. pp. 143-152 (Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010).
@inproceedings{8ba8e6dc43b94a38a9b264ee582cd378,
title = "Automatic compositional reasoning for probabilistic model checking of hardware designs",
abstract = "Adaptive techniques like voltage and frequency scaling, process variations and the randomness of input data contribute significantly to the statistical aspect of contemporary hardware designs. Therefore, the performance metrics of such designs are also statistical in nature. In previous work, we have employed probabilistic model checking to rigorously evaluate the statistical performance of hardware designs. In this paper, we present an automatic compositional reasoning technique to improve the scalability of probabilistic model checking of hardware systems. We partition the set of system observables into disjoint subsets and use them to structurally decompose the system into smaller components. We employ an assume-guarantee form of reasoning and analyze the space of environmental constraints using a value-based case splitting approach. We split the space of values of all the observables of one component into separate value-based cases. We provide an argument for the correctness of our technique. We illustrate the effectiveness of our technique by making probabilistic model checking feasible for evaluating performance metrics such as delay and Bit Error Rate (BER) of non-trivial hardware designs that we use as case studies. For example, we are able to determine the statistical delay of a 64-bit adder design with over 1040 states. We use PRISM as the probabilistic model checking engine in all our experiments.",
author = "Kumar, {Jayanand Asok} and Shobha Vasudevan",
year = "2010",
month = "12",
day = "2",
doi = "10.1109/QEST.2010.25",
language = "English (US)",
isbn = "9780769541884",
series = "Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010",
pages = "143--152",
booktitle = "Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010",

}

TY - GEN

T1 - Automatic compositional reasoning for probabilistic model checking of hardware designs

AU - Kumar, Jayanand Asok

AU - Vasudevan, Shobha

PY - 2010/12/2

Y1 - 2010/12/2

N2 - Adaptive techniques like voltage and frequency scaling, process variations and the randomness of input data contribute significantly to the statistical aspect of contemporary hardware designs. Therefore, the performance metrics of such designs are also statistical in nature. In previous work, we have employed probabilistic model checking to rigorously evaluate the statistical performance of hardware designs. In this paper, we present an automatic compositional reasoning technique to improve the scalability of probabilistic model checking of hardware systems. We partition the set of system observables into disjoint subsets and use them to structurally decompose the system into smaller components. We employ an assume-guarantee form of reasoning and analyze the space of environmental constraints using a value-based case splitting approach. We split the space of values of all the observables of one component into separate value-based cases. We provide an argument for the correctness of our technique. We illustrate the effectiveness of our technique by making probabilistic model checking feasible for evaluating performance metrics such as delay and Bit Error Rate (BER) of non-trivial hardware designs that we use as case studies. For example, we are able to determine the statistical delay of a 64-bit adder design with over 1040 states. We use PRISM as the probabilistic model checking engine in all our experiments.

AB - Adaptive techniques like voltage and frequency scaling, process variations and the randomness of input data contribute significantly to the statistical aspect of contemporary hardware designs. Therefore, the performance metrics of such designs are also statistical in nature. In previous work, we have employed probabilistic model checking to rigorously evaluate the statistical performance of hardware designs. In this paper, we present an automatic compositional reasoning technique to improve the scalability of probabilistic model checking of hardware systems. We partition the set of system observables into disjoint subsets and use them to structurally decompose the system into smaller components. We employ an assume-guarantee form of reasoning and analyze the space of environmental constraints using a value-based case splitting approach. We split the space of values of all the observables of one component into separate value-based cases. We provide an argument for the correctness of our technique. We illustrate the effectiveness of our technique by making probabilistic model checking feasible for evaluating performance metrics such as delay and Bit Error Rate (BER) of non-trivial hardware designs that we use as case studies. For example, we are able to determine the statistical delay of a 64-bit adder design with over 1040 states. We use PRISM as the probabilistic model checking engine in all our experiments.

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

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

U2 - 10.1109/QEST.2010.25

DO - 10.1109/QEST.2010.25

M3 - Conference contribution

SN - 9780769541884

T3 - Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010

SP - 143

EP - 152

BT - Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010

ER -