add formal subcommand

Cargo.lock

@@ -252,6 +252,7 @@ dependencies = [
  "os_pipe",
  "serde",
  "serde_json",
+ "tempfile",
  "trybuild",
  "which",
 ]

crates/fayalite/Cargo.toml

@@ -24,6 +24,7 @@ num-traits.workspace = true
 os_pipe.workspace = true
 serde_json.workspace = true
 serde.workspace = true
+tempfile.workspace = true
 which.workspace = true
 
 [dev-dependencies]

crates/fayalite/src/cli.rs

@@ -13,6 +13,7 @@ use clap::{
 };
 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>;
 
@@ -47,21 +48,40 @@ pub trait RunPhase<Arg> {
 #[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(
@@ -106,25 +126,37 @@ pub struct FirrtlArgs {
 #[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, self.export_options)?;
+            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,
         })
     }
 }
@@ -155,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"],
@@ -191,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)]
@@ -200,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 = self.firrtl.base.run_external_command(cmd)?;
+        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 {
@@ -244,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
@@ -335,6 +598,9 @@ where
             CliCommand::Verilog(c) => {
                 c.run(arg)?;
             }
+            CliCommand::Formal(c) => {
+                c.run(arg)?;
+            }
         }
         Ok(())
     }

crates/fayalite/src/firrtl.rs

@@ -2311,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>,
 }
 
@@ -2318,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,
         }
     }
@@ -2353,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)?;