Presentation

· Contributors · Organizations · Search Program · Flagged · Happening Now

Enhancing Formal Equivalence for Datapath Algorithms: A Proof Strategy with Intermediate Modeling to Address Structural Differences in Implementations

SessionStatic and Formal Verification: Pillars of Modern Design Assurance

DescriptionIn hardware designs, complex Datapath algorithms are initially realized using high-level languages like C/C++, or SystemC to establish the correctness of architecture intent. Same algorithm is then implemented using System Verilog, considering hardware aspects like power, performance, and area. The high-level abstracted model developed and verified initially is used as a golden specification to verify the RTL. It has been established that simulation alone is not sufficient for such complex algorithms. However, when performing Formal Equivalence Verification (FEV) between these two models, FEV tools often struggle to establish equivalency due to significant differences in data handling between the specification (spec)and implementation (impl). Currently, there is no automated or solver support from industry tools that can internally handle these abstraction differences and provide full confidence on the design. An incomplete proof in algorithm design can lead to missing deep corner case bugs. Considering we have many such algorithms which if left unconverged pose a threat to the accuracy of the blocks, we have developed a strategy on how to understand the abstraction difference and reduce it by creating/suggesting intermediate models to the tools. These models are proven in steps to assist the tools to get complete confidence. This presentation talks about one such use case which explains the rational behind identifying potential un-verifiable abstraction differences and then explains the techniques to create intermediate models and assist the tools for the same. Such methodology can vastly enhance the potential of the FV community to converge on designs which are otherwise deemed impossible to verify through traditional FEV.

Presenters

Event Type

Front-End Design