【学习目标】　
　　掌握关于形式验证的的概念，掌握BDD的概念和布尔函数的表示，理解基于二叉判决图(BDD)的验证模型和验证算法，了解模型检验的模型生成和验证方法。本章所涉及的基本知识较多，难度较大，不作为基本要求，读者可根据自己的需要选择是否学习这一章。

　　【学习方法】　
　　在学习新知识的同时着重于理解各种形式验证的概念和基本方法，着重理解模型的建立和验证方法。本章的目的不在于介绍一种方法，而主要是掌握基本概念。通过本章的学习，能在较快接受别的和新出现的验证方法。

　　【学习指南】
　　BDD是一种对形式验证特别有效的布尔函数的一种图形表示方法，本章介绍的组合电路的验证方法就是判断两个电路所生成的化简后的有序BDD是否一致，而对符号模型检验，也是用BDD表示有限状态机。首先理解BDD,才能对后面的方法较容易理解。本章的重点内容为时序电路的模型检验。要理解模型的建立和验证方法的思想。要根据所提到的VHDL内容复习第2章。

　　【难重点】
　　1. 形式验证的基本概念
　　2. 二叉判决图BDD的表示及其性质
　　3. 用BDD验证组合电路等价性的方法
　　4. 同步时序电路的模型
　　5. 模型检验方法
　　6. 用VHDL建立有限自动机模型的方法

　　【预习思考题】
　　1. 形式验证的概念是什么？形式验证与模拟验证有什么不同？各有什么优缺点？
　　2. 什么是等价性验证？什么是性质验证？有什么区别？
　　3. BDD的概念是什么？如何表示布尔函数？有什么重要性质？
　　4. 组合电路的等价性验证依据什么？
　　5. 模型检验的基本过程是什么？需要什么样的描述数据？
　　6. 什么是同步时序电路模型？与一般时序电路模型有什么区别？
　　7. 如何生成有限自动机模型？如何体现时序的同步？
　　8. CTL是个什么样的逻辑？如何表示电路性质？各个时间运算符的意义是什么？
　　9. 如何根据有限自动机模型和CTL模型进行模型检验？

　　【本节知识点】
　　· 形式验证的目的和基本方法
　　· 用BDD表示布尔函数
　　· 组合电路等价性验证
　　· 时序电路模型检验
　　· VHDL描述的有限状态机模型
　　· 描述性指用的计算树逻辑CTL
　　· 模型检验算法