add assert_formal helper for running formal proofs in rust tests

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;

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