• Dependencies

• Building

  • Boost for Python API
  • CMake for C++ Projects

• Python API

• CMake Integration

  • External
  • Embedded
  • Supporting Both

About

This is an implementation of the templated-based Instruction-Level Abstraction (ILA) synthesis based on TCAD18.

Dependencies

• z3 4.4.0 or above.
• boost 1.50.0 or above.

For Debian-based UNIX, you can install by running

apt-get install libboost-all-dev z3 libz3-dev

For OSX, you can install by running

brew install boost boost-python z3

Building

The ILA synthesis engine support build using Boost bjam and CMake. Currently, unit tests are available in the Boost build only.

Boost for Python API

cd /root/of/this/repo
bjam -j$(nproc)

CMake for Cpp Projects

cd /root/of/this/repo
mkdir -p build
cd build
cmake ..
make -j$(nproc)

Python API

You need to first export the library.

# bash
export PYTHONPATH=$(pwd)/build:$PYTHONPATH

# Python 
import ila
abs = ila.Abstraction("test")

CMake Integration

You can use the ilasynth::ilasynth interface target in CMake. This target populates the appropriate usage requirements for include directories, linked libraries, and compile features.

#include <ilasynth/abstraction.hpp>

void foo () {
  auto m = ilasynth::Abstraction("new_abstraction");
}

External

To use the library from a CMake project, you can locate it directly with find_package() and use the namespaced imported target from the generated package configuration:

# CMakeLists.txt
find_package(ilasynth REQUIRED)
...
add_library(my_proj ...)
...
target_link_libraries(my_proj PRIVATE ilasynth::ilasynth)

Embedded

It also supports embedded build, but is not recommended due to its size. To embed the library directly into an existing CMake project, place the entire source tree in a subdirectory and call add_subdirectory() in your CMakeLists.txt file:

add_subdirectory(ilasynth)
...
add_library(my_proj ...)
...
target_link_libraries(my_proj PRIVATE ilasynth::ilasynth)

Supporting Both

To allow your project to support either an externally installed or an embedded library, you can use the following pattern:

# Top level CMakeLists.txt
project(MY_PROJ)
...
option(MY_PROJ_USE_EXTERNAL_ILASYNYH "Use an external library" OFF)
...
add_subdirectory(externals)
...
add_library(my_proj ...)
...
target_link_libraries(my_proj PRIVATE ilasynth::ilasynth)

# externals/CMakeLists.txt
...
if(MY_PROJ_USE_EXTERNAL_ILASYNTH)
  find_package(ilasynth REQUIRED)
else()
  add_subdirectory(ilasynth)
endif()
...

externals/ilasynth is then a complete copy of this source tree, if enabled.

Contributors

• Pramod Subramanyan
• Bo-Yuan Huang
• Hongce Zhang
• Yakir Vizel