Dedicated rewriting: Automatic verification of low power transformations in Register Transfer Level

Vinod Viswanath, Shobha Vasudevan, Jacob A. Abraham

Research output: Contribution to journalArticle

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. We further demonstrate the application of our technique on a completely different kind of hardware circuit, viz. microprocessors. We show the correctness of instruction-driven slicing algorithm as applied to the OR1200 microprocessor.

Original languageEnglish (US)
Pages (from-to)339-353
Number of pages15
JournalJournal of Low Power Electronics
Volume5
Issue number3
DOIs
StatePublished - Oct 1 2009

Keywords

  • Formal verification
  • Hardware verification
  • Low power
  • Term rewriting

ASJC Scopus subject areas

  • Electrical and Electronic Engineering

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

  • Cite this