什么是形式验证

形式验证时要确定电路在哪一级电路上的测试是正确的，使用模型检验的方法看两个电路在描述上是否一致。

对组合逻辑来说，不存在状态寄存器，其输出值Z[t]不依赖于前面的输入值X[t-i](1≤i≤t)。这时只要对每个输入向量证明其输出向量相同。在组合逻辑验证领域有以下两类方法。

方法

形式验证的方法有等价性检查、模型检查、定理证明等。形式验证主要是用来在覆盖所有可能的输入情况下检查是否与给定的规范一致。SoC验证的形式化方法主要是等价性检查和模型检查。

模型检查主要是检查RTL代码是否满足规范中规定的一些特性。在规定这些特性时一般使用特性规范语言，一般也使用基于断言的验证语言。由于这种方法可以在不需要仿真的前提下检查设计中所有可能出现的情况是否满足规定的特性，所以使用这种方法不会遗漏任何的边界情况。