Efficient Formal Verification with Smart Modelling
With the increase in design complexity and diversity, finding bugs quickly to guarantee high-quality functional verification is a formidable challenge as demands for safety and security increase for high-performance, low-power designs. The situation is further exacerbated when bugs are missed by dynamic simulation or are caught in emulation late in the cycle.
At the root cause of all verification complexity is concurrency and control – both of which are massively pervasive and deeply embedded. Formal verification provides efficient capabilities both for bug hunting as well as proving bug absence for concurrent and serial designs. However, getting formal verification tools to produce convergence on proof runs can be a significant challenge for end-to-end verification. Without proof convergence, formal verification cannot produce conclusive outcomes that bugs exist in designs, or they don’t.
In this webinar, we will provide insights on how we can build efficient and reusable formal verification models that can be used for verifying a class of designs with predictability producing verification outcomes that scale with design size. We will cover fundamentals and show how they apply to bigger designs using the Synopsys VC Formal tool.