设计大规模的复杂的数字系统中关键问题之一是如何检查设计的正确性。但是,传统的验证技术例如模拟、仿真和测试,只能针对某些典型的情况或随机进行,这就难以完全排除所有设计错误。传统的验证技术已经无法适应目前集成电路芯片技术高速发展的需求。本论文就是针对上述问题,研究一种新的验证技术-模型检验。模型检验的基本思想是用分支时态逻辑公式f表达系统(程序或电路)的所期望的性质,用有限状态机(Kripke结构)M={S, R, L}表示系统的状态转移结构,通过遍历有限状态机来检验时态逻辑公式的正确性f:{s∈S| M, s|=f}。如不能验证公式f的正确性,系统将给出一个反例,使用户发现公式不成立的原因。模型检验不能直接对硬件电路设计描述文件(如Verilog程序)进行验证,必须将硬件电路设计描述文件转换为有限状态机。本论文就是为了解决这个问题,研究模型检验器的前端系统,即如何从硬件描述语言Verilog提取有限状态机。主要的工作是开发了两个软件编译器:VL2BLIF编译器和BLIF2FSM编译器。VL2BLIF编译器的核心功能是把Verilog程序编译为BLIF-MV程序。BLIF2FSM编译器的核心功能是从BLIF-MV程序中提取出有限状态机,并使用二叉判定图表示有限状态机。主要工作内容为:1.编写lex与yacc源程序,使编译器能够自动地分析Verilog程序与BLIF-MV程序的词法、语法、语义。生成编译器可处理的中间数据结构,并自动检查Verilog程序与BLIF-MV程序的静态语义错误。2.详细研究Verilog程序中的各种语句如何描述数字电路的状态转换关系。并研究在BLIF-MV程序中如何使用时间机和非时间机来描述状态转换关系和更新状态变量。重点分析含有延迟与事件控制的过程赋值语句如何转变为时间机。3.研究如何使用布尔函数来描述BLIF-MV语言的状态转换关系和多值变量的关系。4.研究二叉判定图表示布尔函数的方法。并分析二叉判定图减小存储空间的方法。