Summary form only given. Constrained random simulation is a widespread technique used to perform functional verification of 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. On the other hand, formal verification solutions can deliver very high confidence in the correctness of a design, but they are very limited in the complexity of the designs that they can tackle. In this talk we present Guido, a novel hybrid solution to boost the coverage achieved during functional verification by closely integrating simulation-based and formal techniques. Guido exploits formal verification to effectively guide a logic simulation towards a verification or coverage goal of interest. Guido provides significant value to a verification engineer because 1) it guides the simulation by means of a distance function derived from the circuit structure, and 2) it has a trace sequence controller which monitors and controls the direction of the simulation by striking a balance between random chance and controlled hill-climbing. Finally, we present experimental results indicating that Guido can tackle the verification of complex designs, including a picoJava microprocessor, and reach a verification goal in far fewer simulation cycles than constrained random simulation