WIP getting queue formal to pass -- passes for capacity <= 2

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<T = (), E = CliError> = std::result::Result<T, E>;
@@ -246,15 +253,51 @@ pub struct VerilogArgs {
 #[non_exhaustive]
 pub struct VerilogOutput {
     pub firrtl: FirrtlOutput,
+    pub verilog_files: Vec<PathBuf>,
 }
 
 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<VerilogOutput> {
+        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<VerilogOutput> {
         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<String> {
         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<FormalOutput> {
         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);

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::<Bool>(),
         text: text.intern(),
         source_location,
     });
@@ -160,11 +164,11 @@ endmodule
 }
 
 #[hdl]
-pub fn formal_reset() -> Expr<AsyncReset> {
+pub fn formal_reset() -> Expr<SyncReset> {
     #[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<Interned<Module<formal_reset>>> = OnceLock::new();
     #[hdl]
-    let formal_reset = instance(formal_reset());
+    let formal_reset = instance(*MOD.get_or_init(formal_reset));
     formal_reset.rst
 }

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<FormalArgs> = 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<PathBuf> = 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<Option<HashMap<String, u64>>> = 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<M>(
+    test_name: impl std::fmt::Display,
     module: M,
     mode: FormalMode,
     depth: u64,
@@ -27,6 +110,7 @@ pub fn assert_formal<M>(
 {
     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;

crates/fayalite/src/util/ready_valid.rs

@@ -23,6 +23,19 @@ impl<T: Type> ReadyValid<T> {
         fire
     }
     #[hdl]
+    pub fn fire_data(expr: impl ToExpr<Type = Self>) -> Expr<HdlOption<T>> {
+        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<R: Type>(
         expr: Expr<Self>,
         f: impl FnOnce(Expr<T>) -> Expr<R>,
@@ -163,7 +176,6 @@ pub fn queue<T: Type>(
     }
 }
 
-#[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<UInt<8>> = 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::<UInt<32>>());
+            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);
     }
 }

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
 "#,
     };
 }