Automatic generation of coverage directives targeting signal relationships by statically analyzing RTL

Access full-text files




Gupta, Kshitiz

Journal Title

Journal ISSN

Volume Title



The coverage problem has been a long standing issue in simulation- based veri cation. Coverage metrics are required to track the progress and justify completeness of simulation vectors. This thesis presents a scalable methodology to automatically generate coverage directives which augment line coverage for complete coverage of the RTL. The directives target ambiguity in register relationships derived by statically analyzing behavioral RTL. A Python-based tool has been built on the presented methodology to gener- ates implication properties for coverage. The generated properties for two cores (Amber and V-scale) are instantiated within the testbenches provided with them. Simulation results with all the test programs highlight module instances with high line coverage but uncovered properties. These properties are formally proven to be reachable, thus highlighting coverage holes with the provided tests and the usefulness of our process.


LCSH Subject Headings