Sequential equivalence checking between system level descriptions of designs and their Register Transfer Level (RTL) implementations
is a very challenging and important problem in the context of Systems on a Chip (SoCs). We propose a technique to alleviate
the complexity of the equivalence checking problem, by efficiently decomposing it using compare points. Traditionally, equivalence
checking techniques use nominal or functional mapping of latches as compare points. Since we operate at a level where design
descriptions are in System Level Languages or Hardware Description Languages, we leverage the information available to us
at this level in deducing
sequential compare points. Sequential compare points encapsulate the sequential behavior of designs and are obtained by statically analyzing the design
descriptions. We decompose the design using sequential compare points and represent the design behavior at these compare points
by symbolic expressions. We use a SAT solver to check the equivalence of the symbolic expressions. In order to demonstrate
our technique, we present results on a non-trivial case study. We show an equivalence check between a System C description
and two different Verilog RTL implementations of a Viterbi decoder, that is a component of the DRM SoC.
Keywords Sequential equivalence checking - C vs RTL - SAT solvers - Static analysis of hardware