Verification of VHDL designs using VAL

VAL (VHDL Annotation Language) uses a small number of language constructs to annotate VHDL (VHSIC Hardware Description Language) hardware descriptions. VAL annotations, added to the VHDL entity declaration in the form of formal comments, express intended behavior common to all architectural bodies of the entity. The result is a simple but expressive language extension of VHDL with possible applications to automatic checking of VHDL simulations, hierarchical design, and automatic verification of hardware designs in VHDL. An overview is given of design checking using VAL. VAL is described in detail and it is shown how VAL annotations are used to generate constraints on a VHDL simulation. A brief overview of the VAL transformer demonstrates the feasibility of the design. Some observations based on experience with VAL to date and areas for future work are considered.<>