rust-formal-verification

一个Rust库，它使开发、原型设计和测试新的形式化验证算法（如IC3、PDR、AVY等）变得更加容易。

发布新版本

要发布库的新版本，请运行

1. cargo fmt --check（您也可以运行cargo fmt来快速修复更改）
2. 运行cargo clippy（您也可以运行cargo clippy --fix来快速修复更改）
3. 运行cargo test（这也会测试文档注释）
4. 运行cargo publish

lib.rs:

用于创建和使用位级符号模型检查算法的实用程序。

rust_formal_verification提供读取AIGs、将它们转换为有限状态转换公式等有用类型以及一些常见算法的实用程序。此crate是为开发硬件设备的形式化验证算法而设计的。如BMC、IC3、PDR等算法...

快速入门

为了快速入门，您只需读取一个.aig文件。

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");