rust_formal_verification/
lib.rs

1//! Utilities for the creation and use of bit-level symbolic model checking algorithms.
2//!
3//! rust_formal_verification provides utilities to read AIGs, to convert them to
4//! useful types such as finite state transition formulas, and some common algorithms.
5//! This crate is for developing and prototyping algorithms for formal verification for hardware
6//! devices. Algorithms like BMC, IC3, PDR and so on...
7//!
8//! # Quick Start
9//!
10//! To get you started quickly, all you need to do is read an .aig file.
11//!
12//! ```
13//! use rust_formal_verification::models::{AndInverterGraph, FiniteStateTransitionSystem};
14//!
15//! // read aig file:
16//! let file_path = "tests/examples/ours/counter.aig";
17//! let aig = AndInverterGraph::from_aig_path(file_path);
18//!
19//! // create boolean logic formulas that represent aig:
20//! let fsts = FiniteStateTransitionSystem::from_aig(&aig, false);
21//!
22//! // the formulas can then be read and turned to strings in DIMACS format.
23//! assert_eq!(fsts.get_initial_relation().to_string(), "p cnf 3 3\n-1 0\n-2 0\n-3 0");
24//! ```
25
26// ************************************************************************************************
27// rust submodule declaration, they get searched in their respective file  names
28// ************************************************************************************************
29
30pub mod algorithms; // requires existence of 'algorithms/mod.rs'
31pub mod formulas; // requires existence of 'formulas/mod.rs'
32pub mod models; // requires existence of 'models/mod.rs'
33pub mod solvers; // requires existence of 'solvers/mod.rs'
34
35// ************************************************************************************************
36// re-exports of structs in these modules to simplify paths for other imports
37// ************************************************************************************************
rust_formal_verification/lib.rs

rust_formal_verification/
lib.rs
