随着集成电路设计领域的发展,芯片集成度越来越高,功能越来越强大,验证的地位也越来越高。其中形式验证中的等价性检查贯穿于整个后端设计流程之中。有代码与综合后网表之间的验证等价性检查;综合后的网表与布局布线后设计之间的等价性检查。论文描述了数字电路后端验证的发展和流程。研究了等价性检查的方法,包括组合电路检查方法、时序电路检查方法。论文通过macphy_dl加速器模块完成了等价性检查。检查首先准备了加速器模块RTL代码与网表的信息。加速器网表的面积,RTL代码标准库（startlib_lphvt₉t）中各个模块的面积、数量等参数。其次完成了模块验证流程。1.由准备过程产生流程与编译脚本,等价性检查在操作系统linux底下的目录。2.由抽取过程从加速器模块RTL代码中得到需要编译的代码,并且产生编译脚本。3.在编译过程中检查RTL代码与网表,并且得到要进行比较的gat文件。4.在比较过程中加上约束,给各个状态机赋输入与状态初值,查看下一状态与输出值。最后加速器模块有5000个输出不等价,有8000个下一状态不等价。由信号连接错误产生的不等价通过修改网表得到解决;由时钟门引起的不等价通过加约束删除网表中多余的时钟门得到解决;由无驱动引起的不等价通过加约束给无驱动信号赋值得到解决;由不匹配引起的不等价通过手动匹配管脚得到解决。最终结果5176个输出,10062个下一状态全等价。