Raising the level of Formal Signoff with End-to-End Checking Methodology

The use of formal verification has been steadily increasing thanks to the widespread adoption of automatic formal, formal applications and assertion-based formal checking. However, to continue finding bugs earlier in the design process, we must advance formal verification beyond focusing on a handful of localized functionalities toward completely verifying all block-level design behaviors. An end-to-end formal test bench methodology allows the RTL designer and formal verification engineer to work parallelly to finish design and verification on all functionality formally signed-off as bug-free. Given that today’s formal tools cannot close the end-to-end checkers required to verify complex IP blocks, we must rely on methodology to tackle design complexity in a way that allows the formal tool to converge in project time. This paper aims to demystify the end-to-end formal test bench methodology and discusses how we can reduce the complexity of the design with functional decomposition and abstraction techniques.

Ping Yeung, Oski Technology
Arun Khurana, Oski Technology
Dhruv Gupta, Oski Technology
Ashutosh Prasad, Oski Technology
Achin Mittal, Oski Technology