Sequential equivalence checking

Summary form only for tutorial. 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 identifies 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.