Automatic decomposition for sequential equivalence checking of system level and RTL descriptions

Shobha Vasudevan, Vinod Viswanath, Jacob A. Abraham, Jiajin Tu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06
Pages71-80
Number of pages10
StatePublished - Dec 1 2006
Externally publishedYes
Event4th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06 - Napa, CA, United States
Duration: Jul 27 2006Jul 30 2006

Publication series

NameProceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06

Other

Other4th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06
CountryUnited States
CityNapa, CA
Period7/27/067/30/06

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Hardware and Architecture
  • Software

Fingerprint Dive into the research topics of 'Automatic decomposition for sequential equivalence checking of system level and RTL descriptions'. Together they form a unique fingerprint.

Cite this