version 1.7, 2009/06/28 15:01:57
|
version 1.8, 2009/06/28 16:26:25
|
Line 170 hardware/software and pure software tech
|
Line 170 hardware/software and pure software tech
|
|
|
\paragraph*{WP2 - Verified Compilation} |
\paragraph*{WP2 - Verified Compilation} |
|
|
translation verification, specification of semantics of IRs solving |
Suitable semantics are necessary which support efficient translation |
subproblems. |
validation or support easy verification of a compiler. We will research |
|
into different semantics and into mappings between the semantics of our |
|
processor description language \cite{BrEbKr07} and a compiler backend |
|
semantics, intermediate representation semantics (compatible to LLVM) and |
|
source language semantics. The main research will be on verification and |
|
translation validation for all kinds of compiler optimizations. |
|
|
|
\begin{itemize} |
|
\item Evaluate different semantics regarding suitability for compiler |
|
verification and translation validation, eventually develop new |
|
semantics |
|
\item Develop a translator for an automatic mapping from our processor |
|
description language into verification semantics |
|
\item Develop a validation system from the intermediate representation |
|
(LLVM) to the processor semantics |
|
\item Develop a validation system from the source language (C) to the |
|
intermediate representation (LLVM) |
|
\item Research into verification and translation validation for different |
|
frontend and backend optimizations |
|
\end{itemize} |
|
|
\paragraph*{WP3 - Worst Case Ececution Time Analysis} |
\paragraph*{WP3 - Worst Case Ececution Time Analysis} |
|
|