形式验证可以做什么？

我们经常听到形式验证这个名词，也知道它是通过一种数学证明的方式来验证电路。

但是具体来说形式验证到底能做什么呢？

形式验证可以分为2种：

一是两种模型（RTL vs Gate, RTL vs RTL, Gate vs Gate）在功能上的等效性检查，典型工具有LEC；

二是模型验证保证电路的某些属性是符合预想的，比如使用assertion确定电路的一些属性，然后工具从电路种提取这些属性，看看是不是匹配。

逻辑等效性检查

逻辑等效性检查是基于logic cone，以寄存器作为基点。详细的可看其他的文档。这里讨论模型检查，以BLCAKTIE工具为主介绍。

模型检查

在Blackie中，分为PDC和UDC。PDC是指预先就定义的一些属性，是由工具产商提供，UDC是指用户自定义的，由用户自己编写。

其中PDC有以下的功能检查：

1 语义的一致性（RTL和GATE的一致性）
2 结构的一致性
3 分支使能检查
4 FSM检查
5 跨越时钟域的检查

语义的一致性
这是指RTL的代码与GATE的代码会出现不一致的检查。它可以包括：
1 full_case 检查
2 parrellel_case 检查
3 不定态赋值
4 越界

结构的一致性
这是指一些结构上的问题，比如总线上的数据冲突，双重驱动等。它包括：
1 总线
2 三态逻辑
3 多口的暂存器
4 复位和清零检查

分支使能检查
检查每个分支是否都会有效

FSM检查
检查状态机是否有问题存在，它包括：
1 各个状态是否能跳到
2 状态跳转
3 死锁

跨越时钟域的检查
检查是否存在时钟域上的时序问题，是否有metastability和数据的有效性问题。

UDC是用户定义的assertion的检查。