LEC/FORMAL --- PARTI 原理介绍

LEC：lec（logic equivalence checking）又叫formal check，是对ic design的综合，PR前后的设计进行逻辑对比检查的工具/手段，保证综合不改变rtl原始的logic function。目前用的较多的就是C家的formal工具。接下来介绍一下lec的原理和流程

1. Lec 原理介绍：

之所以搞这个lec，是因为在rtl实现的过程中，会进行各种的优化逻辑操作，有时候为了优化面积或者timing，把一些工具认为不必要的逻辑进行了优化，那优化后的逻辑是否真正的仍然是rtl的需求呢?就需要做一个对比的验证。
在验证过程中，通过对比所有的key point pairs的方式，将整个design进行对比验证。对比过程中，把更靠近设计上游的design认为是golden的，把另一个design认为是revised的。

1.1 key points

当我们的design的instance变成20万，100万时候，不可能把所有的小的逻辑单元拿出来一个个的对比，这样可能会跑上个很久很久很久。为了加速这种对比，通过设定key points的方式。如下图所示，无论是golden还是revised design，都可以设置为key points加上logic cones的方式进行。我们只需要对两者design中对应的key points点进行比较，因为logic cones只是组合逻辑内容，不会影响到结果。这样会大大的加快对比的速度，也能保证准确性。

Key point上都有那些：
Primary inputs (PI) /Primary outputs (PO) /D flip-flop /D latches
Blackboxes (BBOX)/TIE-Z gates /TIE-E gates/CUT gates

1.2 Mapping

在做compare之前，需要进行一个mapping 操作，何为map？其实就是把golden和revised design的key points点一一对应上，首先要保证我们的输入键是正确的，我们比较的两个点的位置是正确的，才能保证结果是正确的。那工具是如何把两个design的key points互相对上的呢？其实在进行map的时候，会有name based map和func-based map，这个要根据项目情况和综合情况，自行组合选择。

1.3 Compare

当上一步骤的map完成之后，接下来就是要进行compare步骤了。
那么compare对于时序逻辑如DFF是怎么处理的呢？如下图所示，并不把这个DFF当成是一个正常的功能逻辑，而是分开，D端口作为比较的点，而Q端口作为下个比较点的输入。

那都有哪些点进行比较呢？其实主要还是从key points中的内容。比较的点包含了逻辑堆的汇聚点，Primary outputs, cut gates, DFFs, D-latches, and blackboxes。
虽然此刻比较的是一些key points点，但是实际还是对逻辑堆的比较，因为工具所比较的内容是从key points点经过逻辑堆，再到key points点才进行的check，正确与否和中间经过的逻辑关系密切。