System, methods, and apparatus for verifying microcircuit designs by interleaving between random and formal simulation techniques to identify input traces useful for driving designs under test into sequences of device states. In a method aspect the invention provides process for beginning random simulation of a sequence of states of a microcircuit design by inputting a sequence of random input vectors to a design under test model in order to obtain a sequence of random simulation states; monitoring a simulation coverage progress metric to determine a preference for switching from random simulation to formal methods of simulating states in the design under test; beginning formal simulation of states in the design under test and monitoring a formal coverage progress metric to determine a preference for resuming random simulation of states of said microcircuit design; and resuming random simulation. Preferably the process of interleaving simulation methods continues until an input vector suitable for driving the design under test model into each of a set of previously-identified goal states has been obtained.