RTL2RTL Formal Equivalence: Boosting the Design Confidence

M. V.Achutha KiranKumar, Aarti Gupta, S. S. Bindumadhava

Research output: Contribution to journalConference articlepeer-review

Abstract

Increasing design complexity driven by feature and performance requirements and the Time to Market (TTM) constraints force a faster design and validation closure. This in turn enforces novel ways of identifying and debugging behavioral inconsistencies early in the design cycle. Addition of incremental features and timing fixes may alter the legacy design behavior and would inadvertently result in undesirable bugs. The most common method of verifying the correctness of the changed design is to run a dynamic regression test suite before and after the intended changes and compare the results, a method which is not exhaustive. Modern Formal Verification (FV) techniques involving new methods of proving Sequential Hardware Equivalence enabled a new set of solutions for the given problem, with complete coverage guarantee. Formal Equivalence can be applied for proving functional integrity after design changes resulting from a wide variety of reasons, ranging from simple pipeline optimizations to complex logic redistributions. We present here our experience of successfully applying the RTL to RTL (RTL2RTL) Formal Verification across a wide spectrum of problems on a Graphics design. The RTL2RTL FV enabled checking the design sanity in a very short time, thus enabling faster and safer design churn. The techniques presented in this paper are applicable to any complex hardware design.

Original languageEnglish (US)
Pages (from-to)29-44
Number of pages16
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume156
DOIs
StatePublished - Jul 8 2014
Externally publishedYes
Event2nd French Singaporean Workshop on Formal Methods and Applications, FSFMA 2014 - Singapore, Singapore
Duration: May 13 2014 → …

All Science Journal Classification (ASJC) codes

  • Software

Fingerprint

Dive into the research topics of 'RTL2RTL Formal Equivalence: Boosting the Design Confidence'. Together they form a unique fingerprint.

Cite this