Assertion based formal verification using Jaspergold

Abstract

SoC verification today is becoming the bottleneck to the entire design flow in terms of cost and effort. In the present era of automation and IoT, smart connected devices handle vast personal information and communicate through a network of billion computing devices, effecting a rapid change in the design environment. Consequently, the time-to-market requirements for design and development have become more aggressive. This implies that SoC verification has to manage potentially more error prone designs with sharp time and resource constraints. Despite the rich literature and advancements in verification technologies, there still exists a significant gap between the present state-of-art technology and verification requirements for modern designs. With an enormous growth in the design complexity, it not possible to have a stand-alone verification technique as the solution. This thesis aims to present an assertion based formal verification strategy that guarantees strict adherence of the DUT to its specifications. A master’s coherent access to memory is exhaustively verified using JasperGold FPV from Cadence Design Systems tool suite and SVA language. The verification results show that using assertion based formal verification techniques guarantees a bug free DUT and expedites the verification sign-off.