Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties

Boosting Verification Scalability via Structural Grouping
and Semantic Partitioning of Properties

Rohit Dureja, Jason Baumgartner, Alexander Ivrii, Robert Kanzelman, and Kristin Yvonne Rozier

This webpage contains supplementary experimental data for "Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties" by R. Dureja, J. Baumgartner, A. Ivrii, R. Kanzelman, and K. Y. Rozier.

Results

Most of the experimental results have been described in the paper. This webpage contains some additional results on support vector computation, leveling order, localization with grouping.

Support Vector Computation (Multiple COI)

The figures below show information for all 174 benchmarks from the HWMCC 2013 multi-property verification track. These benchmarks are not reduced in any way.

Figure 1: SCC computation time using Tarjan's

Forest — Figure 2: Vector length ratio with and without SCC compression

Figure 3: Maximum number of active bitvectors in memory

Figure 4: Multi-COI computation time relative to one-by-one (iterative) computation

Figure 1 shows time taken to compute SCCs for all benchmarks using the linear-time Tarjan's algorithm. The support bitvectors can be packed by representing every SCC as a single weighted support variable; SCC bits have weight equal to the the number of registers in the SCC, while others have unit-weight. Figure 2 shows the ratio of vector lengths with and without packing. The peak memory usage can be reduced by freeing up bitvectors for intermediate gates. The bitvector for a non-property gate is freed after traversing its fanout. Figure 3 shows the ratio of the maximum number of active bitvectors in memory with and without garbage collection. Lastly, Figure 4 shows the overall bitvector-support computation time using our employed approach [9] versus iterative netlist sweeps for each property.

Verification Impact of Grouping

Table 1 (PDF) shows our full experimental results of 48 selected benchmarks from HWMCC. These are obtained by simplifying all the benchmarks by standard logic synthesis (similar to &dc2 in ABC) to solve easy properties, and disjunctive decomposition to fragment each OR-gate property into a sub-property of its literals. Each property, or property group, is solved using a portfolio comprising BMC, IC3, and localization (LOC) without semantic partitioning. Each can process multiple properties: IC3 and BMC in a time- sharing manner, and LOC concurrently abstracting a set of properties which are solved using IC3. The experiment setup used is detailed in the paper. Verification time for 'Level-n' signifies grouping is performed at all levels up to and including n. The data in the table below is used to generate Figure 9, Figure 10, and Table I in the paper.

Grouping Impact on Localization

We select 24 benchmarks having at least 50 properties solved by LOC. Properties not solved by localization are not considered. Table 2 (PDF) shows our complete results on running localization on grouped properties. 'Random' grouping is done by sorting properties by COI size, and partitioning into equally-sized N groups. The data in the table below is used to generate Figure 11 in the paper.