本章介绍对所设计的逻辑电路进行正确性验证的另一种方法：形式验证。它不同于模拟验证，各有优缺点，互为补充。
形式验证分为等价性验证和性质验证两种，性质验证中最常用的方法是模型检验。
　　本章介绍布尔函数的一种新的表示法：二叉判决图BDD。由于最简有序BDD的正则性质，使其成为组合电路等价性验证的有效的方法。在符号模型检验中，也利用BDD隐式表示有限状态机的状态转换函数和输出函数。
　　模型检验是一种有效的时序电路性质验证方法。电路功能的模型用BDD表示的有限状态机表示。性质描述用基于时态逻辑的计算树逻辑CTL描述。CTL是严密的数学表示方法。通过对有限状态机检验状态可达性，判断是否满足CTL描述，从而判断电路性质的正确性。
　　在本章介绍的模型判别方法中，从VHDL描述提取有限状态机模型是一个关键。通过对每个进程中的语句建立子模型，然后进行合并，可得到整个进程的有限状态机模型。对于同步时序电路，还要把与时钟无关的组合电路部分进行合并，以减少不合理的状态。