Reverse engineering is the extraction of word level information from a gate-level netlist. It has applications in formal verification, hardware trust, information recovery, and general technology mapping. A preprocessing step finds blocks in a circuit in which word level components are expected. A second step searches for word level components in these blocks. For this second step, we propose two variants of equivalence checking that consider subfunction containment. We propose algorithms to solve these variants by using subgraph isomorphism. A simulation graph (SG) is constructed for the block and for each library component, using a set of permutation-invariant simulation vectors for that component. If a library component SG is a subgraph of the block SG, we have a candidate match, which is then checked by standard equivalence checking. We extend a state-of-the-art subgraph isomorphism algorithm, LAD, to handle simulation graphs efficiently and also propose a SAT-based formulation. Experimental evaluations show that our algorithms can efficiently find 32-bit arithmetic components in blocks with over 300 primary inputs.

Product line (PL) engineering promotes the development of families of related products, where individual products are differentiated by which optional features they include. Modelling and analyzing requirements models of PLs allows for early detection and correction of requirements errors -- including unintended feature interactions, which are a serious problem in feature-rich systems. A key challenge in analyzing PL requirements is the efficient verification of the product family, given that the number of products is too large to be verified one at a time. Recently, it has been shown how the high-level design of an entire PL, that includes all possible products, can be compactly represented as a single model in the SMV language, and model checked using the NuSMV tool. The implementation in NuSMV uses BDDs, a method that has been outperformed by SAT-based algorithms. In this paper we develop PL model checking using two leading SAT-based symbolic model checking algorithms: IMC and IC3. We describe the algorithms, prove their correctness, and report on our implementation. Evaluating our methods on three PL models from the literature, we demonstrate an improvement of up to 3 orders of magnitude over the existing BDD-based method.