Translation Validation of Code Generation from the SIGNAL Data-Flow Language to Verilog

The SIGNAL is a high-level synchronous data-flow language for the design and implementation of safety-critical embedded systems. It provides a unified framework for specification, modeling, formal analysis, and automatic code generation for different general-purpose languages like Java, C, and C++. However, fully implemented and verified open source tool for code generation from SIGNAL to Hardware Description Language (HDL) is not available. This paper describes the formal verification of the generated Verilog code from the SIGNAL language. Proving the correctness of generated code is very important when it is for safety-critical embedded systems. We use the translation validation technique for verifying the correctness of the generated code. In this approach, the Polychrony Toolset builds the models of source SIGNALprograms with its associated model checker SIGALI. The open source tool Yosys generates models for target Verilog programs in the SMT-LIB standard format. We transform the model generated by Yosys to the model accepted by the SIGALI model checker. Finally, we use the SIGALI model checker to validate the translation by symbolic simulation between both source and target program models. The target program may have fewer behaviors than the source program therefore if the model of the target program implies the model of the source program, it means the target program preserves the semantics of the source program, and the translation is correct.