Bugs happen when multiple events collide in uncommon scenarios. Our methodology leverages your functional simulation activities and starts formal verification from interesting “fishing spots” in the simulation traces. We will show where the most interesting “fishing spots” are, and explain how formal engine health is used to prioritize and guide the process.