Verification of the functional correctness of VHDL specifications is one of the primary and most time consuming task of design. However, it must necessarily be an incomplete task since it is impossible to completely exercise the specification by exhaustively applying all input patterns.The paper aims at presenting a two-step strategy based on symbolic analysis of the VHDL specification, using a behavioral fault model. First, we generate a reduced number of functional test vectors for each process of the specification which allow complete code statement coverage and bit coverage, allowing the identification of possible redundancies in the VHDL process.Then, through the definition of a controllability measure, we verify if these functional test vectors can be applied to the process inputs when it is interconnected to other processes. If this is not the case, the analysis of the non-applicable inputs provides identification of possible code redundancies and design errors. Experimental results show that bit coverage provides complete statement coverage and a more detailed identification of possible design errors.