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.
First you will need to have the following dependencies installed:
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.
There is a directory (tests/) full of test models to run with the checker, accompanied by an instructional README.md
Everything in this repository is in the public domain, under the terms of the Unlicense. For the full text, see LICENSE.