6.4 符号模型检验
6.4.4 CTL符号模型检验
在CTL符号模型检验中，要验证的时序电路抽象为有限状态机模型，要验证的电路所应该满足的规则或性质则用CTL语言描述。首先，需要进行可达性分析，计算该有限状态机模型的合法状态空间。也就是从初始状态集合S0出发所能到达的所有状态的集合S，称之为可达状态集合；然后，再计算满足待验证的CTL性质的状态的集合T；最后进行比较，判断是否有T
S。如果存在s∈S，而同时s
T，则说明该有限状态系统有些合法状态不满足待验证的性质。性质验证是验证状态之间的包含关系，而不是等价关系。验证有限状态机中是否包含所要验证的性质。
1. 可达性分析