1986年E.M.Clarke等提出模型检验（Model Checking）方法[9]。其做法是把要验证的时序电路抽象为有限状态机，用基于时态逻辑(Temporal logic)的CTL语言描述要验证的电路所应该满足的规则或性质(property)，然后采用状态枚举的方法，即遍历有限状态机的状态空间，对每个状态来判断是否满足这些规则或性质。例如，如果一个微处理器的控制部分描述为一个状态机，则对于"是否只有trap指令才能由用户模式转到管理模式"这样的性质描述，模型检验器可以作出回答。对于比较简单的控制器，由于状态数目不太多，这种方法通常是很有效的；但对于数据通路电路，由于状态数目十分巨大，无法显式枚举，因此就有些力不从心。
　　1990年J.R.Burch和E.M.Clarke对模型检验方法加以改进，提出了符号模型检验（Symbolic Model Checking）方法。其主要改进是用一个BDD来表示整个电路，将状态转换函数和输出函数合在一起，称为转换关系（transition relations）。对于带数据通路的时序电路，其状态是比较有规则的，采用BDD表示方法可以有效的利用这种特点，用比较小的空间表示状态图，而且将原来逐个状态遍历改为计算初始状态集合关于状态转换函数的不动点，因此能够验证状态空间很大的电路。此外，该方法对于CTL的描述能力也进行了扩展，使之能描述更复杂的性质。实验表明这种方法可以处理带数据通路逻辑的同步时序电路和异步时序电路，其处理的同步时序电路的状态数大约为5×10²⁰。
　　这是我们下面讲的方法的基础。
　　1991年J.R.Burch和E.M.Clarke指出，对于基于BDD的符号验证方法可以通过划分转换关系（partitioned transition relation）来降低复杂度。在这种方法中，状态转换图用多个BDD来表示，BDD之间是隐式"与"（implicity conjuncted）的关系。从待验证的电路结构可以自然地得到转换关系的划分。由于采用一组BDD来表示状态转换图，每个BDD所对应的功能相应比较简单，与之相关的变量数也比较少，因此，可以预期，每个BDD都比较小。实验表明，与原来的方法相比，BDD的节点数下降约两个数量级，验证所用的时间下降约一个数量级。所能处理的状态数已达到10¹²⁰。需要指出的是，这里的转换关系的划分，只是针对同步电路而言的。
　　1995年，E.M.Clarke将Symbolic Model Checking方法增加了调试功能。当用户提交状态转换图表示和性质描述后，模型检验算法要么判定状态图满足该性质描述，要么给出反例，指出是何种原因导致无法满足该性质。在复杂的设计中，这种反例将有助于设计人员查找细微的错误。但是在基于BDD的模型检验算法中，由于状态用符号表示，得到反例要比原来困难。
　　一般而言，一个硬件系统的动态行为，是最难设计和验证的。时态逻辑是一种表述系统所期望的性质的非常精确和方便的形式化手段。作为分支时态逻辑CTL也适合于描述异步时序系统。
　　本节后面有关于时态逻辑和CTL的介绍。CTL是命题时态逻辑的演变而来的，称为分支时态逻辑，也称为计算树逻辑，因为它描述关于具有不同路径的计算树的特性。
　　基于时态逻辑（特别是CTL）的模型检验的最大优点就是其判别过程高度自动化。用户在提交设计实现和性质描述之后，不需要关注验证的内部处理过程。其缺点主要有两个：
　　· 首先，电路的行为是根据一条条性质描述来进行验证的。如果要验证一个电路的所有行为，无法知道要列举多少条性质描述。CTL命题的语义也不够直观，难于理解。
　　· 其次，就是所谓的"状态空间爆炸"问题。尽管Symbolic Model Checking已经有了较大的进展，但其所能解决的状态空间规模对于包含数据通路的电路来说，仍显得太小。模型检验用于验证设计的控制部分，还是很有效的。至于数据通路的验证，以及数据通路和控制部分之间的交互关系的验证，则需要研究新的验证技术。
　　模型检验只是验证工具的一部分，它的作用还只是局部的，要完整地验证整个系统的所有功能，还需要继续研究。