1996 Research Summaries for the Ptolemy Project

Netlist Comparison for Incremental Verification

Researchers:Gitanjali M. Swamy and Stephen A. Edwards
Advisors:R. K. Brayton and Edward A. Lee
Sponsors:National Science Foundation Fellowship, ARPA and the US Air Force (under the RASSP program, contract F33615-93-C-1317) and the Ptolemy project.
This project is part of an effort to exploit the similarities between successive revisions of a digital system design to reduce the amount of effort required to analyze them. Swamy and Brayton [1] have shown that formal verification, in which a system is exhaustively simulated symbolically (an expensive but very desirable analysis), can be made much faster if information from an analysis of a similar system and the differences between the two systems are known. The objective of this project is to determine the largest section of the new system that can be taken from the old to minimize the amount of work that must be repeated.

Our scheme compares two systems described by netlists of interconnected combinational boolean functions. We assume that there is no correlation between names in the two netlists because, e.g., they were produced by a high-level language compiler. Our objective is to find a matching of primary inputs and a maximal mapping from nodes in the new netlist to those in the old such that the functions computed at these nodes are identical.

Our algorithm works by first identifying candidate node matchings, using this to identify candidate primary input matchings, and then finds the matching that reuses the largest portion of the old network. First, the nodes in each netlist are reduced to a semi-canonical form and hashed into equivalence classes based purely on this form. Next, these classes are refined based on the inputs to each node, producing structural equivalence classes. The set of all possible primary input matchings is generated by considering maximal matchings between such ``equivalent'' nodes with at least one primary input. Finally, the fraction of the new network that can be taken from the old network is evaluated for each matching using a fast, incremental algorithm.

We are currently in the process of implementing and evaluating this algorithm within Berkeley's VIS system for formal verification.

  1. Gitanjali M. Swamy and Robert K. Brayton, ``Incremental Formal Design Verification,'' Proceedings of the 1994 IEEE/ACM International Conference on Computer-Aided Design, San Jose, CA, November 1994, pages 458-465.
Send comments to Stephen Anthony Edwards at sedwards@eecs.berkeley.edu.