From 5fc7dbd6e9a6c698d817643cb8ff670310614d40 Mon Sep 17 00:00:00 2001
From: Jacob Lifshay <programmerjake@gmail.com>
Date: Wed, 25 Sep 2024 01:54:07 -0700
Subject: [PATCH] add assert_formal helper for running formal proofs in rust
 tests

---
 crates/fayalite/src/lib.rs     |  1 +
 crates/fayalite/src/testing.rs | 36 ++++++++++++++++++++++++++++++++++
 2 files changed, 37 insertions(+)
 create mode 100644 crates/fayalite/src/testing.rs

diff --git a/crates/fayalite/src/lib.rs b/crates/fayalite/src/lib.rs
index 83b61b2..70ce724 100644
--- a/crates/fayalite/src/lib.rs
+++ b/crates/fayalite/src/lib.rs
@@ -50,4 +50,5 @@ pub mod ty;
 pub mod util;
 //pub mod valueless;
 pub mod prelude;
+pub mod testing;
 pub mod wire;
diff --git a/crates/fayalite/src/testing.rs b/crates/fayalite/src/testing.rs
new file mode 100644
index 0000000..8046f05
--- /dev/null
+++ b/crates/fayalite/src/testing.rs
@@ -0,0 +1,36 @@
+// SPDX-License-Identifier: LGPL-3.0-or-later
+// See Notices.txt for copyright information
+use crate::{
+    cli::{FormalArgs, FormalMode, FormalOutput, RunPhase},
+    firrtl::ExportOptions,
+};
+use clap::Parser;
+use std::sync::OnceLock;
+
+fn assert_formal_helper() -> FormalArgs {
+    static FORMAL_ARGS: OnceLock<FormalArgs> = OnceLock::new();
+    // ensure we only run parsing once, so errors from env vars don't produce overlapping output if we're called on multiple threads
+    FORMAL_ARGS
+        .get_or_init(|| FormalArgs::parse_from(["fayalite::testing::assert_formal"]))
+        .clone()
+}
+
+#[track_caller]
+pub fn assert_formal<M>(
+    module: M,
+    mode: FormalMode,
+    depth: u64,
+    solver: Option<&str>,
+    export_options: ExportOptions,
+) where
+    FormalArgs: RunPhase<M, Output = FormalOutput>,
+{
+    let mut args = assert_formal_helper();
+    args.verilog.firrtl.base.redirect_output_for_rust_test = true;
+    args.verilog.firrtl.export_options = export_options;
+    args.verilog.debug = true;
+    args.mode = mode;
+    args.depth = depth;
+    args.solver = solver.map(String::from);
+    args.run(module).expect("testing::assert_formal() failed");
+}