RTL2RTL Formal Equivalence: Boosting the Design Confidence

M V Achutha Kiran Kumar
(Intel Technologies Ind Pvt Ltd)
Aarti Gupta
(Intel Technologies Ind Pvt Ltd)
S S Bindumadhava
(Intel Technologies Ind Pvt Ltd)

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.

In Shang-Wei Lin and Laure Petrucci: Proceedings 2nd French Singaporean Workshop on Formal Methods and Applications (FSFMA 2014), Singapore, 13th May 2014, Electronic Proceedings in Theoretical Computer Science 156, pp. 29–44.
Published: 8th July 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.156.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org