Formal Verification Process Boosts Productivity

Claiming dramatic gains in formal verification productivity, OneSpin Solutions has announced a systematic verification process that 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. Termed GapFree Verification, the process, which is a no-cost addition to the company’s 360 Module Verifier (360 MV) formal tool, is said to systematically deliver predictable, repeatable verification results for complex modules and IP. 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; and 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, OneSpin claims. Moreover, the new process and enhanced 360 MV tools mitigate the capacity, scalability, and spurious counter-example limitations exhibited 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. Available now, GapFreeVerification is included in the latest version of 360 MV at no additional cost. OneSpin Solutions
www.onespin-solutions.com