Automatic Compositional Reasoning for Probabilistic Model Checking of Hardware Designs

Adaptive techniques like voltage and frequency scaling, process variations and the randomness of input data contribute signi cantly 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 ...

• Type: Journal
• Year: 2010
• Where: QEST
• Authors: Jayanand Asok Kumar, Shobha Vasudevan
• Keywords: Design, Modeling And Simulation, Performance Metrics, Probabilistic Model, QEST 2010