add assert_formal helper for running formal proofs in rust tests

Cargo.lock

@@ -56,7 +56,7 @@ version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ad186efb764318d35165f1758e7dcef3b10628e26d41a44bc5550652e6804391"
 dependencies = [
- "windows-sys",
+ "windows-sys 0.52.0",
 ]
 
 [[package]]
@@ -66,7 +66,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "61a38449feb7068f52bb06c12759005cf459ee52bb4adc1d5a7c4322d716fb19"
 dependencies = [
  "anstyle",
- "windows-sys",
+ "windows-sys 0.52.0",
 ]
 
 [[package]]
@@ -218,7 +218,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "a258e46cdc063eb8519c00b9fc845fc47bcfca4130e2f08e88665ceda8474245"
 dependencies = [
  "libc",
- "windows-sys",
+ "windows-sys 0.52.0",
 ]
 
 [[package]]
@@ -249,8 +249,10 @@ dependencies = [
  "hashbrown",
  "num-bigint",
  "num-traits",
+ "os_pipe",
  "serde",
  "serde_json",
+ "tempfile",
  "trybuild",
  "which",
 ]
@@ -334,7 +336,7 @@ version = "0.5.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "e3d1354bf6b7235cb4a0576c2619fd4ed18183f689b12b006a0ee7329eeff9a5"
 dependencies = [
- "windows-sys",
+ "windows-sys 0.52.0",
 ]
 
 [[package]]
@@ -413,6 +415,16 @@ version = "1.19.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92"
 
+[[package]]
+name = "os_pipe"
+version = "1.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5ffd2b0a5634335b135d5728d84c5e0fd726954b87111f7506a61c502280d982"
+dependencies = [
+ "libc",
+ "windows-sys 0.59.0",
+]
+
 [[package]]
 name = "prettyplease"
 version = "0.2.20"
@@ -457,7 +469,7 @@ dependencies = [
  "errno",
  "libc",
  "linux-raw-sys",
- "windows-sys",
+ "windows-sys 0.52.0",
 ]
 
 [[package]]
@@ -541,7 +553,7 @@ dependencies = [
  "cfg-if",
  "fastrand",
  "rustix",
- "windows-sys",
+ "windows-sys 0.52.0",
 ]
 
 [[package]]
@@ -665,14 +677,24 @@ dependencies = [
 ]
 
 [[package]]
-name = "windows-targets"
-version = "0.52.4"
+name = "windows-sys"
+version = "0.59.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7dd37b7e5ab9018759f893a1952c9420d060016fc19a472b4bb20d1bdd694d1b"
+checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b"
+dependencies = [
+ "windows-targets",
+]
+
+[[package]]
+name = "windows-targets"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973"
 dependencies = [
  "windows_aarch64_gnullvm",
  "windows_aarch64_msvc",
  "windows_i686_gnu",
+ "windows_i686_gnullvm",
  "windows_i686_msvc",
  "windows_x86_64_gnu",
  "windows_x86_64_gnullvm",
@@ -681,45 +703,51 @@ dependencies = [
 
 [[package]]
 name = "windows_aarch64_gnullvm"
-version = "0.52.4"
+version = "0.52.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bcf46cf4c365c6f2d1cc93ce535f2c8b244591df96ceee75d8e83deb70a9cac9"
+checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3"
 
 [[package]]
 name = "windows_aarch64_msvc"
-version = "0.52.4"
+version = "0.52.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "da9f259dd3bcf6990b55bffd094c4f7235817ba4ceebde8e6d11cd0c5633b675"
+checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469"
 
 [[package]]
 name = "windows_i686_gnu"
-version = "0.52.4"
+version = "0.52.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b474d8268f99e0995f25b9f095bc7434632601028cf86590aea5c8a5cb7801d3"
+checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b"
+
+[[package]]
+name = "windows_i686_gnullvm"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66"
 
 [[package]]
 name = "windows_i686_msvc"
-version = "0.52.4"
+version = "0.52.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1515e9a29e5bed743cb4415a9ecf5dfca648ce85ee42e15873c3cd8610ff8e02"
+checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66"
 
 [[package]]
 name = "windows_x86_64_gnu"
-version = "0.52.4"
+version = "0.52.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5eee091590e89cc02ad514ffe3ead9eb6b660aedca2183455434b93546371a03"
+checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78"
 
 [[package]]
 name = "windows_x86_64_gnullvm"
-version = "0.52.4"
+version = "0.52.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "77ca79f2451b49fa9e2af39f0747fe999fcda4f5e241b2898624dca97a1f2177"
+checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d"
 
 [[package]]
 name = "windows_x86_64_msvc"
-version = "0.52.4"
+version = "0.52.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "32b752e52a2da0ddfbdbcc6fceadfeede4c939ed16d13e648833a61dfb611ed8"
+checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec"
 
 [[package]]
 name = "winsafe"

Cargo.toml

@@ -19,10 +19,13 @@ fayalite-proc-macros-impl = { version = "=0.2.0", path = "crates/fayalite-proc-m
 fayalite-visit-gen = { version = "=0.2.0", path = "crates/fayalite-visit-gen" }
 base16ct = "0.2.0"
 bitvec = { version = "1.0.1", features = ["serde"] }
+clap = { version = "4.5.9", features = ["derive", "env", "string"] }
+eyre = "0.6.12"
 hashbrown = "0.14.3"
 indexmap = { version = "2.2.6", features = ["serde"] }
 num-bigint = "0.4.4"
 num-traits = "0.2.16"
+os_pipe = "1.2.1"
 prettyplease = "0.2.20"
 proc-macro2 = "1.0.83"
 quote = "1.0.36"
@@ -33,3 +36,4 @@ syn = { version = "2.0.66", features = ["full", "fold", "visit", "extra-traits"]
 tempfile = "3.10.1"
 thiserror = "1.0.61"
 trybuild = "1.0"
+which = "6.0.1"

crates/fayalite-proc-macros-impl/Cargo.toml

@@ -13,11 +13,11 @@ rust-version.workspace = true
 version.workspace = true
 
 [dependencies]
-base16ct = { workspace = true }
-num-bigint = { workspace = true }
-prettyplease = { workspace = true }
-proc-macro2 = { workspace = true }
-quote = { workspace = true }
-sha2 = { workspace = true }
-syn = { workspace = true }
-tempfile = { workspace = true }
+base16ct.workspace = true
+num-bigint.workspace = true
+prettyplease.workspace = true
+proc-macro2.workspace = true
+quote.workspace = true
+sha2.workspace = true
+syn.workspace = true
+tempfile.workspace = true

crates/fayalite-proc-macros/Cargo.toml

@@ -16,4 +16,4 @@ version.workspace = true
 proc-macro = true
 
 [dependencies]
-fayalite-proc-macros-impl = { workspace = true }
+fayalite-proc-macros-impl.workspace = true

crates/fayalite-visit-gen/Cargo.toml

@@ -13,11 +13,11 @@ rust-version.workspace = true
 version.workspace = true
 
 [dependencies]
-indexmap = { workspace = true }
-prettyplease = { workspace = true }
-proc-macro2 = { workspace = true }
-quote = { workspace = true }
-serde = { workspace = true }
-serde_json = { workspace = true }
-syn = { workspace = true }
-thiserror = { workspace = true }
+indexmap.workspace = true
+prettyplease.workspace = true
+proc-macro2.workspace = true
+quote.workspace = true
+serde.workspace = true
+serde_json.workspace = true
+syn.workspace = true
+thiserror.workspace = true

crates/fayalite/Cargo.toml

@@ -14,22 +14,24 @@ rust-version.workspace = true
 version.workspace = true
 
 [dependencies]
-bitvec = { workspace = true }
-hashbrown = { workspace = true }
-num-bigint = { workspace = true }
-num-traits = { workspace = true }
-fayalite-proc-macros = { workspace = true }
-serde = { workspace = true }
-serde_json = { workspace = true }
-clap = { version = "4.5.9", features = ["derive", "env"] }
-eyre = "0.6.12"
-which = "6.0.1"
+bitvec.workspace = true
+clap.workspace = true
+eyre.workspace = true
+fayalite-proc-macros.workspace = true
+hashbrown.workspace = true
+num-bigint.workspace = true
+num-traits.workspace = true
+os_pipe.workspace = true
+serde_json.workspace = true
+serde.workspace = true
+tempfile.workspace = true
+which.workspace = true
 
 [dev-dependencies]
-trybuild = { workspace = true }
+trybuild.workspace = true
 
 [build-dependencies]
-fayalite-visit-gen = { workspace = true }
+fayalite-visit-gen.workspace = true
 
 [features]
 unstable-doc = []

crates/fayalite/src/cli.rs

@@ -2,16 +2,18 @@
 // See Notices.txt for copyright information
 use crate::{
     bundle::{Bundle, BundleType},
-    firrtl,
+    firrtl::{self, ExportOptions},
     intern::Interned,
     module::Module,
+    util::streaming_read_utf8::streaming_read_utf8,
 };
 use clap::{
     builder::{OsStringValueParser, TypedValueParser},
-    Args, Parser, Subcommand, ValueEnum, ValueHint,
+    Parser, Subcommand, ValueEnum, ValueHint,
 };
 use eyre::{eyre, Report};
 use std::{error, ffi::OsString, fmt, io, path::PathBuf, process};
+use tempfile::TempDir;
 
 pub type Result<T = (), E = CliError> = std::result::Result<T, E>;
 
@@ -42,56 +44,119 @@ pub trait RunPhase<Arg> {
     fn run(&self, arg: Arg) -> Result<Self::Output>;
 }
 
-#[derive(Args, Debug)]
+#[derive(Parser, Debug, Clone)]
 #[non_exhaustive]
 pub struct BaseArgs {
     /// the directory to put the generated main output file and associated files in
-    #[arg(short, long, value_hint = ValueHint::DirPath)]
-    pub output: PathBuf,
+    #[arg(short, long, value_hint = ValueHint::DirPath, required = true)]
+    pub output: Option<PathBuf>,
     /// the stem of the generated main output file, e.g. to get foo.v, pass --file-stem=foo
     #[arg(long)]
     pub file_stem: Option<String>,
+    #[arg(long, env = "FAYALITE_KEEP_TEMP_DIR")]
+    pub keep_temp_dir: bool,
+    #[arg(skip = false)]
+    pub redirect_output_for_rust_test: bool,
 }
 
 impl BaseArgs {
-    pub fn to_firrtl_file_backend(&self) -> firrtl::FileBackend {
-        firrtl::FileBackend {
-            dir_path: self.output.clone(),
-            top_fir_file_stem: self.file_stem.clone(),
+    fn make_firrtl_file_backend(&self) -> Result<(firrtl::FileBackend, Option<TempDir>)> {
+        let (dir_path, temp_dir) = match &self.output {
+            Some(output) => (output.clone(), None),
+            None => {
+                let temp_dir = TempDir::new()?;
+                if self.keep_temp_dir {
+                    let temp_dir = temp_dir.into_path();
+                    println!("created temporary directory: {}", temp_dir.display());
+                    (temp_dir, None)
+                } else {
+                    (temp_dir.path().to_path_buf(), Some(temp_dir))
+                }
+            }
+        };
+        Ok((
+            firrtl::FileBackend {
+                dir_path,
+                top_fir_file_stem: self.file_stem.clone(),
+                circuit_name: None,
+            },
+            temp_dir,
+        ))
+    }
+    /// handles possibly redirecting the command's output for Rust tests
+    pub fn run_external_command(
+        &self,
+        mut command: process::Command,
+    ) -> io::Result<process::ExitStatus> {
+        if self.redirect_output_for_rust_test {
+            let (reader, writer) = os_pipe::pipe()?;
+            let mut reader = io::BufReader::new(reader);
+            command.stderr(writer.try_clone()?);
+            command.stdout(writer); // must not leave writer around after spawning child
+            command.stdin(process::Stdio::null());
+            let mut child = command.spawn()?;
+            drop(command); // close writers
+            Ok(loop {
+                let status = child.try_wait()?;
+                streaming_read_utf8(&mut reader, |s| {
+                    // use print! so output goes to Rust test output capture
+                    print!("{s}");
+                    io::Result::Ok(())
+                })?;
+                if let Some(status) = status {
+                    break status;
+                }
+            })
+        } else {
+            command.status()
         }
     }
 }
 
-#[derive(Args, Debug)]
+#[derive(Parser, Debug, Clone)]
 #[non_exhaustive]
 pub struct FirrtlArgs {
     #[command(flatten)]
     pub base: BaseArgs,
+    #[command(flatten)]
+    pub export_options: ExportOptions,
 }
 
 #[derive(Debug)]
 #[non_exhaustive]
 pub struct FirrtlOutput {
     pub file_stem: String,
+    pub top_module: String,
+    pub output_dir: PathBuf,
+    pub temp_dir: Option<TempDir>,
 }
 
 impl FirrtlOutput {
-    pub fn firrtl_file(&self, args: &FirrtlArgs) -> PathBuf {
-        let mut retval = args.base.output.join(&self.file_stem);
-        retval.set_extension("fir");
+    pub fn file_with_ext(&self, ext: &str) -> PathBuf {
+        let mut retval = self.output_dir.join(&self.file_stem);
+        retval.set_extension(ext);
         retval
     }
+    pub fn firrtl_file(&self) -> PathBuf {
+        self.file_with_ext("fir")
+    }
 }
 
 impl FirrtlArgs {
     fn run_impl(&self, top_module: Module<Bundle>) -> Result<FirrtlOutput> {
+        let (file_backend, temp_dir) = self.base.make_firrtl_file_backend()?;
         let firrtl::FileBackend {
-            top_fir_file_stem, ..
-        } = firrtl::export(self.base.to_firrtl_file_backend(), &top_module)?;
+            top_fir_file_stem,
+            circuit_name,
+            dir_path,
+        } = firrtl::export(file_backend, &top_module, self.export_options)?;
         Ok(FirrtlOutput {
             file_stem: top_fir_file_stem.expect(
                 "export is known to set the file stem from the circuit name if not provided",
             ),
+            top_module: circuit_name.expect("export is known to set the circuit name"),
+            output_dir: dir_path,
+            temp_dir,
         })
     }
 }
@@ -122,7 +187,22 @@ pub enum VerilogDialect {
     Yosys,
 }
 
+impl fmt::Display for VerilogDialect {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.write_str(self.as_str())
+    }
+}
+
 impl VerilogDialect {
+    pub fn as_str(self) -> &'static str {
+        match self {
+            VerilogDialect::Questa => "questa",
+            VerilogDialect::Spyglass => "spyglass",
+            VerilogDialect::Verilator => "verilator",
+            VerilogDialect::Vivado => "vivado",
+            VerilogDialect::Yosys => "yosys",
+        }
+    }
     pub fn firtool_extra_args(self) -> &'static [&'static str] {
         match self {
             VerilogDialect::Questa => &["--lowering-options=emitWireInPorts"],
@@ -140,7 +220,7 @@ impl VerilogDialect {
     }
 }
 
-#[derive(Args, Debug)]
+#[derive(Parser, Debug, Clone)]
 #[non_exhaustive]
 pub struct VerilogArgs {
     #[command(flatten)]
@@ -158,6 +238,8 @@ pub struct VerilogArgs {
     /// adapt the generated Verilog for a particular toolchain
     #[arg(long)]
     pub verilog_dialect: Option<VerilogDialect>,
+    #[arg(long, short = 'g')]
+    pub debug: bool,
 }
 
 #[derive(Debug)]
@@ -167,28 +249,37 @@ pub struct VerilogOutput {
 }
 
 impl VerilogOutput {
-    pub fn verilog_file(&self, args: &VerilogArgs) -> PathBuf {
-        let mut retval = args.firrtl.base.output.join(&self.firrtl.file_stem);
-        retval.set_extension("v");
-        retval
+    pub fn verilog_file(&self) -> PathBuf {
+        self.firrtl.file_with_ext("v")
     }
 }
 
 impl VerilogArgs {
     fn run_impl(&self, firrtl_output: FirrtlOutput) -> Result<VerilogOutput> {
+        let Self {
+            firrtl,
+            firtool,
+            firtool_extra_args,
+            verilog_dialect,
+            debug,
+        } = self;
         let output = VerilogOutput {
             firrtl: firrtl_output,
         };
-        let mut cmd = process::Command::new(&self.firtool);
-        cmd.arg(output.firrtl.firrtl_file(&self.firrtl));
+        let mut cmd = process::Command::new(firtool);
+        cmd.arg(output.firrtl.firrtl_file());
         cmd.arg("-o");
-        cmd.arg(output.verilog_file(self));
-        if let Some(dialect) = self.verilog_dialect {
+        cmd.arg(output.verilog_file());
+        if *debug {
+            cmd.arg("-g");
+            cmd.arg("--preserve-values=named");
+        }
+        if let Some(dialect) = verilog_dialect {
             cmd.args(dialect.firtool_extra_args());
         }
-        cmd.args(&self.firtool_extra_args);
-        cmd.current_dir(&self.firrtl.base.output);
-        let status = cmd.status()?;
+        cmd.args(firtool_extra_args);
+        cmd.current_dir(&output.firrtl.output_dir);
+        let status = firrtl.base.run_external_command(cmd)?;
         if status.success() {
             Ok(output)
         } else {
@@ -211,12 +302,217 @@ where
     }
 }
 
+#[derive(ValueEnum, Copy, Clone, Debug, PartialEq, Eq, Hash, Default)]
+#[non_exhaustive]
+pub enum FormalMode {
+    #[default]
+    BMC,
+    Prove,
+    Live,
+    Cover,
+}
+
+impl FormalMode {
+    pub fn as_str(self) -> &'static str {
+        match self {
+            FormalMode::BMC => "bmc",
+            FormalMode::Prove => "prove",
+            FormalMode::Live => "live",
+            FormalMode::Cover => "cover",
+        }
+    }
+}
+
+impl fmt::Display for FormalMode {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.write_str(self.as_str())
+    }
+}
+
+#[derive(Clone)]
+struct FormalAdjustArgs;
+
+impl clap::FromArgMatches for FormalAdjustArgs {
+    fn from_arg_matches(_matches: &clap::ArgMatches) -> Result<Self, clap::Error> {
+        Ok(Self)
+    }
+
+    fn update_from_arg_matches(&mut self, _matches: &clap::ArgMatches) -> Result<(), clap::Error> {
+        Ok(())
+    }
+}
+
+impl clap::Args for FormalAdjustArgs {
+    fn augment_args(cmd: clap::Command) -> clap::Command {
+        cmd.mut_arg("output", |arg| arg.required(false))
+            .mut_arg("verilog_dialect", |arg| {
+                arg.default_value(VerilogDialect::Yosys.to_string())
+                    .hide(true)
+            })
+    }
+
+    fn augment_args_for_update(cmd: clap::Command) -> clap::Command {
+        Self::augment_args(cmd)
+    }
+}
+
+#[derive(Parser, Clone)]
+#[non_exhaustive]
+pub struct FormalArgs {
+    #[command(flatten)]
+    pub verilog: VerilogArgs,
+    #[arg(
+        long,
+        default_value = "sby",
+        env = "SBY",
+        value_hint = ValueHint::CommandName,
+        value_parser = OsStringValueParser::new().try_map(which::which)
+    )]
+    pub sby: PathBuf,
+    #[arg(long)]
+    pub sby_extra_args: Vec<OsString>,
+    #[arg(long, default_value_t)]
+    pub mode: FormalMode,
+    #[arg(long, default_value_t = Self::DEFAULT_DEPTH)]
+    pub depth: u64,
+    #[arg(long)]
+    pub solver: Option<String>,
+    #[arg(long)]
+    pub smtbmc_extra_args: Vec<String>,
+    #[command(flatten)]
+    _formal_adjust_args: FormalAdjustArgs,
+}
+
+impl fmt::Debug for FormalArgs {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        let Self {
+            verilog,
+            sby,
+            sby_extra_args,
+            mode,
+            depth,
+            solver,
+            smtbmc_extra_args,
+            _formal_adjust_args: _,
+        } = self;
+        f.debug_struct("FormalArgs")
+            .field("verilog", &verilog)
+            .field("sby", &sby)
+            .field("sby_extra_args", &sby_extra_args)
+            .field("mode", &mode)
+            .field("depth", &depth)
+            .field("solver", &solver)
+            .field("smtbmc_extra_args", &smtbmc_extra_args)
+            .finish_non_exhaustive()
+    }
+}
+
+impl FormalArgs {
+    pub const DEFAULT_DEPTH: u64 = 20;
+}
+
+#[derive(Debug)]
+#[non_exhaustive]
+pub struct FormalOutput {
+    pub verilog: VerilogOutput,
+}
+
+impl FormalOutput {
+    pub fn sby_file(&self) -> PathBuf {
+        self.verilog.firrtl.file_with_ext("sby")
+    }
+}
+
+impl FormalArgs {
+    fn sby_contents(&self, output: &FormalOutput) -> String {
+        let Self {
+            verilog: _,
+            sby: _,
+            sby_extra_args: _,
+            mode,
+            depth,
+            smtbmc_extra_args,
+            solver,
+            _formal_adjust_args: _,
+        } = self;
+        struct OptArg<T>(Option<T>);
+        impl<T: fmt::Display> fmt::Display for OptArg<T> {
+            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+                if let Some(v) = &self.0 {
+                    f.write_str(" ")?;
+                    v.fmt(f)
+                } else {
+                    Ok(())
+                }
+            }
+        }
+        let space_solver = OptArg(solver.as_ref());
+        let smtbmc_options = smtbmc_extra_args.join(" ");
+        let verilog_file = output
+            .verilog
+            .verilog_file()
+            .into_os_string()
+            .into_string()
+            .ok()
+            .expect("verilog file path is not UTF-8");
+        let top_module = &output.verilog.firrtl.top_module;
+        format!(
+            "[options]\n\
+            mode {mode}\n\
+            depth {depth}\n\
+            wait on\n\
+            \n\
+            [engines]\n\
+            smtbmc{space_solver} -- -- {smtbmc_options}\n\
+            \n\
+            [script]\n\
+            read_verilog -sv -formal {verilog_file}\n\
+            prep -top {top_module}\n
+            "
+        )
+    }
+    fn run_impl(&self, verilog_output: VerilogOutput) -> Result<FormalOutput> {
+        let output = FormalOutput {
+            verilog: verilog_output,
+        };
+        let sby_file = output.sby_file();
+        std::fs::write(&sby_file, self.sby_contents(&output))?;
+        let mut cmd = process::Command::new(&self.sby);
+        cmd.arg("-f");
+        cmd.arg(sby_file);
+        cmd.args(&self.sby_extra_args);
+        cmd.current_dir(&output.verilog.firrtl.output_dir);
+        let status = self.verilog.firrtl.base.run_external_command(cmd)?;
+        if status.success() {
+            Ok(output)
+        } else {
+            Err(CliError(eyre!(
+                "running {} failed: {status}",
+                self.sby.display()
+            )))
+        }
+    }
+}
+
+impl<Arg> RunPhase<Arg> for FormalArgs
+where
+    VerilogArgs: RunPhase<Arg, Output = VerilogOutput>,
+{
+    type Output = FormalOutput;
+    fn run(&self, arg: Arg) -> Result<Self::Output> {
+        let verilog_output = self.verilog.run(arg)?;
+        self.run_impl(verilog_output)
+    }
+}
+
 #[derive(Subcommand, Debug)]
 enum CliCommand {
     /// Generate FIRRTL
     Firrtl(FirrtlArgs),
     /// Generate Verilog
     Verilog(VerilogArgs),
+    /// Run a formal proof
+    Formal(FormalArgs),
 }
 
 /// a simple CLI
@@ -302,6 +598,9 @@ where
             CliCommand::Verilog(c) => {
                 c.run(arg)?;
             }
+            CliCommand::Formal(c) => {
+                c.run(arg)?;
+            }
         }
         Ok(())
     }

crates/fayalite/src/firrtl.rs

@@ -18,10 +18,14 @@ use crate::{
     intern::{Intern, Interned},
     memory::{Mem, PortKind, PortName, ReadUnderWrite},
     module::{
-        transform::simplify_memories::simplify_memories, AnnotatedModuleIO, Block,
-        ExternModuleBody, ExternModuleParameter, ExternModuleParameterValue, Module, ModuleBody,
-        NameId, NormalModuleBody, Stmt, StmtConnect, StmtDeclaration, StmtFormal, StmtFormalKind,
-        StmtIf, StmtInstance, StmtMatch, StmtReg, StmtWire,
+        transform::{
+            simplify_enums::{simplify_enums, SimplifyEnumsError, SimplifyEnumsKind},
+            simplify_memories::simplify_memories,
+        },
+        AnnotatedModuleIO, Block, ExternModuleBody, ExternModuleParameter,
+        ExternModuleParameterValue, Module, ModuleBody, NameId, NormalModuleBody, Stmt,
+        StmtConnect, StmtDeclaration, StmtFormal, StmtFormalKind, StmtIf, StmtInstance, StmtMatch,
+        StmtReg, StmtWire,
     },
     reset::{AsyncReset, Reset, SyncReset},
     source_location::SourceLocation,
@@ -32,6 +36,7 @@ use crate::{
     },
 };
 use bitvec::slice::BitSlice;
+use clap::value_parser;
 use hashbrown::{HashMap, HashSet};
 use num_traits::Signed;
 use serde::Serialize;
@@ -476,6 +481,7 @@ trait WrappedFileBackendTrait {
         circuit_name: String,
         contents: String,
     ) -> Result<(), WrappedError>;
+    fn simplify_enums_error(&mut self, error: SimplifyEnumsError) -> WrappedError;
 }
 
 struct WrappedFileBackend<B: FileBackendTrait> {
@@ -533,6 +539,11 @@ impl<B: FileBackendTrait> WrappedFileBackendTrait for WrappedFileBackend<B> {
                 WrappedError
             })
     }
+
+    fn simplify_enums_error(&mut self, error: SimplifyEnumsError) -> WrappedError {
+        self.error = Err(error.into());
+        WrappedError
+    }
 }
 
 #[derive(Clone)]
@@ -2225,7 +2236,7 @@ impl<'a> Exporter<'a> {
 }
 
 pub trait FileBackendTrait {
-    type Error;
+    type Error: From<SimplifyEnumsError>;
     type Path: AsRef<Self::Path> + fmt::Debug + ?Sized;
     type PathBuf: AsRef<Self::Path> + fmt::Debug;
     fn path_to_string(&mut self, path: &Self::Path) -> Result<String, Self::Error>;
@@ -2300,6 +2311,7 @@ impl<T: ?Sized + FileBackendTrait> FileBackendTrait for &'_ mut T {
 #[non_exhaustive]
 pub struct FileBackend {
     pub dir_path: PathBuf,
+    pub circuit_name: Option<String>,
     pub top_fir_file_stem: Option<String>,
 }
 
@@ -2307,6 +2319,7 @@ impl FileBackend {
     pub fn new(dir_path: impl AsRef<Path>) -> Self {
         Self {
             dir_path: dir_path.as_ref().to_owned(),
+            circuit_name: None,
             top_fir_file_stem: None,
         }
     }
@@ -2342,7 +2355,10 @@ impl FileBackendTrait for FileBackend {
         circuit_name: String,
         contents: String,
     ) -> Result<(), Self::Error> {
-        let top_fir_file_stem = self.top_fir_file_stem.get_or_insert(circuit_name);
+        let top_fir_file_stem = self
+            .top_fir_file_stem
+            .get_or_insert_with(|| circuit_name.clone());
+        self.circuit_name = Some(circuit_name);
         let mut path = self.dir_path.join(top_fir_file_stem);
         if let Some(parent) = path.parent().filter(|v| !v.as_os_str().is_empty()) {
             fs::create_dir_all(parent)?;
@@ -2370,6 +2386,7 @@ impl Default for TestBackendPrivate {
 pub struct TestBackend {
     pub files: BTreeMap<String, String>,
     pub error_after: Option<i64>,
+    pub options: ExportOptions,
     #[doc(hidden)]
     /// `#[non_exhaustive]` except allowing struct update syntax
     pub __private: TestBackendPrivate,
@@ -2380,6 +2397,7 @@ impl fmt::Debug for TestBackend {
         let Self {
             files,
             error_after,
+            options,
             __private: TestBackendPrivate { module_var_name },
         } = self;
         writeln!(
@@ -2394,6 +2412,9 @@ impl fmt::Debug for TestBackend {
         if *error_after != Option::default() {
             writeln!(f, "        error_after: {error_after:?},")?;
         }
+        if *options != ExportOptions::default() {
+            writeln!(f, "        options: {options:?},")?;
+        }
         write!(f, "    }};")
     }
 }
@@ -2409,6 +2430,12 @@ impl fmt::Display for TestBackendError {
 
 impl Error for TestBackendError {}
 
+impl From<SimplifyEnumsError> for TestBackendError {
+    fn from(value: SimplifyEnumsError) -> Self {
+        TestBackendError(value.to_string())
+    }
+}
+
 impl TestBackend {
     #[track_caller]
     pub fn step_error_after(&mut self, args: &dyn fmt::Debug) -> Result<(), TestBackendError> {
@@ -2465,9 +2492,20 @@ impl FileBackendTrait for TestBackend {
 
 fn export_impl(
     file_backend: &mut dyn WrappedFileBackendTrait,
-    top_module: Interned<Module<Bundle>>,
+    mut top_module: Interned<Module<Bundle>>,
+    options: ExportOptions,
 ) -> Result<(), WrappedError> {
-    let top_module = simplify_memories(top_module);
+    let ExportOptions {
+        simplify_memories: do_simplify_memories,
+        simplify_enums: do_simplify_enums,
+    } = options;
+    if let Some(kind) = do_simplify_enums {
+        top_module =
+            simplify_enums(top_module, kind).map_err(|e| file_backend.simplify_enums_error(e))?;
+    }
+    if do_simplify_memories {
+        top_module = simplify_memories(top_module);
+    }
     let indent_depth = Cell::new(0);
     let mut global_ns = Namespace::default();
     let circuit_name = global_ns.get(top_module.name_id());
@@ -2488,20 +2526,102 @@ fn export_impl(
     .run(top_module)
 }
 
+#[derive(Clone)]
+struct OptionSimplifyEnumsKindValueParser;
+
+impl OptionSimplifyEnumsKindValueParser {
+    const NONE_NAME: &'static str = "off";
+}
+
+impl clap::builder::TypedValueParser for OptionSimplifyEnumsKindValueParser {
+    type Value = Option<SimplifyEnumsKind>;
+
+    fn parse_ref(
+        &self,
+        cmd: &clap::Command,
+        arg: Option<&clap::Arg>,
+        value: &std::ffi::OsStr,
+    ) -> Result<Self::Value, clap::Error> {
+        if value == Self::NONE_NAME {
+            Ok(None)
+        } else {
+            Ok(Some(
+                value_parser!(SimplifyEnumsKind).parse_ref(cmd, arg, value)?,
+            ))
+        }
+    }
+
+    fn possible_values(
+        &self,
+    ) -> Option<Box<dyn Iterator<Item = clap::builder::PossibleValue> + '_>> {
+        Some(Box::new(
+            [Self::NONE_NAME.into()]
+                .into_iter()
+                .chain(value_parser!(SimplifyEnumsKind).possible_values()?)
+                .collect::<Vec<_>>()
+                .into_iter(),
+        ))
+    }
+}
+
+#[derive(clap::Parser, Copy, Clone, PartialEq, Eq, Hash)]
+#[non_exhaustive]
+pub struct ExportOptions {
+    #[clap(long = "no-simplify-memories", action = clap::ArgAction::SetFalse)]
+    pub simplify_memories: bool,
+    #[clap(long, value_parser = OptionSimplifyEnumsKindValueParser, default_value = OptionSimplifyEnumsKindValueParser::NONE_NAME)]
+    pub simplify_enums: std::option::Option<SimplifyEnumsKind>,
+}
+
+impl fmt::Debug for ExportOptions {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.write_str("ExportOptions {")?;
+        if f.alternate() {
+            f.write_str("\n")?;
+        }
+        let mut sep = if f.alternate() { "\n    " } else { " " };
+        let comma_sep = if f.alternate() { ",\n    " } else { ", " };
+        let default = ExportOptions::default();
+        if self.simplify_memories != default.simplify_memories {
+            write!(f, "{sep}simplify_memories: {:?}", self.simplify_memories)?;
+            sep = comma_sep;
+        }
+        if self.simplify_enums != default.simplify_enums {
+            write!(f, "{sep}simplify_enums: {:?}", self.simplify_enums)?;
+            sep = comma_sep;
+        }
+        write!(
+            f,
+            "{sep}..ExportOptions::default(){}",
+            if f.alternate() { "\n}" } else { " }" }
+        )
+    }
+}
+
+impl Default for ExportOptions {
+    fn default() -> Self {
+        Self {
+            simplify_memories: true,
+            simplify_enums: None,
+        }
+    }
+}
+
 pub fn export<T: BundleType, B: FileBackendTrait>(
     file_backend: B,
     top_module: &Module<T>,
+    options: ExportOptions,
 ) -> Result<B, B::Error> {
     let top_module = Intern::intern_sized(top_module.canonical());
     WrappedFileBackend::with(file_backend, |file_backend| {
-        export_impl(file_backend, top_module)
+        export_impl(file_backend, top_module, options)
     })
 }
 
 #[doc(hidden)]
 #[track_caller]
 pub fn assert_export_firrtl_impl<T: BundleType>(top_module: &Module<T>, expected: TestBackend) {
-    let result = export(TestBackend::default(), top_module).unwrap();
+    let result = export(TestBackend::default(), top_module, expected.options).unwrap();
     if result != expected {
         panic!(
             "assert_export_firrtl failed:\nyou can update the expected output by using:\n-------START-------\n{result:?}\n-------END-------"

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/module/transform/simplify_enums.rs

@@ -41,6 +41,12 @@ impl fmt::Display for SimplifyEnumsError {
 
 impl std::error::Error for SimplifyEnumsError {}
 
+impl From<SimplifyEnumsError> for std::io::Error {
+    fn from(value: SimplifyEnumsError) -> Self {
+        std::io::Error::new(std::io::ErrorKind::Other, value)
+    }
+}
+
 #[hdl]
 struct TagAndBody<T, BodyWidth: Size> {
     tag: T,
@@ -595,10 +601,12 @@ impl Folder for State {
     }
 }
 
-#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
+#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug, clap::ValueEnum)]
 pub enum SimplifyEnumsKind {
     SimplifyToEnumsWithNoBody,
+    #[clap(name = "replace-with-bundle-of-uints")]
     ReplaceWithBundleOfUInts,
+    #[clap(name = "replace-with-uint")]
     ReplaceWithUInt,
 }
 

crates/fayalite/src/testing.rs

@@ -0,0 +1,34 @@
+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");
+}

crates/fayalite/src/util.rs

@@ -6,6 +6,7 @@ mod const_cmp;
 mod const_usize;
 mod misc;
 mod scoped_ref;
+pub(crate) mod streaming_read_utf8;
 
 #[doc(inline)]
 pub use const_bool::{ConstBool, ConstBoolDispatch, ConstBoolDispatchTag, GenericConstBool};

crates/fayalite/src/util/streaming_read_utf8.rs

@@ -0,0 +1,29 @@
+use std::{
+    io::{self, BufRead},
+    str,
+};
+
+pub(crate) fn streaming_read_utf8<R: BufRead, E: From<io::Error>>(
+    reader: R,
+    mut callback: impl FnMut(&str) -> Result<(), E>,
+) -> Result<(), E> {
+    let mut buf = [0; 4];
+    let mut buf_len = 0;
+    for byte in reader.bytes() {
+        buf[buf_len] = byte?;
+        buf_len += 1;
+        match str::from_utf8(&buf[..buf_len]) {
+            Ok(buf) => {
+                callback(buf)?;
+                buf_len = 0;
+            }
+            Err(e) => {
+                if e.error_len().is_some() {
+                    callback("\u{FFFD}")?; // replacement character
+                    buf_len = 0;
+                }
+            }
+        }
+    }
+    Ok(())
+}