Formal extraction of memorizing elements for sequential VHDL synthesis

We present a method for latch and flip flop recognition 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 is based on a formal representation of VHDL in terms of interpreted Petri nets (IPN). After the compilation of the description, a Petri net preserving the simulation semantics is built. In order to simplify the formal recognition of the memorizing elements appearing in the description, the Petri net is reduced to a unique minimal form. Ultimately a set of equations can be extracted, and a formal analysis is performed on all cyclic VHDL symbol assignments. This methodology has been implemented and is illustrated on a representative set of simple VHDL descriptions