Efficient Generation of Stimuli for Functional Verification by Backjumping Across Extended FSMs