Formalization of finite state machines with data path for the verification of high-level synthesis

This research aims at verifying the abstract specification levels of standard hardware description languages (we use VHDL [IE931). HLS translates a behavioral description, written as one or more processes, into an abstract automaton in which the states correspond to decision and synchronization points, and operations of the behavioral algorithm are executed on the state transitions [JD97]. After the allocation of the functional units to the operations, and their scheduling, the system is modeled as the interconnection of two modules: (1) an operative (or data) part, which contains the data registers, operators, multiplexers and busses; (2) a control part, which generates the control signals of the operative part, and the sequence of steps to perform the overall computation