Ecient Verication and Synthesis using Design Commonalities

In this paper we solve the problem of identify-ing a \matching " between two logic circuits or \net-works". A matching is a functions that maps each gate or \node " in the new circuit into one in the old circuit (if a matching does not exist it maps it to null). We present both an exact and a heuristic way to solve the maximal matching problem. The matching problem does not require any input corre-spondences. The purpose is to identify structurally identical regions in the networks, and exploit the commonality between them for more ecient ver-i cation and synthesis. Synthesis and verication tools that recognize commonalities both between two versions of the same design, as well within a single design, may be able to outperform their counterparts that do not utilize these commonalities. This work is concerned with detecting structural "matchings " that may be re-utilized.