Skip to content
A Modeling and Verification Platform for SoCs using ILAs
Branch: master
Clone or download
zhanghongce Merge pull request #81 from zhanghongce/cover-up
Update Verilog Parser Reference
Latest commit 61f90d3 Mar 13, 2019
Type Name Latest commit message Commit time
Failed to load latest commit information.
.github/ISSUE_TEMPLATE Update issue template Jan 24, 2019
boilerplate Remove examples except the boiler plate project template Jan 24, 2019
cmake Fix z3 lib name list Jan 27, 2019
docs Move doxygen output and paper to ILAng-Doc Feb 13, 2019
include Merge branch 'master' of into cove… Mar 1, 2019
scripts Unify md style Feb 5, 2019
src Merge branch 'master' of into cove… Mar 1, 2019
test Merge branch 'master' of into cove… Mar 1, 2019
.clang-format Format and config (LLVM) Nov 27, 2018
.gitignore add vtargetgen test Dec 25, 2018
.gitmodules Remove examples except the boiler plate project template Jan 24, 2019
CMakeLists.txt Update version Jan 27, 2019
LICENSE Update README for z3 instructions Feb 24, 2019


Build Status Build Status Build status Coverage Status Codacy Badge Language grade: C/C++ Percentage of issues still open license Documentation Documentation docker



ILAng requires CMake (3.8 or above) and compilers with CXX11 support. To install dependencies on Debian-based UNIX:

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

To install dependencies on OSX:

brew install bison flex boost boost-python z3
  • The z3 SMT solver (over 4.4.0) is required. Detailed instruction for building latest z3 can be found here.
  • The Boost package is required only for building the synthesis engine and the Python API.

Tested Environments

OS Compiler CMake z3 Boost Status
Ubuntu 14.04 (Trusty) gcc 4.8.4 3.8.0 4.7.1 1.54 Build Status
Ubuntu 16.04 (Xenial) gcc 5.4.0 3.12.4 4.4.1 1.58 Build Status
Ubuntu 16.04 (Xenial) clang 7.0.0 3.12.4 4.4.1 1.58 Build Status
Ubuntu 18.04 (Bionic) gcc 7.3.0 3.13.1 latest 1.65 Build status
OSX 10.13.0 (High Sierra) Xcode 9.4.1 3.11.4 4.8.4 1.68 Build Status

Default Build

To build ILAng with default configuration, create a build directory and execute:

mkdir -p build && cd build
cmake .. 
make -j$(nproc)

After the build complete, run unit tests and install the library.

make run_test
sudo make install


  • Use -DILANG_FETCH_DEPS=OFF to disable config-time updating submodules for in-source dependencies.
  • Use -DILANG_BUILD_TEST=OFF to disalbe building the unit tests.
  • Use -DILANG_BUILD_SYNTH=OFF to disable building the synthesis engine.
  • Use -DILANG_INSTALL_DEV=ON to enable installing working features.

CMake Integration

You can use the ilang::ilang interface target in CMake. This target populates the appropriate usage requirements for include directories, linked libraries, and compile features. To use the ILAng library, ilang++.h is the file to include. (This does not include working features.)

// cxx source
#include <ilang/ilang++.h>

void foo () {
  auto m = ilang::Ila("new_ila_model");


To use the ILAng 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(ilang REQUIRED)
add_library(my_proj ...)
target_link_libraries(my_proj PRIVATE ilang::ilang)


ILAng 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:

# CMakeLists.txt
add_library(my_proj ...)
target_link_libraries(my_proj PRIVATE ilang::ilang)

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
option(MY_PROJ_USE_EXTERNAL_ILANG "Use an external ILAng library" OFF)
add_library(my_proj ...)
target_link_libraries(my_proj PRIVATE ilang::ilang)
# externals/CMakeLists.txt
  find_package(ilang REQUIRED)

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

Docker Image

docker-io docker-image docker-version

An docker image with the ILAng platform and all dependencies can be fetched from Docker Hub.

docker pull byhuang/ilang:latest

Once the container is initiated, run


to initialize the environment settings. This docker image also contains the model checker CoSA with the SMT solvers z3 and Boolector.

You can’t perform that action at this time.