Anmol Mathur *Calypto Design Systems*

Masahiro Fujita* University of Tokyo*

Andrea Fideli* ST Microelectronics,
Italy*

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.

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.

·
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