Skip to content
A Modeling and Verification Platform for SoCs using ILAs
Branch: master
Clone or download
Pull request Compare This branch is even with Bo-Yuan-Huang:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.github/ISSUE_TEMPLATE
boilerplate
cmake
docs
extern
include
scripts
src
test
.clang-format
.gitignore
.gitmodules
.lgtm.yml
.travis.yml
CMakeLists.txt
LICENSE
README.md

README.md

ILAng

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

Build

Prerequisites

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

Options

  • 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");
}

External

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)

Embedded

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

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

source init.sh

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.