1.4 EDA的主要领域

1.4.5 数字系统形式验证

　在层次化设计过程中, 一般采用"自顶向下"的设计方法。在较高层次的设计完成之后, 都要经过检验, 证明正确以后才进入较低层次的设计。1.4.2节中介绍的模拟技术就是最为流行的方法之一。但是, 模拟技术存在右边所示缺点：
　数字系统形式验证则不进行动作模拟; 而是用形式验证的方法验证数字系统的正确性:
　（1）对数字系统作结构描述, 这是验证的对象。
　（2）对数字系统作功能描述, 作为验证的目标。
　验证的过程就是根据描述和一套公理系统证明该结构描述所实现的功能是否与相应的功能描述等价。