Generating Good Properties from a Small Number of Use Cases

The final design of today’s ICs is in many cases created by combining functional blocks from various vendors or reusing them from previous projects. Often only partial information about the internal behavior of such blocks is available. One way to describe the behavior of a functional block are formal properties. The advantage of properties in comparison to informal specifications is that they are precise and can be handled by tools. We present a technique to automatically generate SystemVerilog-Assertions from designs using dynamic dependency graphs. The dynamic dependency graphs are created from a set of predefined or automatically generated use cases. Using the dynamic dependency graph we compute the conditions under which specific outputs are observable. By this, 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. We abstract from the concrete values in the use cases using symbolic values and merging the temporal behavior of similar conditions. In the end, a modelchecker verifies the correctness of the generated propertie