Boolean Satisfiability Attack and Its Use in VLSI Testing

Instructor 

Dr. Ujjwal Guin is a Godbold Associate Professor in the Department of Electrical and Computer Engineering at Auburn University.

Learning Objectives

Boolean Satisfiability Analysis, commonly referred to as SAT analysis, seeks to determine the satisfiability of a given propositional logic formula. Using a locked circuit and its unlocked counterpart, Boolean Satisfiability (SAT) attacks rely on algorithms based on satisfiability checking to determine the keys of a logic-locked circuit. In this course, we will discuss the foundational concepts of Boolean Satisfiability Analysis, explore the SAT attack, and examine the effectiveness of various logic locking schemes against the SAT attack. Additionally, this course will explore the possibility of repurposing the SAT attack tool to generate test patterns for logic circuit testing. The course includes a series of simulation tutorials that provide hands-on experience with the key concepts discussed.

This course is divided into five modules:

• Unit 1: This section covers the fundamentals of Boolean Satisfiability Analysis. Additionally, it offers a detailed, step-by-step guide on utilizing SAT methods to detect stuck-at faults during VLSI testing. A demonstration of an SAT solver, MiniSat, is provided to show the test pattern generation of a circuit. (Auburn Module: 2)
• Unit 2: This section explains the Boolean Satisfiability (SAT) attack, along with comprehensive guidance on implementing this attack using a dedicated SAT attack tool. This section includes a demonstration that showcases the practical application of the SAT attack, illustrating step-by-step usage of the tool. (Auburn Module: 3)
• Unit 3: A thorough exploration of the SAT attack, exploiting Distinguishing Input patterns (DIPs) and systematic oracle responses to unlock the key value, is provided. The mechanism of how the SAT attack achieves efficiency by reducing the key spaces exponentially is explained. (Auburn Module: 4)
• Unit 4: The trainees will get an overview of SAT-based Automatic Test Pattern Generation (ATPG) techniques for simple stuck-at-fault detection. The section also explores the process of generalizing a circuit modeled for stuck-at-fault testing to its equivalent logic-locking counterpart. A miter circuit construction to effectively generate test patterns will be provided. (Auburn Module: 5)
• Unit 5: A comprehensive framework leveraging the SAT attack tool is introduced, which generates test patterns for multiple faults not detected by the commercial ATPG tool. It will also cover a framework for classifying redundant and non-redundant faults. (Auburn Module: 6)

Prerequisites:

• A basic understanding of circuits, gates, and VLSI testing is required.
• Knowledge of Boolean expressions and mathematical modeling of circuits to CNF equations is helpful but not required.
• A basic understanding of Linux systems is required.
• The knowledge of commercial ATPG tools like TetraMax is helpful but not required.

Biography

Ujjwal Guin is a Godbold Associate Professor in the Department of Electrical and Computer Engineering at Auburn University. He received his Ph.D. from the University of Connecticut in 2016. He is actively engaged in research projects spanning hardware security and trust, supply chain security, cybersecurity, and VLSI design and testing. He has developed several on-chip structures and techniques to enhance the security, trustworthiness, and reliability of integrated circuits. His contributions include authoring one book, two book chapters, thirty journal articles, and more than forty refereed conference papers. His research has been widely recognized through best paper nominations, awards, research grants, and prizes from various security competitions. Notably, one of his papers was referenced in the White House 100-Day Reviews under the EO 14017 report, specifically in the “Building Resilient Supply Chains” section, published in June 2021. Dr. Guin’s research projects are funded by the U.S. Army, the Air Force Office of Scientific Research (AFOSR), the Secret Service, the National Science Foundation (NSF), and the Air Force Research Laboratory (AFRL). He served on the technical program committees of several prestigious conferences, including DAC, ITC, HOST, VTS, PAINE, VLSID, GLSVLSI, ISVLSI, and Blockchain. He is currently the Technical Program Co-Chair of HOST 2025. He is a Senior Member of IEEE and ACM.