rust-formal-verification

A rust library that makes it easier to develop, prototype and test new algorithms for formal verification like IC3, PDR, AVY and others.

Publishing a new version

To publish a new version of the library :

1. run cargo fmt --check (you may run cargo fmt to fix changes quickly)
2. run cargo clippy (you may run cargo clippy --fix to fix changes quickly)
3. run cargo test (This also tests doc comments)
4. run cargo publish

lib.rs:

Utilities for the creation and use of bit-level symbolic model checking algorithms.

rust_formal_verification provides utilities to read AIGs, to convert them to useful types such as finite state transition formulas, and some common algorithms. This crate is for developing and prototyping algorithms for formal verification for hardware devices. Algorithms like BMC, IC3, PDR and so on...

Quick Start

To get you started quickly, all you need to do is read an .aig file.

use rust_formal_verification::models::{AndInverterGraph, FiniteStateTransitionSystem};

// read aig file:
let file_path = "tests/examples/ours/counter.aig";
let aig = AndInverterGraph::from_aig_path(file_path);

// create boolean logic formulas that represent aig:
let fsts = FiniteStateTransitionSystem::from_aig(&aig, false);

// the formulas can then be read and turned to strings in DIMACS format.
assert_eq!(fsts.get_initial_relation().to_string(), "p cnf 3 3\n-1 0\n-2 0\n-3 0");