VeSUV is a transformation tool that encodes embedded systems designs written in the hardware/software co-design language SystemC into PVL, the internal language of VerCors. It creates an encoding of both the design and the SystemC scheduling semantics to generate a PVL program that is semantically equivalent to the original SystemC design. VeSUV also generates basic specifications for the encoded program. The user can then add further specifications and verify them normally with VerCors.