The miniaturization of transistors in recent technology nodes requires tremendous back-end tuning and optimizations, making bug fixing at later design stages more expensive. Therefore, it is imperative to find design bugs as early as possible. The first defense against bugs is block-level testing performed by designers, and constrained-random simulation is the prevalent method. However, this method may miss corner-case scenarios. In this paper we propose an innovative methodology that reuses existing constrainedrandom testbenches for formal bug hunting. To support the methodology, we present several techniques to enhance RTL symbolic simulation, and integrate state-of-the-art word-level and Boolean-level verification techniques into a common framework called BugHunter. From case studies DLX, Alpha and FIR, BugHunter found more bugs than constrained-random simulation using fewer cycles, including four new bugs in the verified design previously unknown to the designer. The results ...