Automatic functional test program generation for pipelined processors using model checking

Formal techniques offer an opportunity to significantly reduce the cost of microprocessor verification. We propose a model checking based approach to automatically generate functional test programs for pipelined processors. We specify the processor architecture in an Architecture Description Language (ADL). The processor model is extracted from the ADL specification. Specific properties are applied to the processor model using SMV model checker to generate test programs. We applied this methodology on a single-issue DLX processor to demonstrate the usefulness of our approach.