Tutorial T7 Sequential Equivalence Checking
Anmol Mathur, S. Balakrishnan, Raj S. Mitra · 2006
Traditional equivalence checkers used for RTL-to-gate-level equivalence rely on the exact matching of state points to reduce the problem of proving equivalence between the two models to that of proving equivalence between the next state functions of the corresponding state points and the functions at corresponding outputs. They are hence classified as combinational equivalence checkers. The need for proving equivalence between models that do not have exact one-to-one mapping between state points (flops/latches) has grown tremendously in the last few years. There are two main application domains that are driving the need for more powerful equivalence checking paradigms that relax the restriction on the exact matching of state points between the specification and the implementation: • System-level to RTL equivalence checking • RTL to RTL equivalence checking with sequential micro-architectural changes We define sequential equivalence checking (SEC) to be the process of checking functional equivalence between models that do not satisfy the assumption of one-to-one flop mapping. The need for SEC is being driven by the widespread use of system-level modeling in SystemC/C/C++ for developing golden functional reference models, models for micro-architectural refinement and platforms for software development. This tutorial will identify the design flows where SEC can be effectively used, identify the key technologies needed for developing an effective SEC tool and demonstrate its value proposition in design flows. The tutorial should appeal to the following groups of people: • Designers/CAD engineers using system-level modeling based design flows or making sequential RTL changes • CAD tool developers looking for insight into the key technology needed for sequential equivalence checking