Abstract
This paper describes VSYML, a symbolic simulator that extracts formal models from VHDL descriptions. The generated models are adequate to formal reasoning in various frameworks. VSYML is a reimplementation of its ancestor Theosim; it brings various improvements e.g., with regard to arrays and other complex data types.