Improving Bounded Model Checkers Scalability for Circuit De-Obfuscation: An Exploration

With the globalization and distribution of the semiconductor supply chain, intellectual property (IP) protection has become a necessity. Recent years have witnessed a surge of interest in logic locking as a proactive IP protection solution. However, in recent years, we also have seen an increase in logic/circuit de-obfuscation attacks that put the strength of logic locking at risk. One of these attacks on locked circuits is the bounded-model-checker (BMC)-based attack, where the adversary has limited access to the design-for-testability (DFT) (known as scan chain). While the BMC-based attack is widely known as an algorithmic attack, numerous studies show that the attack lacks scalability since it has two unrolling factors: sequential unrolling and miter duplication. Inspired by straightforward heuristics widely used for satisfiability problems in the computer science SAT community, in this paper, we will explore a set of methodologies that can have a significant impact on mitigating the BMC attack's scalability issue. For this purpose, through the BMC attack process, we explore the efficacy of "restart" and "initialization" on the attack performance, in which we apply some modification on the locked design before ("initialization") or within ("restart") the BMC execution. By applying "restart" and "initialization" in numerous different configurations, our experimental results show >85% consistent improvement in the BMC attack that can lead to a stronger algorithmic attack scenario on logic locking.