Description
Systems are increasingly being constructed from off-the-shelf components acquired through a globally distributed supply chain. There is a rising concern over the trustworthiness of these components, especially when used in mission-critical applications. In this report, we present a systematic framework for automatically deriving high-level functions and structures from the gate-level netlist of a digital circuit. First, we formally define the problem of reverse engineering a bit-level description into the corresponding high-level description of a digital circuit. We then present a portfolio of techniques for solving this problem with judicious use of formal methods.