Formally verified redundancy removal
Stefan Hendricx, Luc Claesen · 1999
In general, logic redundancy tends to degrade design-quality by introducing additional delays in signal propaga-tion, by increasing the gate count or simply by making the resulting hardware untestable. Since they cannot always be avoided, unwanted redundancies have to be first identified and then removed from our designs. In this paper, an alter-native methodology to identify and remove redundancy is proposed, which is based on a formal, symbolic verification strategy. The formal framework underlying our approach aids in identifying redundancies and allows us to guarantee the correctness of their removal. 1.