Modem, high performance microprocessors are extremely complex machines which require substantial validation effort to ensure functional correctness prior to tapeout. Generating the corner cases to test these designs is a mostly manual process, where completion is hard to judge. Experience shows that the errors that are caught late in the design, many post-silicon, are interactions between different components in very improbable corner case situations. In this paper we present a technique that targets such error-causing interactions by automatically generat- ing test vectors that will cause the processor to exercise all transitions of the control logic in simulation. We use techniques from formal verification to derive transition tours of a fully enumerated state graph of the control logic of the processor. Our system works from a Verilog description of the original machine and is currently being used to validate an embedded dual-issue processor in the node controller of the Stanford FLASH Multiprocessor. Modeling the processor control results in 200K states and an 8M instruction trace to check all transitions of control arcs.