数字电路的功能可靠是集成电路行业发展的重要基础,基于模型的验证方法被广泛应用于数字电路功能验证中。但是,目前大多数建模方法复杂度较高,所建模型难以准确表示数字电路的功能行为和时序行为,进而难以确保基于模型进行的功能验证是有效和充分的。扩展有限状态机（Extended Finite State Machine,EFSM）作为一种形式化描述模型,能够准确表征系统的动态行为,常用于各类系统的建模与验证中。因此,本论文运用EFSM模型对数字电路进行建模,并在此基础上,进行基于模型的功能验证。依据寄存器传输级（Register Transfer Level,RTL）数字电路的特征,分析其过程块内的功能行为与EFSM模型的变量、状态和迁移等元素之间的对应关系,由此构建过程块的EFSM模型。并从数据驱动关系和时序关系两方面对过程块间关系进行分析,根据过程块间关系,构建RTL数字电路的EFSM模型。研究一种基于EFSM模型的RTL数字电路功能验证方法。具体而言,设计一种贡献度指导的EFSM模型测试序列生成方法,以提高测试序列的生成效率;对于生成的测试序列,采用遗传算法生成其激励向量,并设计适应度函数指导激励向量生成,以提高功能验证的覆盖率。为验证RTL数字电路的EFSM模型构建的有效性,以及基于EFSM模型的RTL数字电路功能验证的有效性和效率,本论文以五个数字电路为实验对象,对其进行EFSM模型构建及基于EFSM模型的功能验证。实验结果表明,本文所提方法在合理时间内能够构建RTL数字电路的EFSM模型,且该模型能够完整地描述数字电路的行为;基于EFSM模型的RTL数字电路功能验证不仅能够有效提高功能验证覆盖率,而且能够缩短验证时间,提升验证效率。