逻辑综合是一种通过EDA工具将设计的RTL模型自动转换为门网表的过程，总的来说，这个过程在研发流程中已经非常非常成熟了。
逻辑综合这个过程，类似于人为地修改RTL一样，也是可能会出现错误的。这些错误可能是综合工具的BUG、错误的用户指令或者错误的Verilog语法使用等等。
另外，在后端物理实现的很多步骤中都会涉及对门级网表的修改，这同样也会引入错误导致功能和原始的RTL不同。
因此，在芯片研发的流程中，只要你使用逻辑综合将RTL转换为门级网表，那么你必然需要使用FEC工具进行RTL和门级网表等价性比对。
下图是一个FEC RTLvs Netlist等价性比对的示例。看起来不同，实际功能是一致的，在后端不同的约束下具有不同的实现。
FEC等价性检查的第一步是建立映射关系，这个建立的过程可由工具实现，也可以认为指定。映射的点可以是输入、输出、寄存器以及其他人为指定的比较点等等。
映射完成后，FEV工具需要计算相应的逻辑值，执行实际的比对。
这些计算和比对的公式我们都已经在数字电路课程中学到过，例如下图用到的摩根定律。
在实际进行 RTL vs Netlist比对时，我们会遇到很多复杂的场景。这个时候就需要case by case分析，然后例如约束或者工具指令解决问题。这些问题解决的方式最好需要经过组内有经验的工程师一起检视。
作者：验证哥布林
原文链接：使用FEC进行RTLvs Netlist比对
微信公众号：
推荐阅读
更多IC设计技术干货请关注</span>IC设计技术专栏。
