An efficient and cost effective mechanism for generating test files for automatic verification of a device model is disclosed. Uncompleted coverage goals determined based upon simulating processing of a test file by a design model may be expressed as negative assertions for input to a test data generator, where output from the test data generator may used to create a test file for completing all or some of the uncompleted coverage goals. The test data generator may indicate data which causes a property to fail, and therefore, may indicate test data which causes the uncompleted coverage goal to succeed. The initial test file may represent zero code coverage and/or zero functional coverage, thereby enabling the test data generator to automatically create one or more test files for accomplishing the more extensive code coverage goals and/or functional coverage goals. Functional coverage goals may be automatically generated by the test data generator.