Existing timing verification tools can provide methodologies for identifying and optimizing critical true paths in an embedded combinational module; however, the problem of justifying these paths to the chip level is a very difficult one. This paper addresses the problem of timing verification at the entire chip level. We use a critical path tool, CRITIC, to obtain critical paths in an embedded combinational module. In order to reduce the complexity of checking whether the module-level critical path is indeed critical at the chip level, we use techniques from formal verification to extract the control behavior of the circuit, and check whether there is any control sequence which will justify the path to the chip level. The results of the experiments on several processor designs show that our approach is very effective in large sequential circuits such as microprocessors, where conventional ATPG techniques require inordinate amounts of CPU time. The experiments also show that the execution time remains reasonable as the circuit size increases, since we deal with a reduced control space rather than the entire state space of the circuit.