PrincetonUniversity / ILAng

• Build

  • Prerequisites
  • Default Build
  • Options

• CMake Integration

  • External
  • Embedded
  • Supporting Both

• Docker

• License

• Contributing

Build

Prerequisites

ILAng requires CMake (3.9.6 or above) and compilers with C++17 support. To install dependencies on Debian-based Linux:

apt-get install bison flex z3 libz3-dev

To install dependencies (besides z3) on Fedora-based Linux:

yum install bison flex

To install dependencies on OSX:

brew install bison flex z3

Default Build

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

mkdir -p build && cd build
cmake .. 
make

If you are using git older than 1.8.4, init the submodule from root and disable config-time submodule fetching:

git submodule update --init --recursive
mkdir -p build && cd build
cmake .. -DILANG_FETCH_DEPS=OFF
make

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

make run_test
sudo make install

Options

• Use -DILANG_FETCH_DEPS=OFF to disable config-time submodule fetching.
• Use -DILANG_BUILD_TEST=OFF to disalbe building the unit tests.
• Use -DILANG_BUILD_SYNTH=ON to enable building the synthesis engine (required Boost).
• Use -DILANG_BUILD_INVSYN=OFF to disable building invariant synthesis feature.
• Use -DILANG_BUILD_SWITCH=ON to enable building smt-switch interface support.
• Use -DILANG_BUILD_COSIM=ON to enable building Xilinx cosimulation support.
• Use -DILANG_INSTALL_DEV=ON to install 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");
}

An example can be found in the template repo PrincetonUniversity/template-ila.

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

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 solver z3.

License

ILAng is licensed under the MIT license:

Copyright © 2018 Princeton University

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

ILAng contains the Google logging module, which is licensed under glog license. Copyright (c) 2008, Google Inc.

ILAng contains the Google Test project, which is licensed under googletest license. Copyright 2008, Google Inc.

ILAng contains the JSON library, which is licensed under the MIT License. Copyright (c) 2013-2019 Niels Lohmann.

ILAng contains the fmt, which is licensed under License. Copyright (c) 2012-present, Victor Zverovich.

ILAng uses the Verilog parser, which is licensed under the MIT License. Copyright (c) 2016 Ben Marshall.

ILAng uses the VCD parser, which is licensed under the MIT License. Copyright (c) 2018 Ben Marshall.

ILAng uses the SMT parser, which is licensed under the MIT License. Copyright (c) 2010 Alberto Griggio.

ILAng uses the smt-switch, which is licensed under the BSD 3-Clause License. Copyright (c) 2019-2020 the authors.

ILAng uses ItSy, which is licensed under the MIT License. Copyright (c) 2016 Princeton University.

Contributing

Please refer to CONTRIBUTING for further details.