From 3e2fb9b94f9841fb930ff6ac5940865561d4e567 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Thu, 3 Oct 2024 01:08:01 -0700 Subject: [PATCH] WIP getting queue formal to pass -- passes for capacity <= 2 --- crates/fayalite/src/cli.rs | 89 ++++++++--- crates/fayalite/src/formal.rs | 15 +- crates/fayalite/src/testing.rs | 86 +++++++++- crates/fayalite/src/util/ready_valid.rs | 199 ++++++++++++++++++------ crates/fayalite/tests/module.rs | 31 +++- 5 files changed, 343 insertions(+), 77 deletions(-) diff --git a/crates/fayalite/src/cli.rs b/crates/fayalite/src/cli.rs index a771de6..cbef722 100644 --- a/crates/fayalite/src/cli.rs +++ b/crates/fayalite/src/cli.rs @@ -12,7 +12,14 @@ use clap::{ Parser, Subcommand, ValueEnum, ValueHint, }; use eyre::{eyre, Report}; -use std::{error, ffi::OsString, fmt, io, path::PathBuf, process}; +use std::{ + error, + ffi::OsString, + fmt::{self, Write}, + fs, io, mem, + path::{Path, PathBuf}, + process, +}; use tempfile::TempDir; pub type Result = std::result::Result; @@ -246,15 +253,51 @@ pub struct VerilogArgs { #[non_exhaustive] pub struct VerilogOutput { pub firrtl: FirrtlOutput, + pub verilog_files: Vec, } impl VerilogOutput { - pub fn verilog_file(&self) -> PathBuf { + pub fn main_verilog_file(&self) -> PathBuf { self.firrtl.file_with_ext("v") } + fn unadjusted_verilog_file(&self) -> PathBuf { + self.firrtl.file_with_ext("unadjusted.v") + } } impl VerilogArgs { + fn process_unadjusted_verilog_file(&self, mut output: VerilogOutput) -> Result { + let input = fs::read_to_string(output.unadjusted_verilog_file())?; + let file_separator_prefix = "\n// ----- 8< ----- FILE \""; + let file_separator_suffix = "\" ----- 8< -----\n\n"; + let mut input = &*input; + let main_verilog_file = output.main_verilog_file(); + let mut file_name: Option<&Path> = Some(&main_verilog_file); + loop { + let (chunk, next_file_name) = if let Some((chunk, rest)) = + input.split_once(file_separator_prefix) + { + let Some((next_file_name, rest)) = rest.split_once(file_separator_suffix) else { + return Err(CliError(eyre!("parsing firtool's output failed: found {file_separator_prefix:?} but no {file_separator_suffix:?}"))); + }; + input = rest; + (chunk, Some(next_file_name.as_ref())) + } else { + (mem::take(&mut input), None) + }; + let Some(file_name) = mem::replace(&mut file_name, next_file_name) else { + break; + }; + let file_name = output.firrtl.output_dir.join(file_name); + fs::write(&file_name, chunk)?; + if let Some(extension) = file_name.extension() { + if extension == "v" || extension == "sv" { + output.verilog_files.push(file_name); + } + } + } + Ok(output) + } fn run_impl(&self, firrtl_output: FirrtlOutput) -> Result { let Self { firrtl, @@ -265,14 +308,15 @@ impl VerilogArgs { } = self; let output = VerilogOutput { firrtl: firrtl_output, + verilog_files: vec![], }; let mut cmd = process::Command::new(firtool); cmd.arg(output.firrtl.firrtl_file()); cmd.arg("-o"); - cmd.arg(output.verilog_file()); + cmd.arg(output.unadjusted_verilog_file()); if *debug { cmd.arg("-g"); - cmd.arg("--preserve-values=named"); + cmd.arg("--preserve-values=all"); } if let Some(dialect) = verilog_dialect { cmd.args(dialect.firtool_extra_args()); @@ -281,7 +325,7 @@ impl VerilogArgs { cmd.current_dir(&output.firrtl.output_dir); let status = firrtl.base.run_external_command(cmd)?; if status.success() { - Ok(output) + self.process_unadjusted_verilog_file(output) } else { Err(CliError(eyre!( "running {} failed: {status}", @@ -424,7 +468,7 @@ impl FormalOutput { } impl FormalArgs { - fn sby_contents(&self, output: &FormalOutput) -> String { + fn sby_contents(&self, output: &FormalOutput) -> Result { let Self { verilog: _, sby: _, @@ -448,15 +492,8 @@ impl FormalArgs { } 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!( + let mut retval = format!( "[options]\n\ mode {mode}\n\ depth {depth}\n\ @@ -465,18 +502,30 @@ impl FormalArgs { [engines]\n\ smtbmc{space_solver} -- -- {smtbmc_options}\n\ \n\ - [script]\n\ - read_verilog -sv -formal {verilog_file}\n\ - prep -top {top_module}\n - " - ) + [script]\n" + ); + for verilog_file in &output.verilog.verilog_files { + let verilog_file = verilog_file + .to_str() + .ok_or_else(|| CliError(eyre!("verilog file path is not UTF-8")))?; + if verilog_file.contains(|ch: char| { + (ch != ' ' && ch != '\t' && ch.is_ascii_whitespace()) || ch == '"' + }) { + return Err(CliError(eyre!( + "verilog file path contains characters that aren't permitted" + ))); + } + writeln!(retval, "read_verilog -sv -formal \"{verilog_file}\"").unwrap(); + } + writeln!(retval, "prep -top {top_module}").unwrap(); + Ok(retval) } 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))?; + std::fs::write(&sby_file, self.sby_contents(&output)?)?; let mut cmd = process::Command::new(&self.sby); cmd.arg("-f"); cmd.arg(sby_file); diff --git a/crates/fayalite/src/formal.rs b/crates/fayalite/src/formal.rs index 5e90b59..eab1969 100644 --- a/crates/fayalite/src/formal.rs +++ b/crates/fayalite/src/formal.rs @@ -1,6 +1,10 @@ // SPDX-License-Identifier: LGPL-3.0-or-later // See Notices.txt for copyright information -use crate::{intern::Intern, prelude::*}; +use crate::{ + intern::{Intern, Interned}, + prelude::*, +}; +use std::sync::OnceLock; #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)] pub enum FormalKind { @@ -32,7 +36,7 @@ pub fn formal_stmt_with_enable_and_loc( kind, clk, pred, - en, + en: en & !formal_reset().cast_to_static::(), text: text.intern(), source_location, }); @@ -160,11 +164,11 @@ endmodule } #[hdl] -pub fn formal_reset() -> Expr { +pub fn formal_reset() -> Expr { #[hdl_module(extern)] fn formal_reset() { #[hdl] - let rst: AsyncReset = m.output(); + let rst: SyncReset = m.output(); m.annotate_module(BlackBoxInlineAnnotation { path: "fayalite_formal_reset.v".intern(), text: r"module __fayalite_formal_reset(output rst); @@ -180,7 +184,8 @@ endmodule }); m.verilog_name("__fayalite_formal_reset"); } + static MOD: OnceLock>> = OnceLock::new(); #[hdl] - let formal_reset = instance(formal_reset()); + let formal_reset = instance(*MOD.get_or_init(formal_reset)); formal_reset.rst } diff --git a/crates/fayalite/src/testing.rs b/crates/fayalite/src/testing.rs index 8046f05..a647f47 100644 --- a/crates/fayalite/src/testing.rs +++ b/crates/fayalite/src/testing.rs @@ -5,7 +5,14 @@ use crate::{ firrtl::ExportOptions, }; use clap::Parser; -use std::sync::OnceLock; +use hashbrown::HashMap; +use serde::Deserialize; +use std::{ + fmt::Write, + path::{Path, PathBuf}, + process::Command, + sync::{Mutex, OnceLock}, +}; fn assert_formal_helper() -> FormalArgs { static FORMAL_ARGS: OnceLock = OnceLock::new(); @@ -15,8 +22,84 @@ fn assert_formal_helper() -> FormalArgs { .clone() } +#[derive(Deserialize)] +struct CargoMetadata { + target_directory: String, +} + +fn get_cargo_target_dir() -> &'static Path { + static RETVAL: OnceLock = OnceLock::new(); + RETVAL.get_or_init(|| { + let output = Command::new( + std::env::var_os("CARGO") + .as_deref() + .unwrap_or("cargo".as_ref()), + ) + .arg("metadata") + .output() + .expect("can't run `cargo metadata`"); + if !output.status.success() { + panic!( + "can't run `cargo metadata`:\n{}\nexited with status: {}", + String::from_utf8_lossy(&output.stderr), + output.status + ); + } + let CargoMetadata { target_directory } = + serde_json::from_slice(&output.stdout).expect("can't parse output of `cargo metadata`"); + PathBuf::from(target_directory) + }) +} + +#[track_caller] +fn get_assert_formal_target_path(test_name: &dyn std::fmt::Display) -> PathBuf { + static DIRS: Mutex>> = Mutex::new(None); + let test_name = test_name.to_string(); + // don't use line/column numbers since that constantly changes as you edit tests + let file = std::panic::Location::caller().file(); + // simple reproducible hash + let simple_hash = file.bytes().chain(test_name.bytes()).fold( + ((file.len() as u32) << 16).wrapping_add(test_name.len() as u32), + |mut h, b| { + h = h.wrapping_mul(0xaa0d184b); + h ^= h.rotate_right(5); + h ^= h.rotate_right(13); + h.wrapping_add(b as u32) + }, + ); + let mut dir = String::with_capacity(64); + write!(dir, "{simple_hash:08x}-").unwrap(); + for ch in Path::new(file) + .file_stem() + .unwrap_or_default() + .to_str() + .unwrap() + .chars() + .chain(['-']) + .chain(test_name.chars()) + { + dir.push(match ch { + ch if ch.is_alphanumeric() => ch, + '_' | '-' | '+' | '.' | ',' | ' ' => ch, + _ => '_', + }); + } + let index = *DIRS + .lock() + .unwrap() + .get_or_insert_with(HashMap::new) + .entry_ref(&dir) + .and_modify(|v| *v += 1) + .or_insert(0); + write!(dir, ".{index}").unwrap(); + get_cargo_target_dir() + .join("fayalite_assert_formal") + .join(dir) +} + #[track_caller] pub fn assert_formal( + test_name: impl std::fmt::Display, module: M, mode: FormalMode, depth: u64, @@ -27,6 +110,7 @@ pub fn assert_formal( { let mut args = assert_formal_helper(); args.verilog.firrtl.base.redirect_output_for_rust_test = true; + args.verilog.firrtl.base.output = Some(get_assert_formal_target_path(&test_name)); args.verilog.firrtl.export_options = export_options; args.verilog.debug = true; args.mode = mode; diff --git a/crates/fayalite/src/util/ready_valid.rs b/crates/fayalite/src/util/ready_valid.rs index ab19cd1..41299a6 100644 --- a/crates/fayalite/src/util/ready_valid.rs +++ b/crates/fayalite/src/util/ready_valid.rs @@ -23,6 +23,19 @@ impl ReadyValid { fire } #[hdl] + pub fn fire_data(expr: impl ToExpr) -> Expr> { + let expr = expr.to_expr(); + let option_ty = Expr::ty(expr).data; + #[hdl] + let fire_data = wire(option_ty); + connect(fire_data, option_ty.HdlNone()); + #[hdl] + if expr.ready { + connect(fire_data, expr.data); + } + fire_data + } + #[hdl] pub fn map( expr: Expr, f: impl FnOnce(Expr) -> Expr, @@ -163,7 +176,6 @@ pub fn queue( } } -#[cfg(todo)] #[cfg(test)] mod tests { use super::*; @@ -171,27 +183,39 @@ mod tests { cli::FormalMode, firrtl::ExportOptions, module::transform::simplify_enums::SimplifyEnumsKind, testing::assert_formal, }; + use std::num::NonZero; - #[test] - fn test_queue() { + #[track_caller] + fn test_queue(capacity: NonZeroUsize, inp_ready_is_comb: bool, out_valid_is_comb: bool) { + assert_formal( + format_args!("test_queue_{capacity}_{inp_ready_is_comb}_{out_valid_is_comb}"), + queue_test(capacity, inp_ready_is_comb, out_valid_is_comb), + FormalMode::BMC, + 20, + None, + ExportOptions { + simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts), + ..ExportOptions::default() + }, + ); #[hdl_module] fn queue_test(capacity: NonZeroUsize, inp_ready_is_comb: bool, out_valid_is_comb: bool) { - #[hdl] - let clk: Clock = m.input(); - #[hdl] - let rst: SyncReset = m.input(); #[hdl] let inp_data: HdlOption> = m.input(); #[hdl] let out_ready: Bool = m.input(); #[hdl] + let start_check: Bool = m.input(); + #[hdl] + let clk: Clock = m.input(); + #[hdl] let cd = wire(); connect( cd, #[hdl] ClockDomain { clk, - rst: rst.to_reset(), + rst: formal_reset().to_reset(), }, ); #[hdl] @@ -216,52 +240,139 @@ mod tests { } else if !ReadyValid::fire(dut.inp) & ReadyValid::fire(dut.out) { connect_any(next_count, count - 1u8); } - hdl_assert(clk, count.cmp_eq(dut.count), ""); + hdl_assert(cd.clk, count.cmp_eq(dut.count), ""); #[hdl] - let index = reg_builder().clock_domain(cd).reset(HdlNone::>()); + let started_check = reg_builder().clock_domain(cd).reset(false); #[hdl] - let data = reg_builder().clock_domain(cd).reset(HdlNone()); + let steps_till_output = reg_builder().clock_domain(cd).reset(0u32); #[hdl] - match index { - HdlNone => - { - #[hdl] - if ReadyValid::fire(dut.inp) { - connect(index, HdlSome(0u32)); - connect(data, dut.inp.data); - } + let expected_output = reg_builder().clock_domain(cd).reset(HdlNone()); + #[hdl] + if start_check & !started_check { + #[hdl] + if let HdlSome(inp) = ReadyValid::fire_data(dut.inp) { + connect(started_check, true); + connect_any( + steps_till_output, + count + (!ReadyValid::fire(dut.out)).cast_to(UInt[1]), + ); + connect(expected_output, HdlSome(inp)); } - HdlSome(cur_index) => + } else if started_check & steps_till_output.cmp_ne(0u32) & ReadyValid::fire(dut.out) { + connect_any(steps_till_output, steps_till_output - 1u32); + } + #[hdl] + let stored_output = reg_builder().clock_domain(cd).reset(HdlNone()); + #[hdl] + if let HdlSome(out) = ReadyValid::fire_data(dut.out) { + #[hdl] + if (start_check & !started_check) | (started_check & steps_till_output.cmp_ne(0u32)) { + connect(stored_output, HdlSome(out)); + } + } + #[hdl] + if started_check & steps_till_output.cmp_eq(0u32) { + #[hdl] + if let HdlSome(expected_output) = expected_output { #[hdl] - if cur_index.cmp_ge(next_count) { - connect(index, HdlNone()); - #[hdl] - if let HdlSome(data) = data { - #[hdl] - if let HdlSome(out_data) = dut.out.data { - hdl_assert(clk, data.cmp_eq(out_data), ""); - } else { - hdl_assert(clk, false.to_expr(), ""); - } - } else { - hdl_assert(clk, false.to_expr(), ""); - } + if let HdlSome(stored_output) = stored_output { + hdl_assert(cd.clk, stored_output.cmp_eq(expected_output), ""); } else { - connect(index, HdlSome((cur_index + 1u8).cast_to_static())); + hdl_assert(cd.clk, false.to_expr(), ""); } + } else { + hdl_assert(cd.clk, false.to_expr(), ""); } } } - assert_formal( - queue_test(NonZeroUsize::new(2).unwrap(), false, false), - FormalMode::BMC, - 20, - None, - ExportOptions { - simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts), - ..ExportOptions::default() - }, - ); + } + + #[test] + fn test_1_false_false() { + test_queue(NonZero::new(1).unwrap(), false, false); + } + + #[test] + fn test_1_false_true() { + test_queue(NonZero::new(1).unwrap(), false, true); + } + + #[test] + fn test_1_true_false() { + test_queue(NonZero::new(1).unwrap(), true, false); + } + + #[test] + fn test_1_true_true() { + test_queue(NonZero::new(1).unwrap(), true, true); + } + + #[test] + fn test_2_false_false() { + test_queue(NonZero::new(2).unwrap(), false, false); + } + + #[test] + fn test_2_false_true() { + test_queue(NonZero::new(2).unwrap(), false, true); + } + + #[test] + fn test_2_true_false() { + test_queue(NonZero::new(2).unwrap(), true, false); + } + + #[test] + fn test_2_true_true() { + test_queue(NonZero::new(2).unwrap(), true, true); + } + + #[cfg(todo)] + #[test] + fn test_3_false_false() { + test_queue(NonZero::new(3).unwrap(), false, false); + } + + #[cfg(todo)] + #[test] + fn test_3_false_true() { + test_queue(NonZero::new(3).unwrap(), false, true); + } + + #[cfg(todo)] + #[test] + fn test_3_true_false() { + test_queue(NonZero::new(3).unwrap(), true, false); + } + + #[cfg(todo)] + #[test] + fn test_3_true_true() { + test_queue(NonZero::new(3).unwrap(), true, true); + } + + #[cfg(todo)] + #[test] + fn test_4_false_false() { + test_queue(NonZero::new(4).unwrap(), false, false); + } + + #[cfg(todo)] + #[test] + fn test_4_false_true() { + test_queue(NonZero::new(4).unwrap(), false, true); + } + + #[cfg(todo)] + #[test] + fn test_4_true_false() { + test_queue(NonZero::new(4).unwrap(), true, false); + } + + #[cfg(todo)] + #[test] + fn test_4_true_true() { + test_queue(NonZero::new(4).unwrap(), true, true); } } diff --git a/crates/fayalite/tests/module.rs b/crates/fayalite/tests/module.rs index 856cbf0..7d12739 100644 --- a/crates/fayalite/tests/module.rs +++ b/crates/fayalite/tests/module.rs @@ -3390,7 +3390,15 @@ fn test_formal() { assert_export_firrtl! { m => "/test/check_formal.fir": r#"FIRRTL version 3.2.0 -circuit check_formal: +circuit check_formal: %[[ + { + "class": "firrtl.transforms.BlackBoxInlineAnno", + "name": "fayalite_formal_reset.v", + "text": "module __fayalite_formal_reset(output rst);\n reg rst;\n (* gclk *)\n reg gclk;\n initial rst = 1;\n always @(posedge gclk)\n rst <= 0;\nendmodule\n", + "target": "~check_formal|formal_reset" + } +]] + type Ty0 = {rst: UInt<1>} module check_formal: @[module-XXXXXXXXXX.rs 1:1] input clk: Clock @[module-XXXXXXXXXX.rs 2:1] input en1: UInt<1> @[module-XXXXXXXXXX.rs 3:1] @@ -3399,12 +3407,21 @@ circuit check_formal: input pred1: UInt<1> @[module-XXXXXXXXXX.rs 6:1] input pred2: UInt<1> @[module-XXXXXXXXXX.rs 7:1] input pred3: UInt<1> @[module-XXXXXXXXXX.rs 8:1] - assert(clk, pred1, en1, "en check 1") @[module-XXXXXXXXXX.rs 9:1] - assume(clk, pred2, en2, "en check 2") @[module-XXXXXXXXXX.rs 10:1] - cover(clk, pred3, en3, "en check 3") @[module-XXXXXXXXXX.rs 11:1] - assert(clk, pred1, UInt<1>(0h1), "check 1") @[module-XXXXXXXXXX.rs 12:1] - assume(clk, pred2, UInt<1>(0h1), "check 2") @[module-XXXXXXXXXX.rs 13:1] - cover(clk, pred3, UInt<1>(0h1), "check 3") @[module-XXXXXXXXXX.rs 14:1] + inst formal_reset of formal_reset @[formal.rs 189:24] + assert(clk, pred1, and(en1, not(formal_reset.rst)), "en check 1") @[module-XXXXXXXXXX.rs 9:1] + inst formal_reset_1 of formal_reset @[formal.rs 189:24] + assume(clk, pred2, and(en2, not(formal_reset_1.rst)), "en check 2") @[module-XXXXXXXXXX.rs 10:1] + inst formal_reset_2 of formal_reset @[formal.rs 189:24] + cover(clk, pred3, and(en3, not(formal_reset_2.rst)), "en check 3") @[module-XXXXXXXXXX.rs 11:1] + inst formal_reset_3 of formal_reset @[formal.rs 189:24] + assert(clk, pred1, and(UInt<1>(0h1), not(formal_reset_3.rst)), "check 1") @[module-XXXXXXXXXX.rs 12:1] + inst formal_reset_4 of formal_reset @[formal.rs 189:24] + assume(clk, pred2, and(UInt<1>(0h1), not(formal_reset_4.rst)), "check 2") @[module-XXXXXXXXXX.rs 13:1] + inst formal_reset_5 of formal_reset @[formal.rs 189:24] + cover(clk, pred3, and(UInt<1>(0h1), not(formal_reset_5.rst)), "check 3") @[module-XXXXXXXXXX.rs 14:1] + extmodule formal_reset: @[formal.rs 168:5] + output rst: UInt<1> @[formal.rs 171:32] + defname = __fayalite_formal_reset "#, }; }