This course was developed as a MEST Micro-Certificate. MEST Micro-Certificates offer short, self-paced learning opportunities through focused training modules and webinars on specialized technical topics. Participants who successfully complete the program requirements earn a certificate of completion.
These programs are designed for U.S. citizens, including Department of War and other government personnel, government-affiliated employees, industry professionals, college students, and faculty.
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.
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.
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.
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.
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.
Format: Online, asynchronous
Platform: nanoHUB
Estimated Time: 30 hours
Level: Advanced Undergraduate/Graduate Student
Prerequisites: A basic understanding of circuits, gates, and VLSI testing. A basic understanding of Linux systems.
Instructor: Professor Ujjwal Guin, Auburn University
Course Objectives:
Explain Boolean Satisfiability Analysis concepts
Apply SAT methods for stuck-at fault detection
Implement SAT attacks using the dedicated tool
Analyze DIPs and oracle responses to recover keys
Design SAT-based ATPG frameworks for fault classification
Request Course Enrollment
To enroll in this course, you must have a nanoHUB account. Create one here: https://nanohub.org/register/
Request membership in the MEST group in nanoHUB at https://nanohub.org/groups/mest