Formal semantics analysis for VHDL RTL synthesis

摘要

A set of synthesis-oriented semantic models, which is named structural semantics, for VHDL synthesis subset is presented in this paper. The principle of this semantics is the definition of course. In addition, we give the definition of course set, which is used to interpret the VHDL input description. In addition, it is also the basis of language level transformation and optimization. Correctness of any optimization algorithm can be judged explicitly by means of this semantic method. Some relevant definitions and theorems are presented too in this paper. The purpose of presenting this semantics is to guide the language level optimization, which guarantee the correctness of transformation (rewrite). The semantics was used to prove three important theorems, i.e. common sub-expression extraction, loop unrolling and common factoring, which were used in language level optimization.