Formal analysis of single WAIT VHDL processes for semantic based synthesis

This paper deals with the formal identification of flip-flops and latches within VHDL descriptions of hardware systems. Due to the simulation based semantics of VHDL, the existing synthesis tools rely on explicit templates to guarantee memorizing element inference. The approach proposed here is based on a formal representation of VHDL in terms of Interpreted Petri Nets. A Petri Net preserving the simulation semantic is build as a result of of VHDL compilation and then reduced to a unique minimal form. A set of equations is extracted and a formal analysis is performed on all cyclic symbol assignments. The result is a RTL VHDL description, synthesizable by any existing synthesis tools. This methodology has been implemented and is illustrated on a set of simple and representative descriptions.