Instruction-Level Abstraction (ILA)

A paper summarizing the formal definition and modeling case studies: arXiv link.

Templated-based ILA synthesis

To build ILA synthesis tool, look in the py-tmpl-synth directory.

For API documents and tutorials, see the docs directory.

Modeling and Verification Case Studies

For some examples, see the examples directory.

ILA description and C++ API

Requirements:

• z3 4.4.0 or above
• CMake 2.8 or above
• glog

Building with Cmake:

  mkdir -p build
  cd build
  cmake .. -DZ3_INCLUDE_DIR=<path/to/z3/header>
  make install

For tutorial, see c++ api example.

For API documentation, see the page ILA-Tools-API.

For developers, implementation details can be found on ILA-Tools-Impl.

Publications:

• Formal Security Verification of Concurrent Firmware in SoCs using Instruction-Level Abstraction for Hardware. Bo-Yuan Huang, Sayak Ray, Aarti Gupta, Jason Fung, and Sharad Malik. in Proceedings of the Design Automation Conference. (DAC 2018), San Francisco, CA. June 2018.

• Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification. Bo-Yuan Huang, Hongce Zhang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta, and Sharad Malik. [arXiv:1801.01114] [PDF]

• Template-based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification. Pramod Subramanyan, Bo-Yuan Huang, Yakir Vizel, Aarti Gupta, and Sharad Malik. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 2017. [PDF]

• Invited: Specification and Modeling for Systems-on-Chip Security Verification. Sharad Malik and Pramod Subramanyan. in Proceedings of the Design Automation Conference. (DAC 2016), Austin, TX. June 2016. [PDF]

• Verifying Information Flow Properties of Firmware using Symbolic Execution. Pramod Subramanyan, Sharad Malik, Hareesh Khattri, Abhranil Maiti and Jason Fung. in Proceedings of Design Automation and Test in Europe. (DATE 2016). Dresden, Germany, March 2016. [PDF]

• Template-based Synthesis of Instruction-Level Abstractions for SoC Verification. Pramod Subramanyan, Yakir Vizel, Sayak Ray and Sharad Malik. in Proceedings of Formal Methods in Computer-Aided Design. (FMCAD 2015). Austin, TX, September 2015. [PDF]