libre-chip/fayalite
3
0
Fork 0
Code Issues Pull requests Actions Packages Projects Releases Wiki Activity

switch default solver to z3

Browse source
This commit is contained in:
Jacob Lifshay 2024-10-03 01:43:46 -07:00
parent 3e2fb9b94f
commit 4084a70485
Signed by: programmerjake
SSH key fingerprint: SHA256:B1iRVvUJkvd7upMIiMqn6OyxvD2SgJkAH3ZnUOj6z+c
2 changed files with 6 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
crates/fayalite/src/cli.rs
View file

@ -419,8 +419,8 @@ pub struct FormalArgs {
pub mode: FormalMode, pub mode: FormalMode,
#[arg(long, default_value_t = Self::DEFAULT_DEPTH)] #[arg(long, default_value_t = Self::DEFAULT_DEPTH)]
pub depth: u64, pub depth: u64,
#[arg(long)] #[arg(long, default_value = "z3")]
pub solver: Option<String>, pub solver: String,
#[arg(long)] #[arg(long)]
pub smtbmc_extra_args: Vec<String>, pub smtbmc_extra_args: Vec<String>,
#[command(flatten)] #[command(flatten)]
@ -479,18 +479,6 @@ impl FormalArgs {
solver, solver,
_formal_adjust_args: _, _formal_adjust_args: _,
} = self; } = 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 smtbmc_options = smtbmc_extra_args.join(" ");
let top_module = &output.verilog.firrtl.top_module; let top_module = &output.verilog.firrtl.top_module;
let mut retval = format!( let mut retval = format!(
@ -500,7 +488,7 @@ impl FormalArgs {
wait on\n\ wait on\n\
\n\ \n\
[engines]\n\ [engines]\n\
smtbmc{space_solver} -- -- {smtbmc_options}\n\ smtbmc {solver} -- -- {smtbmc_options}\n\
\n\ \n\
[script]\n" [script]\n"
); );

4
crates/fayalite/src/testing.rs
View file

@ -115,6 +115,8 @@ pub fn assert_formal<M>(
args.verilog.debug = true; args.verilog.debug = true;
args.mode = mode; args.mode = mode;
args.depth = depth; args.depth = depth;
args.solver = solver.map(String::from); if let Some(solver) = solver {
args.solver = solver.into();
}
args.run(module).expect("testing::assert_formal() failed"); args.run(module).expect("testing::assert_formal() failed");
} }