RTL2RTL Formal Equivalence: Boosting the Design Confidence

TL;DR

This paper demonstrates how RTL2RTL formal verification enhances confidence in complex hardware design by providing quick, exhaustive equivalence checking, thus enabling faster and safer design modifications.

Contribution

The paper presents practical application of RTL2RTL formal verification techniques to ensure design correctness efficiently across various complex hardware scenarios.

Findings

Enabled rapid and comprehensive equivalence checking

Reduced debugging time and increased design confidence

Applicable to a wide range of complex hardware designs

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.