CAD for Assurance of Electronic Systems

RANE: Reversal Assessment of Netlist Encryption

By: Shervin Roshanisefat (George Mason University) and Avesta Sasan (George Mason University)

Stage: RTL, HDL


This package is a collection of pluggable functions and classes in Python for assessing obfuscated circuits. These components include:

  1. A SAT interface using pySMT to easily interface with different SAT solvers
  2. A formal verification tool interface to use SystemVerilog for SAT queries
  3. A graph interface to NetworkX and graph-tools libraries for graph processing
  4. Verilog and bench format IO read/write functions

The toolkit has several modules out-of-the box using the available components:

  • Combinational SAT attack code in less than 250 lines of Python.
  • An unrolling SAT attack implementation using the SAT interface.
  • An unrolling SAT attack implementation using formal verification tool interface configured for Symbiyosys. This module accepts high-level Verilog or SystemVerilog code and treats it as an obfuscated or oracle circuit.
  • Implementations of several obfuscation techniques.

Implemented modules have comparable performance with the available SAT attack binaries implemented in C since SAT calls are handled using binary files.


Shervin Roshanisefat

Input/Output Interface

  • Input: Verilog and Bench files
  • Output: Key information


  • Python
  • Symbiyosys
  • pySMT

Licensing Info

BSD 3-clause