Property Mining using Dynamic Dependency Graphs

Abstract

We present a technique to automatically generate SystemVerilog-Assertions from designs using dynamic dependency graphs. We extract relations between signals of the design using only a few simulation runs, which drastically reduces the required number of use cases compared to other approaches. Additionally, unlike previous approaches, we do not use expression templates to establish those relations. We abstract from the concrete use cases by inserting symbolic values and by merging similar conditions in time. A model-checker verifies the correctness of the generated properties. The evaluation shows that our approach is able to create more expressive properties than state of the art techniques, while requiring less simulation data.