1020: Arithmetic Overflow Verification using Formal LINT Tools

LINT tools have been supporting digital designers to structurally detect design issues early in the design cycle. One of the key problems they seek to address is “arithmetic overflow” detection. Due to inevitable false negatives within pure Structural LINTing flow, designers struggle to isolate the real issues. Manual assessment of certain types of violations can be tedious, error-prone, and very time-consuming. LINT combined with Formal Methods of Analysis offers exciting new opportunities. Formal LINT tools provide efficient Formal-enhanced solutions for many LINTing applications to ensure good design quality. One of the areas of concern is arithmetic overflow verification. Formal-aware LINTing helps designers identify real design issues much more efficiently. However, efficient formal-aware verification requires RTL designers to adopt a certain coding style for signed arithmetic operations. . We have been partnering with EDA vendors to improve reliability and robustness of arithmetic overflow verification in Formal LINT tools, aiming to achieve higher productivity and accuracy. While the tools keep improving in their coverage, this paper recommends the most promising RTL coding style if one wants to use Formal LINT tools to detect arithmetic overflow. The paper illustrates strength of Formal LINT technology over Structural LINTing, summarizes best practices and pitfalls in signed arithmetic RTL implementation, articulates the approach taken in tool evaluations, and briefly presents the tool evaluation results.