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

ASJC Scopus subject areas

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

Fingerprint Dive into the research topics of 'Dedicated rewriting: Automatic verification of low power transformations in RTL'. Together they form a unique fingerprint.

  • 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