Functional verification is widely acknowledged as a major bottleneck in microprocessor design. While early work on specification driven functional test program generation has proposed several promising ideas, many challenges remain in applying them to realistic embedded processors. We present a graph coverage based functional test program generation approach for pipelined processors. The proposed methodology makes three important contributions. First, it automatically generates the graph model of the pipelined processor from the speci.cation using functional abstraction. Second, it generates functional test programs based on the coverage of the pipeline behavior. Finally, the test generation time is drastically reduced due to the use of module level property checking. We applied this methodology on the DLX processor to demonstrate the usefulness of our approach.