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

Fingerprint

Decomposition
Computer hardware description languages

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Hardware and Architecture
  • Software

Cite this

Vasudevan, S., Viswanath, V., Abraham, J. A., & Tu, J. (2006). Automatic decomposition for sequential equivalence checking of system level and RTL descriptions. In Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06 (pp. 71-80). [1695903] (Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06).

Automatic decomposition for sequential equivalence checking of system level and RTL descriptions. / Vasudevan, Shobha; Viswanath, Vinod; Abraham, Jacob A.; Tu, Jiajin.

Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06. 2006. p. 71-80 1695903 (Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06).

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

Vasudevan, S, Viswanath, V, Abraham, JA & Tu, J 2006, Automatic decomposition for sequential equivalence checking of system level and RTL descriptions. in Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06., 1695903, Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06, pp. 71-80, 4th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06, Napa, CA, United States, 7/27/06.
Vasudevan S, Viswanath V, Abraham JA, Tu J. Automatic decomposition for sequential equivalence checking of system level and RTL descriptions. In Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06. 2006. p. 71-80. 1695903. (Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06).
Vasudevan, Shobha ; Viswanath, Vinod ; Abraham, Jacob A. ; Tu, Jiajin. / Automatic decomposition for sequential equivalence checking of system level and RTL descriptions. Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06. 2006. pp. 71-80 (Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06).
@inproceedings{c905eab0faf94fee98ce87c1b95e4a38,
title = "Automatic decomposition for sequential equivalence checking of system level and RTL descriptions",
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.",
author = "Shobha Vasudevan and Vinod Viswanath and Abraham, {Jacob A.} and Jiajin Tu",
year = "2006",
month = "12",
day = "1",
language = "English (US)",
isbn = "1424404215",
series = "Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06",
pages = "71--80",
booktitle = "Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06",

}

TY - GEN

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

AU - Vasudevan, Shobha

AU - Viswanath, Vinod

AU - Abraham, Jacob A.

AU - Tu, Jiajin

PY - 2006/12/1

Y1 - 2006/12/1

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

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

UR - http://www.scopus.com/inward/record.url?scp=34548835962&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=34548835962&partnerID=8YFLogxK

M3 - Conference contribution

SN - 1424404215

SN - 9781424404216

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

SP - 71

EP - 80

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

ER -