Functional Verification based on the EFSM Model