Dedicated rewriting

Automatic verification of low power transformations in RTL

Vinod Viswanath, Shobha Vasudevan, Jacob A. Abraham

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

Abstract

We present dedicated rewriting, a novel technique to automatically prove the correctness of low power transformations in hardware systems described at the Register Transfer Level (RTL). We guarantee the correctness of any low power transformation by providing a functional equivalence proof of the hardware design before and after the transformation. We characterize low power transformations as rules, within our system. Dedicated rewriting is a highly automated deductive verification technique specially honed for proving correctness of low power transformations. We provide a notion of equivalence and establish the equivalence proof within our dedicated rewriting system. We demonstrate our technique on a non-trivial case study. We show equivalence of a Verilog RTL implementation of a Viterbi decoder, a component of the DRM SoC, before and after the application of multiple low power transformations.

Original languageEnglish (US)
Title of host publicationProceedings
Subtitle of host publication22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems
Pages77-82
Number of pages6
DOIs
StatePublished - Mar 30 2009
Event22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems - New Delhi, India
Duration: Jan 5 2009Jan 9 2009

Publication series

NameProceedings: 22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems

Other

Other22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems
CountryIndia
CityNew Delhi
Period1/5/091/9/09

Fingerprint

Hardware
Computer hardware description languages
System-on-chip

ASJC Scopus subject areas

  • Hardware and Architecture
  • Control and Systems Engineering
  • Electrical and Electronic Engineering

Cite this

Viswanath, V., Vasudevan, S., & Abraham, J. A. (2009). Dedicated rewriting: Automatic verification of low power transformations in RTL. In Proceedings: 22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems (pp. 77-82). [4749656] (Proceedings: 22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems). https://doi.org/10.1109/VLSI.Design.2009.85

Dedicated rewriting : Automatic verification of low power transformations in RTL. / Viswanath, Vinod; Vasudevan, Shobha; Abraham, Jacob A.

Proceedings: 22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems. 2009. p. 77-82 4749656 (Proceedings: 22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems).

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

Viswanath, V, Vasudevan, S & Abraham, JA 2009, Dedicated rewriting: Automatic verification of low power transformations in RTL. in Proceedings: 22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems., 4749656, Proceedings: 22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems, pp. 77-82, 22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems, New Delhi, India, 1/5/09. https://doi.org/10.1109/VLSI.Design.2009.85
Viswanath V, Vasudevan S, Abraham JA. Dedicated rewriting: Automatic verification of low power transformations in RTL. In Proceedings: 22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems. 2009. p. 77-82. 4749656. (Proceedings: 22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems). https://doi.org/10.1109/VLSI.Design.2009.85
Viswanath, Vinod ; Vasudevan, Shobha ; Abraham, Jacob A. / Dedicated rewriting : Automatic verification of low power transformations in RTL. Proceedings: 22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems. 2009. pp. 77-82 (Proceedings: 22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems).
@inproceedings{5e4e9d071e164b86b54490429e940823,
title = "Dedicated rewriting: Automatic verification of low power transformations in RTL",
abstract = "We present dedicated rewriting, a novel technique to automatically prove the correctness of low power transformations in hardware systems described at the Register Transfer Level (RTL). We guarantee the correctness of any low power transformation by providing a functional equivalence proof of the hardware design before and after the transformation. We characterize low power transformations as rules, within our system. Dedicated rewriting is a highly automated deductive verification technique specially honed for proving correctness of low power transformations. We provide a notion of equivalence and establish the equivalence proof within our dedicated rewriting system. We demonstrate our technique on a non-trivial case study. We show equivalence of a Verilog RTL implementation of a Viterbi decoder, a component of the DRM SoC, before and after the application of multiple low power transformations.",
author = "Vinod Viswanath and Shobha Vasudevan and Abraham, {Jacob A.}",
year = "2009",
month = "3",
day = "30",
doi = "10.1109/VLSI.Design.2009.85",
language = "English (US)",
isbn = "9780769535067",
series = "Proceedings: 22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems",
pages = "77--82",
booktitle = "Proceedings",

}

TY - GEN

T1 - Dedicated rewriting

T2 - Automatic verification of low power transformations in RTL

AU - Viswanath, Vinod

AU - Vasudevan, Shobha

AU - Abraham, Jacob A.

PY - 2009/3/30

Y1 - 2009/3/30

N2 - We present dedicated rewriting, a novel technique to automatically prove the correctness of low power transformations in hardware systems described at the Register Transfer Level (RTL). We guarantee the correctness of any low power transformation by providing a functional equivalence proof of the hardware design before and after the transformation. We characterize low power transformations as rules, within our system. Dedicated rewriting is a highly automated deductive verification technique specially honed for proving correctness of low power transformations. We provide a notion of equivalence and establish the equivalence proof within our dedicated rewriting system. We demonstrate our technique on a non-trivial case study. We show equivalence of a Verilog RTL implementation of a Viterbi decoder, a component of the DRM SoC, before and after the application of multiple low power transformations.

AB - We present dedicated rewriting, a novel technique to automatically prove the correctness of low power transformations in hardware systems described at the Register Transfer Level (RTL). We guarantee the correctness of any low power transformation by providing a functional equivalence proof of the hardware design before and after the transformation. We characterize low power transformations as rules, within our system. Dedicated rewriting is a highly automated deductive verification technique specially honed for proving correctness of low power transformations. We provide a notion of equivalence and establish the equivalence proof within our dedicated rewriting system. We demonstrate our technique on a non-trivial case study. We show equivalence of a Verilog RTL implementation of a Viterbi decoder, a component of the DRM SoC, before and after the application of multiple low power transformations.

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

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

U2 - 10.1109/VLSI.Design.2009.85

DO - 10.1109/VLSI.Design.2009.85

M3 - Conference contribution

SN - 9780769535067

T3 - Proceedings: 22nd International Conference on VLSI Design - Held Jointly with 7th International Conference on Embedded Systems

SP - 77

EP - 82

BT - Proceedings

ER -