From 45dbb554d07e8a0ea05b0e88ae79bc88f616f968 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Wed, 25 Sep 2024 01:52:41 -0700 Subject: [PATCH] add formal subcommand --- Cargo.lock | 1 + crates/fayalite/Cargo.toml | 1 + crates/fayalite/src/cli.rs | 312 +++++++++++++++++++++++++++++++--- crates/fayalite/src/firrtl.rs | 7 +- 4 files changed, 297 insertions(+), 24 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 1c237af..fa6fb6b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -252,6 +252,7 @@ dependencies = [ "os_pipe", "serde", "serde_json", + "tempfile", "trybuild", "which", ] diff --git a/crates/fayalite/Cargo.toml b/crates/fayalite/Cargo.toml index 2306e7a..21089c0 100644 --- a/crates/fayalite/Cargo.toml +++ b/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] diff --git a/crates/fayalite/src/cli.rs b/crates/fayalite/src/cli.rs index c171c22..a771de6 100644 --- a/crates/fayalite/src/cli.rs +++ b/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 = std::result::Result; @@ -47,21 +48,40 @@ pub trait RunPhase { #[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, /// the stem of the generated main output file, e.g. to get foo.v, pass --file-stem=foo #[arg(long)] pub file_stem: Option, + #[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)> { + 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, } 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) -> Result { + 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, + #[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 { + 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 { + 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, + #[arg(long, default_value_t)] + pub mode: FormalMode, + #[arg(long, default_value_t = Self::DEFAULT_DEPTH)] + pub depth: u64, + #[arg(long)] + pub solver: Option, + #[arg(long)] + pub smtbmc_extra_args: Vec, + #[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(Option); + impl fmt::Display for OptArg { + 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 { + 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 RunPhase for FormalArgs +where + VerilogArgs: RunPhase, +{ + type Output = FormalOutput; + fn run(&self, arg: Arg) -> Result { + 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(()) } diff --git a/crates/fayalite/src/firrtl.rs b/crates/fayalite/src/firrtl.rs index ba37bcc..4a1547d 100644 --- a/crates/fayalite/src/firrtl.rs +++ b/crates/fayalite/src/firrtl.rs @@ -2311,6 +2311,7 @@ impl FileBackendTrait for &'_ mut T { #[non_exhaustive] pub struct FileBackend { pub dir_path: PathBuf, + pub circuit_name: Option, pub top_fir_file_stem: Option, } @@ -2318,6 +2319,7 @@ impl FileBackend { pub fn new(dir_path: impl AsRef) -> 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)?;