  Due to the adoption of horizontal business models following the globalization
of semiconductor manufacturing, the overproduction of integrated circuits (ICs)
and the piracy of intellectual properties (IPs) can lead to significant damage
to the integrity of the semiconductor supply chain. Logic locking emerges as a
primary design-for-security measure to counter these threats, where ICs become
fully functional only when unlocked with a secret key. However, Boolean
satisfiability-based attacks have rendered most locking schemes ineffective.
This gives rise to numerous defenses and new locking methods to achieve SAT
resiliency. This paper provides a unique perspective on the SAT attack
efficiency based on conjunctive normal form (CNF) stored in SAT solver. First,
we show how the attack learns new relations between keys in every iteration
using distinguishing input patterns and the corresponding oracle responses. The
input-output pairs result in new CNF clauses of unknown keys to be appended to
the SAT solver, which leads to an exponential reduction in incorrect key
values. Second, we demonstrate that the SAT attack can break any locking scheme
within linear iteration complexity of key size. Moreover, we show how key
constraints on point functions affect the SAT attack complexity. We explain why
proper key constraint on AntiSAT reduces the complexity effectively to constant
1. The same constraint helps the breaking of CAS-Lock down to linear iteration
complexity. Our analysis provides a new perspective on the capabilities of SAT
attack against multiplier benchmark c6288, and we provide new directions to
achieve SAT resiliency.
