The adaptation of a software verification technique to hardware design verification is proposed. Current testing strategies can be augmented by examining the consistency of the design, as represented in a Computer Hardware Description Language (CHDL) specification, with assertions characterizing the desired function of the design. The verification process consists of transforming the specification into a more readily examined set of constructs, determining axioms appropriate for the given application, generating assertions, and analyzing the specification using the inductive assertion method. Verification is demonstrated on several types of hardware designs, including arithmetic modules and datapath designs, and advantages of the technique for different applications are discussed. |