1. An apparatus for verifying correctness of a behavioral model of a microcode machine, the microcode machine operable in a native state and an emulated state, the apparatus, comprising: means for producing the native state; means for producing the emulated state; and means for comparing the native state and the emulated state.