cross-posted from: https://discuss.tchncs.de/post/2357238
Are you an engineer working on designing complex modern chips or System On Chips (SOCs) at the Register Transfer Level (RTL)? Have you ever been in one of the following frustrating situations?
•Your RTL designs suffered a major (and expensive) bug escape due to insufficient coverage of corner cases during simulation testing.
• You created a new RTL module and want to see its real flows in simulation, but realize this will take another few weeks of testbench development work.
• You tweaked a piece of RTL to aid synthesis or timing and need to spend weeks simulating to make sure you did not actually change its functionality.
• You are in the late stages of validating a design, and the continuing stream of new bugs makes it clear that your randomized simulations are just not providing proper coverage.
• You modified the control register specification for your design and need to spend lots of time simulating to make sure your changes to the RTL correctly implement these registers.
If so, congratulations: you have picked up the right book! Each of these situations can be addressed using formal verification (FV) to significantly increase both your overall productivity and your confidence in your results. You will achieve this by using formal mathematical tools to create orders-of-magnitude increases in efficiency and productivity, as well as introducing mathematical near-certainty into areas previously dependent on informal testing.
Design verification has always been essential to chip design. However as chip complexity increased over years, state-space and required verification effort exponentially exploded. With emerging powerful and commercially accessible tools, formal verification has become more viable and even unavoidable for reliable sign-off and catching bugs early in the process. I found this book a very helpful introduction to formal verification. It explains how formal can be utilized, different methods like formal property verification (FPV) and sequential equivalence checks (SEC) and where they are useful, limitations, complexity problems and how to mitigate the issues that come with formal. It explains how formal and functional can complement each other for combined sigh-off. It explains theoretical concepts with clear examples and diagrams. It explains formal algorithms as well for anyone interested, but focus is more about how to utilize formal in your projects. And if you are a total beginner, do not worry, there is section which explains essentials of Systemverilog Assertions (SVA), which you can completely skip if you know about it already.
