A Framework for Static Analysis of VHDL Code

Abstract

Software in real time systems underlies strict timing constraints.
These are among others hard deadlines regarding
the worst-case execution time (WCET) of the application.
Thus, the computation of a safe and precise WCET is a key
issue1 for validating the behavior of safety-critical systems,
e.g. the flight control system in avionics or the airbag control
software in the automotive industry.
Saarland University and AbsInt Angewandte Informatik
GmbH have developed a successful approach for computing
the WCET of a task. The resulting tool, called aiT, is
based on the abstract interpretation [3, 4] of timing models
of the processor and its periphery. Such timing models
are hand-crafted and therefore error-prone. Additionally
the modeling requires a hard engineering effort, so that the
development process is very time consuming.
Because modern processors are synthesized from a formal
hardware specification, e.g., in VHDL or VERILOG, the
hand-crafted timing model can be developed by manually
analyzing the processor specification.
Due to the complexity of this step, there is a need for support
tools that ease the creation of analyzes on such specifi-
cations. This paper introduces the primer work on a framework
for static analyzes on VHDL.