Applying formal verification techniques to verify a Fetch Unit

Abstract

The fetch unit of a GPP is a difficult block to verify. The complexity of the problem stems from the size of the state (cache, pipeline, etc.). Formal verification techniques, traditionally, have difficulty handling problems with large amounts of memory. We will explore different approaches to deal with these limitations such that we are able to reduce the wall time needed by the Formal Verification tools. This project covers the design and implementation of a Testbench for Formal Verification. In addition, it introduces different techniques and configurations to reduce the complexity of the Design Under Test and how they are applied into our Formal Verification Testbench. Finally, the performance impact of each technique is analyzed at the end of the document.