Constrained random simulation is a widespread technique used to perform functional verification on complex digital designs, because it can generate simulation vectors at a very high rate. However, the generation of high-coverage tests remains a major challenge even in light of this high performance. In this paper we present Guido, a hybrid verification software that uses formal verification techniques to guide the simulation towards a verification goal. Guido is novel in that 1) it guides the simulation by means of a distance function derived from the circuit structure, and 2) it has a trace sequence controller that monitors and controls the direction of the simulation by striking a balance between random chance and controlled hill-climbing. We present experimental results indicating that Guido can tackle complex designs, including a picoJava microprocessor, and reach a verification goal in far fewer simulation cycles than random simulation.