Formal Methods for Reverse Engineering Gate-Level Netlists.

摘要

In this report, we present a systematic framework for automatically deriving high-level structures from the gate-level netlist of a digital circuit, and techniques that specifically address each of these challenges. To cope with the large functional space, we crafted a library that contains more than a thousand commonly used components. Leveraging formal verification techniques such as symbolic evaluation, model checking and equivalence checking, we further address the problem of a large implementation space per function, and recover structure from an unstructured netlist.