Sequential Equivalence Checking

Anmol Mathur Calypto Design Systems

Masahiro Fujita University of Tokyo

Andrea Fideli ST Microelectronics, Italy

Abstract. 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.

Topics Covered. In this tutorial, we will cover the following key areas:

1. Need for sequential equivalence checking in designs flows (1 hour)

a. Design flows using system-level models in SystemC/C++

b. Common verification flows using system-level models

c. Value proposition of SEC compared to alternate flows

2. Notions of sequential equivalence (30 min)

3. Characterization of differences between (30 min)

a. System-level models and RTL

b. RTL revisions requiring sequential equivalence checking

c. System-level revisions

4. Key sequential equivalence checking technologies (1.5 hours)

a. System-level modeling languages and model extraction

b. Specification of interfaces differences

c. Sequential analysis techniques and inductive proofs

d. Hybrid solvers : combining Boolean and word-level solvers

e. Debugging flows

The tutorial will also demonstrate the technology using a commercial sequential equivalence checker and some research prototypes. We intend to use demo examples in the tutorial wherever possible.

Intended Audience. 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

· Researchers looking for new avenues of research relevant to a real industrial tool