OneSpin GapFreeVerification for Formal Verification

GapFreeVerification, from OneSpin Solutions, is a patent-pending, systematic verification process for its 360 Module Verifier (360 MV) solution that dramatically boosts verification productivity. The new process systematically delivers predictable, repeatable verification results for complex modules and IP, accelerating the gap-free formal verification that ensures first-time error-free operation. It defines a structured and integrated sequence of user activities and tool tasks; this sequence predictably transforms the design-under-verification (DUV) and its informal specification into a gap-free formal specification and a provably equivalent DUV. GapFreeVerification is included in the latest version of 360 MV at no additional cost.

The GapFreeVerification process virtually eliminates the extensive effort required by simulation-based and other formal verification approaches for:

  • Verification planning and review
  • Construction of complex coverage models
  • Collection and analysis of massive coverage information to improve verification quality

The new process guides users in the systematic construction of a high-level, functional reference model consisting of a gap-free property set. The high-level reference model is a formal specification of the entire expected functionality of the DUV – analogous to golden reference models that specify expected DUV behavior in advanced testbenches. Using 360 MV’s property and completeness checking capabilities, the reference model is compared to the DUV with the same rigor as RTL and netlist models are compared using formal equivalence checking. This ensures gap-free verification and error-free DUV operation. In addition, the new process and enhanced 360 MV tools mitigate the capacity, scalability and spurious counter-example limitations common in other formal verification tools, which are targeted primarily at “bug hunting.” By mitigating these limitations, GapFreeVerification extends systematic formal verification to a broad range of complex modules and IP where other formal approaches fail to scale.

More info: OneSpin Solutions