We present our methodology to formally prove properties of VHDL designs by first translating them to Rocq. Because our translation keeps all parameters (a.k.a. generics) uninstantiated, we develop algorithms that check the correctness of given VHDL designs under all parameter valuations. These checks detect whether there are combinatorial loops, missing or multiple signal assignments, wrong integer assignments with respect to specified ranges, array access and assignment errors, and integer overflows for some valuation of the parameters. Once these checks pass, we show how to compute a topological ordering of the signal assignments that is valid for all parameter valuations, and which allows us to translate to simple Rocq functions that capture the functional behaviors of the VHDL designs given as input. We further show to address pipelined circuits and present an application on the verification of a FPU.