add WIP formal proof for queue()

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()
+            },
+        );
+    }
+}