集成电路产业已经成为国民经济的朝阳产业,每年在全球产生数千亿美元的生产价值。从世界上第一个块集成电路芯片诞生至今,集成电路芯片的面积越来越小,单位面积集成的电路元器件数越来越多,如今一块芯片上已集成了数亿个门。随成电路集成度的增高,人们发现制约集成电路发展的一个重要因素是芯片设计与芯片制造的严重脱节。阻碍芯片设计发展的一个重要因素便是如何验证芯片设计的正确性。传统的模拟验证已经难以满足芯片设计的要求。而形式化验证方法因其是基于严格的数学方法来确保芯片设计的正确性,因此已经在芯片设计领域受到越来越多的重视。实现形式化验证的理论并形成相关验证工具软件的一个关键点就是电路模型的抽取和仿真。本论文首先研究和学习了形式化验证的相关理论知识,包括该理论的主要分支,发展情况。并对目前形式化验证领域的主流算法GSTE进行了深入学习和研究,并对比了该算法与传统算法的不同。其次对当前学术界以及工业界的一些常用工具SMV,VIS,FORTE等进行研究和源码剖析。并对当前电路设计语言VERILOG进行学习研究后,在基于以上工具所提供的电路描述语言的基础上简化VERILOG。设计了一套针对GSTE算法的验证工具的电路描述语言的语法和语义。然后让软件能够方便的对电路进行描述并对电路模型进行抽取。最后设计了系统的框架以及技术路线。然后,研究了电路设计前端语言描述与数字电路形式化验证算法的结合点。分析了电路模型在计算机内存中表示的相关数据结构。研究了如何将一个用语言描述的电路抽取为适合采用GSTE算法来进行验证的电路模型,使得GSTE算法能够应用在实际的电路设计领域。使用编译工具LEX,YACC实现了本软件的电路输入前端,在对语法树进行语义推理后产生了电路模型的二叉判定图数据结构后,交由后端GSTE验证算法进行电路模型的形式化验证。本论文在对数字电路仿真进行了相关研究后,基于抽取的电路模型,实现对该电路模型的仿真,能够得到相应的波形图,从来能方便的对GSTE算法进行演示。最后对全文进行了系统全面的概括总结,并指出了本文所设计工具的不足以及下一步的改进方向,并展望了形式化验证算法在电路设计领域的良好应用前景。