随着计算机软硬件系统规模的日益复杂化、重要化，如何保证计算机系统的正确性和可靠性，逐渐成为当前理论界和产业界共同关心的重要问题。长期以来，常用的系统设计检验方法是以经验为基础的测试方法。但是，测试方法只能证明错误的存在，但不能证明错误的不存在，所以，对于高可靠性系统来说，测试方法有明显的局限性。 在过去二十多年间，各国研究人员为解决这个问题付出了巨大的努力，取得了重要的进展。在为此提出的诸多理论和方法中，模型检查(Model Checking)以其简洁明了和自动化程度高而引人注目。 本文首先介绍了模型检查技术的基本思想、研究方向和最新研究进展以及相关背景工具和VHDL语言，然后介绍了模型检查技术的理论基础，并研究和设计了一个针对时序电路VHDL设计的模型检查系统的解决方案。本文的主要工作有： 1.研究模型检查相关理论和算法，包括Kripke结构、时序逻辑CTL、不动点计算、反例路径生成等。并在此基础上实现了一个基于Kripke结构、不动点计算和OBDD动态排序的模型检查器，可验证VHDL设计的正确性。 2.提出了一个针对时序电路VHDL设计的模型检查系统的解决方案。包括了实现方案选择、系统主要内容(包括VHDL建模，给出规格说明，进行模型检查)以及系统总体框架； 3.实现将VHDL设计转换成有限状态机，并使之能同时适用于异步时序电路和同步时序电路，这包括建模算法、子模型的建立，子模型的合并等；另外对上述建模算法进行优化，对于同步时序电路能有效化简，减少系统状态空间。 4.研究和实现OBDD相关技术，将VHDL数据类型用OBDD表示，并采用动态变量排序的筛选算法，使OBDD变量序得到优化，减少OBDD的规模。 5.最后对一个锁存器VHDL设计进行模型检查以检验所做工作。