Formal Model for System-Level Power Management Design

Mirela Simonovi\'c1,2,a, Vojin Zivojnovi\'c1,b and Lazar Saranovac2,c
1Aggios Inc.
2School of Electrical Engineering, University of Belgrade, Serbia


In this paper we present a new formal model, called p-FSM, for system-level power management design. The p-FSM is a modular, compositional, hierarchical, and unified model for hardware and software components. The model encapsulates power management control mechanisms, operating states and properties of a component that affect power, energy and thermal aspects of the system. Inter-component dependencies are modeled through a component-based interface. By connecting multiple p-FSMs we gradually compose the model of the whole system which ensures correct-by-construction system-level control sequencing. The model can also be used to formally verify the functional correctness of the power management design.

Full Text (PDF)