Résumé
Generic algorithms for sequential equivalence checking are computationally expensive because they are based on state space traversal. This is the main reason why commercial tools often use combinational equivalence checking techniques to verify sequential designs. This approach consists in identifying potential equivalent flip- flops or nets in the two designs under verification. This is called the matching step. Due to sequential optimizations performed during synthesis, which can remove, merge, replicate or retime flip-flops, this matching step can be very complex and incomplete. Moreover if the matching is incomplete, even if a fast and efficient SAT solver is used during the combinational equivalence-checking step, this kind of approach may fail. In this paper, we present a complete matching engine, which is able to handle optimized circuit and don’t care conditions. The efficiency of the proposed engine is confirmed by experimental results on retimed and optimized circuits.