This paper presents software (model) transformations that can be used to effectively generate high fault coverage test sets. Unlike synthesis or design for testability methods which involve hardware modifications, this approach does not modify the hardware design. Instead, it transforms a software model of the design into a new software model that has desirable testability properties. A sequential test generator generates tests for the new model. The new model may not be functionally equivalent to the original design but our transformations guarantee that the tests generated for the new model can always be inverse mapped to serve as tests for the original design. Experimental results show that significantly high fault coverage can be achieved by using this approach.