add WIP formal proof for queue()

crates/fayalite/src/lib.rs

@@ -50,4 +50,5 @@ pub mod ty;
 pub mod util;
 //pub mod valueless;
 pub mod prelude;
+pub mod testing;
 pub mod wire;

crates/fayalite/src/testing.rs

@@ -0,0 +1,36 @@
+// SPDX-License-Identifier: LGPL-3.0-or-later
+// See Notices.txt for copyright information
+use crate::{
+    cli::{FormalArgs, FormalMode, FormalOutput, RunPhase},
+    firrtl::ExportOptions,
+};
+use clap::Parser;
+use std::sync::OnceLock;
+
+fn assert_formal_helper() -> FormalArgs {
+    static FORMAL_ARGS: OnceLock<FormalArgs> = OnceLock::new();
+    // ensure we only run parsing once, so errors from env vars don't produce overlapping output if we're called on multiple threads
+    FORMAL_ARGS
+        .get_or_init(|| FormalArgs::parse_from(["fayalite::testing::assert_formal"]))
+        .clone()
+}
+
+#[track_caller]
+pub fn assert_formal<M>(
+    module: M,
+    mode: FormalMode,
+    depth: u64,
+    solver: Option<&str>,
+    export_options: ExportOptions,
+) where
+    FormalArgs: RunPhase<M, Output = FormalOutput>,
+{
+    let mut args = assert_formal_helper();
+    args.verilog.firrtl.base.redirect_output_for_rust_test = true;
+    args.verilog.firrtl.export_options = export_options;
+    args.verilog.debug = true;
+    args.mode = mode;
+    args.depth = depth;
+    args.solver = solver.map(String::from);
+    args.run(module).expect("testing::assert_formal() failed");
+}

crates/fayalite/src/util/ready_valid.rs

@@ -162,3 +162,106 @@ pub fn queue<T: Type>(
         }
     }
 }
+
+#[cfg(todo)]
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::{
+        cli::FormalMode, firrtl::ExportOptions,
+        module::transform::simplify_enums::SimplifyEnumsKind, testing::assert_formal,
+    };
+
+    #[test]
+    fn test_queue() {
+        #[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 cd = wire();
+            connect(
+                cd,
+                #[hdl]
+                ClockDomain {
+                    clk,
+                    rst: rst.to_reset(),
+                },
+            );
+            #[hdl]
+            let dut = instance(queue(
+                UInt[ConstUsize::<8>],
+                capacity,
+                inp_ready_is_comb,
+                out_valid_is_comb,
+            ));
+            connect(dut.cd, cd);
+            connect(dut.inp.data, inp_data);
+            connect(dut.out.ready, out_ready);
+            #[hdl]
+            let count = reg_builder().clock_domain(cd).reset(0u32);
+            #[hdl]
+            let next_count = wire();
+            connect(next_count, count);
+            connect(count, next_count);
+            #[hdl]
+            if ReadyValid::fire(dut.inp) & !ReadyValid::fire(dut.out) {
+                connect_any(next_count, count + 1u8);
+            } 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]
+            let index = reg_builder().clock_domain(cd).reset(HdlNone::<UInt<32>>());
+            #[hdl]
+            let data = reg_builder().clock_domain(cd).reset(HdlNone());
+            #[hdl]
+            match index {
+                HdlNone =>
+                {
+                    #[hdl]
+                    if ReadyValid::fire(dut.inp) {
+                        connect(index, HdlSome(0u32));
+                        connect(data, dut.inp.data);
+                    }
+                }
+                HdlSome(cur_index) =>
+                {
+                    #[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(), "");
+                        }
+                    } else {
+                        connect(index, HdlSome((cur_index + 1u8).cast_to_static()));
+                    }
+                }
+            }
+        }
+        assert_formal(
+            queue_test(NonZeroUsize::new(2).unwrap(), false, false),
+            FormalMode::BMC,
+            20,
+            None,
+            ExportOptions {
+                simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts),
+                ..ExportOptions::default()
+            },
+        );
+    }
+}