There has been much interest recently in combining the strengths of formal verification techniques and simulation for functional validation of large designs [6].Typically, a formal test model is first obtained from the design. Then, test sequences which satisfy certain coverage criteria are generated from the test model, which are simulated on the design for functional validation. In this paper, we focus on automatic abstractions for obtaining the test model from the design for simulation vector generation under the transition tour coverage model. Since most efforts using guided simulation have concentrated only on state/transition coverage, without relating these to error coverage of the original design, there is hardly any notion of preserving correctness, which has made it hard to use abstraction effectively.