formality形式驗證裏的案件分析

在當前的形式驗證的領域，主要有兩個工具，一個就是Cadence的conformal，另外一個就是Synopsys的formality（以下簡稱FM）。 通常情況下，形式驗證的工具的主戰場，是在RTLvsSYN這個階段，主要是由於綜合器的mapping/optimization會遇到各種各樣的挑戰。但是，本案有一些不同，在通常很容易的SYNvsLAY裏邊，出現了一點小插曲。筆者整理了一下，以嗜各位讀

>>阅读原文<<