Synopsys is supporting free downloads of a primer on formal verification, written by three key industry players.
Finding Your Way Through Formal Verification is authored by Bernard Murphy, former CTO at Atrenta; Manish Pandey, a Fellow at Synopsys and adjunct professor at Carnegie Mellon University, who leads the R&D teams for formal and static technologies, and machine learning at Synopsys; and Sean Safarpour, director of application engineering at Synopsys, where his team supports the development and deployment of products such as VC Formal, Hector and assertion IPs.
The e-book offers an introduction to formal verification methods for those who may be curious about the technique, or have already decided to take it up as a part of a wider verification plan and need to understand its advantages and limitations in order to manage its use effectively. It should provide a foundation on how formal methods work, when and where to apply them and how formal verification is managed in the overall verification process.
Early chapters lay out the background for the emergence of formal verification, the basic formal techniques, and some of the early limitations. The book then goes on to explain how to get started with formal techniques, how to apply it more widely in current designs, adding formal techniques to your current flow, and a look forward to use in specific application domains such as security, safety, data-path and clock-domain crossing analysis. In its last chapters it considers the future of formal verification, including the possible impact of techniques such as machine learning.
There is also a useful further reading list, and a glossary of formal terms.