Translation Validation for Synchronous Data-Flow Specification in the SIGNAL Compiler
Abstract
We present a method to construct a validator based on translation validation approach to prove the value-equivalence of variables in the compilation of the Signal compiler. The computation of output signals in a Signal program and their counterparts in the generated C code is represented by a Synchronous Data-flow Value-Graph (Sdvg). Our validator proves that every output signal and its counterpart variable have the same values by transforming the Sdvg graph.
Origin : Files produced by the author(s)
Loading...
