Symbolic functional vector generation for VHDL specifications

Verification of the functional correctness of VHDL specifications is one of the primary and most time consuming tasks 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 allows 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 interconnected to other processes. If this is not the case, the analysis of the nonapplicable 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.