Summary: The design of control units of modern processors is quite complex due to many speed-up techniques like pipelining and out-of-order execution. The existing approaches to formal verification of processor designs are applicable to very high level descriptions that ignore timing details of control signals. In this paper, we propose an approach for verification of detailed design of processors. Our approach suggests the use of Esterel language which has rieh constructs for succinct and modular description of control. The Esterel Simulation tool Xes and verification tools Xeve and FcTools can be used effectively to catch minor bugs as well as subtle timing errors. As an illustration, we have developed an Esterel implementation of DLX pipeline control and verified certain crucial properties.