CAD for Assurance of Electronic Systems


By: Rakibul Hassan (George Mason University), Gaurav Kohle (UC Davis), Setareh Rafatirad (UC Davis), Houman Homayoun (UC Davis), and Sai Manoj Pudukotai Dinakarrao (George Mason University)

Stage: Gate-Level


We propose a neural network-based cognitive SAT to SAT-hard clause translator under the constraints of minimal PPA overheads while preserving the original functionality with impenetrable security. Our proposed method is incubated with a SAT-hard clause generator that translates the existing conjunctive normal form (CNF) through minimal perturbations such as inclusion of pair of inverters or buffers or adding new lightweight SAT-hard block depending on the provided CNF. For efficient SAT-hard clause generation, the proposed method is equipped with a multi-layer neural network that first learns the dependencies of features (literals and clauses), followed by a long-short-term-memory (LSTM) network to validate and backpropagate the SAT-hardness for better learning and translation. For a fair comparison with the state-of-the-art, we evaluate our proposed technique on ISCAS’85 and ISCAS’89 benchmarks. It is seen to successfully defend against multiple state-of-the-art SAT attacks devised for hardware RE with minimal overheads.


Rakibul Hassan

Input/Output Interface

  • Input: ISCAS’85 Bench File
  • Output: Obfuscated Netlist


MiniSAT SAT solver


Selsam, Daniel; Lamm, Matthew; Bünz, Benedikt; Liang, Percy; de Moura, Leonardo; Dill, David L

Learning a SAT Solver from Single-Bit Supervision Journal Article

In: CoRR, vol. abs/1802.03685, 2018.

Links | BibTeX