6.4 符号模型检验 6.4.1 模型检验的概念 　定理证明的一个显著特点是验证过程中使用的主要是结构信息而非行为信息。模型检验的方法则刚好相反，只判别系统的行为是否满足某种性质或特性。 　我们在设计电路时，希望有哪些功能，这些功能有哪些性质？例如，交通灯控制，希望在什么时候变什么颜色的灯，这是功能；二个交叉方向不能同时有绿灯出现，这就是性质。当然在验证时，也可以把一些功能当成性质来验证。 　模型检验是采用状态机分析（state machine analysis）或者称为状态空间搜索（state exploration）的技术来判别用某种时态逻辑所描述的命题正确与否。在BDD提出之后不久，表示状态机采用了BDD表示方法，使得验证方法得到较大的发展。 　状态机即为表示电路功能的有限状态机。在状态机中搜索一条或几条路径所描述的性质。