1. A method for generating a test program for a processor, comprising: receiving a formal description of an instruction set for the processor; receiving a formal description of a test specification; and generating a test program using the formal description of the instruction set and the formal description of the test specification.