Generation of Formal CPU Profiles for Embedded Systems

The advent of IoT devices cleared the way for embedded systems to be used everywhere in daily life. These systems typically have very strict constraints on area and power consumption that are difficult, if not infeasible, to meet for commercial off-the-shelf (COTS) processors. At the same time, custom system designs are often not a viable option, due to price limits that force companies to keep design effort, cost and time to a minimum.This work proposes a highly automated method for a formal analysis of signal activity in a COTS processor during software (SW) execution. Our analysis provides a thorough understanding on the interaction between Hardware (HW) and SW with bit-level and clock cycle accuracy. Designers can use this knowledge to locate and exploit the identified behavioral patterns for a wide range of HW improvements. In this paper, we focus on qualifying switching activity by analyzing the controllability of signals. When applied to a SuperH-2 processor for different softwares, we were able to reduce its area by up to 69% and power by up to 56%. We demonstrate the scalability of this method on an industry-scale software system for IoT with about 1.7k lines of C code.