CAD for Assurance of Electronic Systems

Functional Corruptibility-Guided SAT-Based Attack on Sequential Logic Encryption

By: Yinghua Hu (University of Southern California), Yuke Zhang (University of Southern California), Kaixin Yang (University of Southern California), Dake Chen (University of Southern California), Peter A. Beerel (University of Southern California), and Pierluigi Nuzzo (University of Southern California)

Stage: Gate-Level


Fun-SAT is a Boolean satisfiability (SAT)-based attack against sequential logic locking. Fun-SAT relies on a notion of functional corruptibility for a sequential circuit to efficiently estimate the minimum unrolling depth required for a successful SAT attack to prune out of the search space all the wrong keys of a locked circuit. Therefore, in a SAT-based attack to sequential logic locking, Fun-SAT can significantly reduce both the SAT-attack effort spent to produce candidate keys and the model checking effort spent to prove that a set of candidate keys is correct. The attack can effectively be used to evaluate the security of sequential locking schemes.


Yinghua Hu

Input/Output Interface

  • Input: Gate-level netlist of the locked circuit, oracle access to the original circuit, and cycle length of the key sequence
  • Output: Correct key sequence


Python 3.6 or higher version
nuXmv (
Synopsys VCS (
SAT attack tool (

Licensing Info

MIT License


Hu, Yinghua; Zhang, Yuke; Yang, Kaixin; Chen, Dake; Beerel, Peter A.; Nuzzo, Pierluigi

Fun-SAT: Functional Corruptibility-Guided SAT-Based Attack on Sequential Logic Encryption Proceedings Article

In: 2021 IEEE International Symposium on Hardware Oriented Security and Trust (HOST), IEEE, 2021.

Abstract | Links | BibTeX


  • This work was supported in part by the Air Force Research Laboratory (AFRL) and the Defense Advanced Research Projects Agency (DARPA) under agreement number FA8650-18-1-7817.