Embedded Software Verification and Debugging

Today the debugging and verification of complex system-on-a-chips cannot be considered only on hardware modules anymore. The amount of software has increased significantly over the last years and therefore, the co-debugging and the co-verification of hardware and embedded software modules have become of fundamental importance. This book addresses the current state-of-the-art of hardware/software co-debugging and co-verification methodologies. This chapter intends to give an overview about these main topics and concepts.

This chapter presents an overview of different embedded software debug techniques enabled by recent advances in the EDA tools allowing either interactive or playback type debug of software and hardware (RTL) in a simulation of a complete system. Most of the methods and ideas described here present a summary of different approaches applied within our day-to-day work at Cadence\({\textregistered }\) Design Systems. With growing complexity of software and hardware solutions and an increasing push at reducing the time-to-market, it has become very important to simulate or run as much of the target system and software, as early as possible in order to enable system-level validation of the complete design and evaluation of any potential risks or limitations, that may not be obvious at unit level (e.g., considering the CPU and each piece of hardware IP in isolation). New SoC systems bring increasing integration level of both software and hardware elements and the final product requires all of the components to interact as designed, in order to satisfy the growing user expectations for speed, efficiency, and reliability. Furthermore software complexity in the embedded systems has recently exploded as more functionality is driven by microcontrollers with reprogrammable firmware allowing addition of features to products after release.

Bugs vary in their root causes and their revealed behaviors; some may cause a crash or a core dump, while others may cause an incorrect or missing output or an unexpected behavior. Moreover, most bugs are revealed long after their actual cause. A variable might be assigned early in the execution, and that value may cause a bug far from that last assigned place. This often requires users to manually track heuristic information over different execution states. This information may include a trace of specific variables’ values and their assigned locations, functions and their returned values, and detailed execution paths. This chapter introduces Dynamic Temporal Assertions (DTA) into the conventional source-level debugging session. It extends a typical gdb-like source-level debugger named UDB with on-the-fly temporal assertions. Each assertion is capable of: (1) validating a sequence of execution states, named temporal interval, and (2) referencing out-of-scope variables, which may not be live in the execution state at evaluation time. These new DTA assertions are not bounded by the limitations of ordinary in-code assertions such as locality, temporality, and static hardwiring into the source code. Furthermore, they advance typical interactive debugging sessions and their conditional breakpoints and watchpoints.

Embedded systems are used everywhere in our daily lives. About 90% of the produced microprocessors are used in embedded systems. Embedded systems get more and more dominated by software. Bugs remain in the software and can often be observed for the first time only in late development phases. It is difficult to reproduce bugs in embedded systems based on test reports. Our proposed automated bug reproduction concept is capable of handling sensor inputs as well as thread schedules. It reduces the manual effort while debugging a reproduced bug by applying dynamic verification during replay. This chapter shows the implementation of assertions and presents anomaly detection techniques to locate the root-causes of bugs. Anomalies can be detected by comparing executions which cause the bug with executions which do not cause the bug. Interferences between two executions which can be compared have to be detected. Using partitioning techniques, we explain coverage-based analysis and metrics as well as invariant-based analysis. The monitoring of the software for these analyses may cause a high overhead and thus may result in long monitoring times. Therefore, we show how monitoring can be accelerated by hierarchical refinement. Most of the available automated bug reproduction and dynamic verification tools are only applicable on specific platforms. Debugging tools, like the GDB, are usually the first tools which are available for new embedded platforms. Therefore, our tool is implemented based on the GDB. We present a tool for automated bug reproduction and efficient dynamic verification implemented with a debugger tool.

Model-Driven Development (MDD) is slowly superseding traditional ways of developing embedded software. In line with the MDD, debugging real-time embedded software systems (RTESS) and visualizing their behavior using models, such as UML diagrams, is becoming a reality. However, the additional overhead, introduced by the existing techniques, presents a hurdle in applying model-based debugging for resource constrained, deeply embedded systems. To address this gap, we discuss a model-based debugging methodology for RTESS, which employs a target debugger on the host and runtime monitoring mechanisms on the target. Two variants of a time and memory-aware runtime monitoring methodology, namely, (a) software and (b) on-chip monitoring, are discussed. Using the proposed approach, the target behavior can be visualized in real time using UML sequence and timing diagrams with minimal, generic overhead in the target. An empirical evaluation, based on a prototype implementation of the proposed runtime monitoring mechanisms, is presented. Performance metrics, such as the instrumentation overhead and time spent in the monitoring routine, are discussed.

Cyber-physical systems (CPS) are complex systems including computing and communication together with control of the physical environment. They must be safe and secure, since they are often used in critical applications involving lives and expensive infrastructure, such as mass transportation, power plants, or medical equipments. The high interaction of these systems with the environment demands that it be comprised of numerous and varied devices. The control of these devices is accomplished by a hardware-dependent software layer highly specialized, which is commonly a source of error that can affect the operation of the entire system. Thus, this approach proposes a technique for specification and runtime monitoring of high-level communication between devices and drivers, which is based on finite-state machines and temporal properties. Supported by a tool set developed in this context, this approach provides a complete workflow, including a domain-specific language, called TDevC, as front-end, followed by the validation and optimization of the high-level models, synthesis from models to real hardware monitors (SystemVerilog) or simulation-based monitoring mechanism for virtual platforms (SystemC). The proposed approach is evaluated with some real-life examples including IP controller of an Ethernet device, a serial port, and a temperature controller using sensors and actuators to validate all the phases of the workflow of the proposed approach. All violation of temporal properties expressed for each device has been detected successfully, including properties involving different layers of the software.

We present a novel proof by induction algorithm, which combines k-induction with invariants to model check embedded C software with bounded and unbounded loops. The k-induction algorithm consists of three cases: in the base case, we aim to find a counterexample with up to k loop unwindings; in the forward condition, we check whether loops have been fully unrolled and that the safety property P holds in all states reachable within k unwindings; and in the inductive step, we check that whenever P holds for k unwindings, it also holds after the next unwinding of the system. For each step of the k-induction algorithm, we infer invariants using affine constraints (i.e., polyhedral) to specify pre and postconditions. The algorithm was implemented in two different ways, with and without invariants using polyhedral, and the results were compared. Experimental results show that both forms can handle a wide variety of safety properties in typical embedded software applications from telecommunications, control systems, and medical devices domains; however, the k-induction algorithm adopting polyhedral solves more verification tasks, which demonstrate an improvement of the induction algorithm effectiveness.

The verification of embedded software has become an important subject over the last years. However, neither standalone verification approaches, like simulation-based/formal verification, nor state-of-the-art semiformal verification approaches are able to verify large and complex-embedded software with or without hardware dependencies. This work presents a scalable hybrid verification approach for the verification of embedded software using a semiformal algorithm optimized with static parameter assignment (SPA). These algorithms and methodologies like SPA and counterexample guided simulation are used to combine simulation-based and formal verification in a new way. SPA offers a method to interact between dynamic and static verification approaches based on an automated ranking determination of possible function parameters according to the impact on the model size. Furthermore, SPA inserts initialization code for specific function parameters into the source code under test and supports model building and optimization algorithms to reduce the state space. We have successfully applied this optimized hybrid verification methodology to embedded software applications: Motorola’s Powerstone Benchmark suite and a complex automotive industrial embedded software. The results show that our approach scales better than standalone software model checkers to reach deep state spaces.