Analysing and closing simulation coverage by automatic generation and verification of formal properties from coverage reports

A significant amount of time during simulation-based hardware design verification is spent analysing coverage reports in order to identify which uncovered cases are coverable and which are not, ie indicating areas of dead code. This dead-code analysis is typically left until the code is stable because changes to the code can mean having to start the analysis again. Some formal tools offer a push-button functionality allowing this process to be automated to some extent. This paper extends this capability of formal tools. A method is presented that automatically extracts candidates for dead code analysis from coverage reports, turns these into formal assertions and uses a formal property checker to determine whether or not the code can be reached. The core principle of the method is based on temporal induction. The method is fully automatic and generic in that it can be implemented with any state-of-the-art formal property checker; it also does not need code stability. The major benefits of employing this method in practice are a saving of engineering effort and earlier coverage closure which can avoid late discovery of bugs and schedule slips.