OneSpin extensible ABV plus formal linting is the Best of 2020
By: John Cooley
Best of 2020
YOU CAN TWEAK IT: The core strength OneSpin ABV has is that it's tweakable as a tool overall. For example, one user talks about tweaking OneSpin such that his company has a custom app just so DV-Verify auto-generates assertions for their proprietary internal programming language. A different customer loves DV-Verify because he can access it at such a deep low-level, he can create their own in-house OneSpin extensions to create a whole set of custom formal tools just for his company's unique design style. Try doing this with JasperGold or Questa Formal or VC Formal! (Good luck!) Why can you tweak OneSpin SW? Because years ago OneSpin originally started out as a "formal parts" EDA tool vendor.
Although DV-Inspect's biggest "plus" is in its "Autochecks" functions, it also has a lint browser. This is actually the first step I run. This lint browser is closer in functionality to a normal linter. It does have some noise, but less than a normal linter. To help reduce the noise typical of normal lint checks, DV-Inspect lets you filter between categories of checks, e.g. truncation, shift, and integer. The structural checks are all available out-of-the-box. You don't need to write any assertions. Below are examples of what DV-Inspect will automatically find and flag "as is"..