Formal Model for System-Level Power Management Design
Mirela Simonovi\'c1,2,a, Vojin Zivojnovi\'c1,b and Lazar Saranovac2,c
1Aggios Inc.
amirela.simonovic@aggios.com
cvojin.zivojnovic@aggios.com
claza@el.etf.rs
2School of Electrical Engineering, University of Belgrade, Serbia
ABSTRACT
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.
