mohdsm81 / romp

romp is a verification tool that uses the murphi verification language along side a parallelized random walk of the state-space to perform verification tasks.

romp

romp is a verification tool that uses the murphi verification language along side a parallelized random walk of the state-space to perform verification tasks.

It utilizes libmurphi which is a custom fork of rumur's librumur murphi parsing library, and CMake build system.

Building from Source

First you will need to have the following dependencies installed:

• Either GCC or Clang
• Bison
• CMake
• Flex
• Libgmp
• Python ≥ 3.4

Then:

# Download romp
git clone https://github.com/civic-fv/romp
cd romp

# Configure and compile
mkdir build
cd build
cmake ..
make
make install

# Generate a checker
romp my-model.m

# Compile the checker
cc -std=c++17 -pthread -O3 -o my-model.romp my-model.romp.cpp

# Run the checker
./a.out

Compilation produces several artifacts including the romp binary itself:

• romp: Tool for translating a Murphi model into a program that implements a checker;;
• libmurphi.a: A library for building your own Murphi model tools; and
• include/murphi/: The API for the above library.

Tests

There is a directory (tests/) full of test models to run with the checker, accompanied by an instructional README.md

Legal

Everything in this repository is in the public domain, under the terms of the Unlicense. For the full text, see LICENSE.