queue formal proof passes!

crates/fayalite/src/cli.rs

@@ -516,7 +516,7 @@ impl FormalArgs {
         std::fs::write(&sby_file, self.sby_contents(&output)?)?;
         let mut cmd = process::Command::new(&self.sby);
         cmd.arg("-f");
-        cmd.arg(sby_file);
+        cmd.arg(sby_file.file_name().unwrap());
         cmd.args(&self.sby_extra_args);
         cmd.current_dir(&output.verilog.firrtl.output_dir);
         let status = self.verilog.firrtl.base.run_external_command(cmd)?;

crates/fayalite/src/formal.rs

@@ -1,7 +1,8 @@
 // SPDX-License-Identifier: LGPL-3.0-or-later
 // See Notices.txt for copyright information
 use crate::{
-    intern::{Intern, Interned},
+    int::BoolOrIntType,
+    intern::{Intern, Interned, Memoize},
     prelude::*,
 };
 use std::sync::OnceLock;
@@ -172,12 +173,7 @@ pub fn formal_reset() -> Expr<SyncReset> {
         m.annotate_module(BlackBoxInlineAnnotation {
             path: "fayalite_formal_reset.v".intern(),
             text: r"module __fayalite_formal_reset(output rst);
-    reg rst;
-    (* gclk *)
-    reg gclk;
-    initial rst = 1;
-    always @(posedge gclk)
-        rst <= 0;
+    assign rst = $initstate;
 endmodule
 "
             .intern(),
@@ -189,3 +185,63 @@ endmodule
     let formal_reset = instance(*MOD.get_or_init(formal_reset));
     formal_reset.rst
 }
+
+macro_rules! make_any_const_fn {
+    ($ident:ident, $verilog_attribute:literal) => {
+        #[hdl]
+        pub fn $ident<T: BoolOrIntType>(ty: T) -> Expr<T> {
+            #[hdl_module(extern)]
+            pub(super) fn $ident<T: BoolOrIntType>(ty: T) {
+                #[hdl]
+                let out: T = m.output(ty);
+                let width = ty.width();
+                let verilog_bitslice = if width == 1 {
+                    String::new()
+                } else {
+                    format!(" [{}:0]", width - 1)
+                };
+                m.annotate_module(BlackBoxInlineAnnotation {
+                    path: Intern::intern_owned(format!(
+                        "fayalite_{}_{width}.v",
+                        stringify!($ident),
+                    )),
+                    text: Intern::intern_owned(format!(
+                        r"module __fayalite_{}_{width}(output{verilog_bitslice} out);
+    (* {} *)
+    reg{verilog_bitslice} out;
+endmodule
+",
+                        stringify!($ident),
+                        $verilog_attribute,
+                    )),
+                });
+                m.verilog_name(format!("__fayalite_{}_{width}", stringify!($ident)));
+            }
+            #[derive(Copy, Clone, PartialEq, Eq, Hash)]
+            struct TheMemoize<T>(T);
+            impl<T: BoolOrIntType> Memoize for TheMemoize<T> {
+                type Input = ();
+                type InputOwned = ();
+                type Output = Option<Interned<Module<$ident<T>>>>;
+                fn inner(self, _input: &Self::Input) -> Self::Output {
+                    if self.0.width() == 0 {
+                        None
+                    } else {
+                        Some($ident(self.0))
+                    }
+                }
+            }
+            let Some(module) = TheMemoize(ty).get_owned(()) else {
+                return 0_hdl_u0.cast_bits_to(ty);
+            };
+            #[hdl]
+            let $ident = instance(module);
+            $ident.out
+        }
+    };
+}
+
+make_any_const_fn!(any_const, "anyconst");
+make_any_const_fn!(any_seq, "anyseq");
+make_any_const_fn!(all_const, "allconst");
+make_any_const_fn!(all_seq, "allseq");

crates/fayalite/src/prelude.rs

@@ -14,8 +14,9 @@ pub use crate::{
         ReduceBits, ToExpr,
     },
     formal::{
-        formal_global_clock, formal_reset, hdl_assert, hdl_assert_with_enable, hdl_assume,
-        hdl_assume_with_enable, hdl_cover, hdl_cover_with_enable, MakeFormalExpr,
+        all_const, all_seq, any_const, any_seq, formal_global_clock, formal_reset, hdl_assert,
+        hdl_assert_with_enable, hdl_assume, hdl_assume_with_enable, hdl_cover,
+        hdl_cover_with_enable, MakeFormalExpr,
     },
     hdl, hdl_module,
     int::{Bool, DynSize, KnownSize, SInt, SIntType, Size, UInt, UIntType},

crates/fayalite/src/testing.rs

@@ -68,7 +68,6 @@ fn get_assert_formal_target_path(test_name: &dyn std::fmt::Display) -> PathBuf {
         },
     );
     let mut dir = String::with_capacity(64);
-    write!(dir, "{simple_hash:08x}-").unwrap();
     for ch in Path::new(file)
         .file_stem()
         .unwrap_or_default()
@@ -84,6 +83,7 @@ fn get_assert_formal_target_path(test_name: &dyn std::fmt::Display) -> PathBuf {
             _ => '_',
         });
     }
+    write!(dir, "-{simple_hash:08x}").unwrap();
     let index = *DIRS
         .lock()
         .unwrap()
@@ -91,7 +91,7 @@ fn get_assert_formal_target_path(test_name: &dyn std::fmt::Display) -> PathBuf {
         .entry_ref(&dir)
         .and_modify(|v| *v += 1)
         .or_insert(0);
-    write!(dir, ".{index}").unwrap();
+    write!(dir, "-{index}").unwrap();
     get_cargo_target_dir()
         .join("fayalite_assert_formal")
         .join(dir)

crates/fayalite/src/util/ready_valid.rs

@@ -49,7 +49,6 @@ impl<T: Type> ReadyValid<T> {
     }
 }
 
-// TODO: needs testing
 #[hdl_module]
 pub fn queue<T: Type>(
     ty: T,
@@ -134,7 +133,7 @@ pub fn queue<T: Type>(
     #[hdl]
     if inp_fire {
         #[hdl]
-        if inp_index.cmp_eq(capacity) {
+        if inp_index.cmp_eq(capacity.get() - 1) {
             connect_any(inp_index, 0_hdl_u0);
         } else {
             connect_any(inp_index, inp_index + 1_hdl_u1);
@@ -144,7 +143,7 @@ pub fn queue<T: Type>(
     #[hdl]
     if out_fire {
         #[hdl]
-        if out_index.cmp_eq(capacity) {
+        if out_index.cmp_eq(capacity.get() - 1) {
             connect_any(out_index, 0_hdl_u0);
         } else {
             connect_any(out_index, out_index + 1_hdl_u1);
@@ -153,10 +152,12 @@ pub fn queue<T: Type>(
 
     #[hdl]
     if indexes_equal {
-        connect(
-            count,
-            maybe_full.cast_to_static::<UInt<1>>() << (count_ty.width() - 1),
-        );
+        #[hdl]
+        if maybe_full {
+            connect_any(count, capacity);
+        } else {
+            connect_any(count, 0_hdl_u0);
+        }
     } else {
         if capacity.is_power_of_two() {
             debug_assert_eq!(count_ty.width(), index_ty.width() + 1);
@@ -182,6 +183,7 @@ mod tests {
     use crate::{
         cli::FormalMode, firrtl::ExportOptions,
         module::transform::simplify_enums::SimplifyEnumsKind, testing::assert_formal,
+        ty::StaticType,
     };
     use std::num::NonZero;
 
@@ -190,8 +192,8 @@ mod tests {
         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,
+            FormalMode::Prove,
+            14,
             None,
             ExportOptions {
                 simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts),
@@ -200,12 +202,6 @@ mod tests {
         );
         #[hdl_module]
         fn queue_test(capacity: NonZeroUsize, inp_ready_is_comb: bool, out_valid_is_comb: bool) {
-            #[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]
@@ -219,6 +215,24 @@ mod tests {
                 },
             );
             #[hdl]
+            let inp_data: HdlOption<UInt<8>> = wire();
+            #[hdl]
+            if any_seq(Bool) {
+                connect(inp_data, HdlSome(any_seq(UInt::<8>::TYPE)));
+            } else {
+                connect(inp_data, HdlNone());
+            }
+            #[hdl]
+            let out_ready: Bool = wire();
+            connect(out_ready, any_seq(Bool));
+            let index_ty: UInt<32> = UInt::TYPE;
+            #[hdl]
+            let index_to_check = wire();
+            connect(index_to_check, any_const(index_ty));
+            let index_max = !index_ty.zero();
+            // we saturate at index_max, so only check indexes where we properly maintain position
+            hdl_assume(clk, index_to_check.cmp_ne(index_max), "");
+            #[hdl]
             let dut = instance(queue(
                 UInt[ConstUsize::<8>],
                 capacity,
@@ -228,62 +242,96 @@ mod tests {
             connect(dut.cd, cd);
             connect(dut.inp.data, inp_data);
             connect(dut.out.ready, out_ready);
+            hdl_assume(
+                clk,
+                index_to_check.cmp_ne(!Expr::ty(index_to_check).zero()),
+                "",
+            );
+
             #[hdl]
-            let count = reg_builder().clock_domain(cd).reset(0u32);
+            let expected_count = reg_builder().clock_domain(cd).reset(0u32);
             #[hdl]
-            let next_count = wire();
-            connect(next_count, count);
-            connect(count, next_count);
+            let next_expected_count = wire();
+            connect(next_expected_count, expected_count);
+            connect(expected_count, next_expected_count);
             #[hdl]
             if ReadyValid::fire(dut.inp) & !ReadyValid::fire(dut.out) {
-                connect_any(next_count, count + 1u8);
+                connect_any(next_expected_count, expected_count + 1u8);
             } else if !ReadyValid::fire(dut.inp) & ReadyValid::fire(dut.out) {
-                connect_any(next_count, count - 1u8);
+                connect_any(next_expected_count, expected_count - 1u8);
             }
-            hdl_assert(cd.clk, count.cmp_eq(dut.count), "");
+            hdl_assert(cd.clk, expected_count.cmp_eq(dut.count), "");
+
             #[hdl]
-            let started_check = reg_builder().clock_domain(cd).reset(false);
-            #[hdl]
-            let steps_till_output = reg_builder().clock_domain(cd).reset(0u32);
-            #[hdl]
-            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);
+            let prev_out_ready = reg_builder().clock_domain(cd).reset(!0_hdl_u3);
             connect_any(
-                        steps_till_output,
-                        count + (!ReadyValid::fire(dut.out)).cast_to(UInt[1]),
+                prev_out_ready,
+                (prev_out_ready << 1) | out_ready.cast_to(UInt[1]),
             );
-                    connect(expected_output, HdlSome(inp));
-                }
-            } 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());
+            let prev_inp_valid = reg_builder().clock_domain(cd).reset(!0_hdl_u3);
+            connect_any(
+                prev_inp_valid,
+                (prev_inp_valid << 1) | HdlOption::is_some(inp_data).cast_to(UInt[1]),
+            );
+            hdl_assume(clk, (prev_out_ready & prev_inp_valid).cmp_ne(0u8), "");
+
             #[hdl]
-            if let HdlSome(out) = ReadyValid::fire_data(dut.out) {
+            let inp_index = reg_builder().clock_domain(cd).reset(index_ty.zero());
             #[hdl]
-                if (start_check & !started_check) | (started_check & steps_till_output.cmp_ne(0u32))
-                {
-                    connect(stored_output, HdlSome(out));
+            let stored_inp_data = reg_builder().clock_domain(cd).reset(0u8);
+
+            #[hdl]
+            if let HdlSome(data) = ReadyValid::fire_data(dut.inp) {
+                #[hdl]
+                if inp_index.cmp_lt(index_max) {
+                    connect_any(inp_index, inp_index + 1u8);
+                    #[hdl]
+                    if inp_index.cmp_eq(index_to_check) {
+                        connect(stored_inp_data, data);
                     }
                 }
+            }
+
             #[hdl]
-            if started_check & steps_till_output.cmp_eq(0u32) {
+            if inp_index.cmp_lt(index_to_check) {
+                hdl_assert(clk, stored_inp_data.cmp_eq(0u8), "");
+            }
+
             #[hdl]
-                if let HdlSome(expected_output) = expected_output {
+            let out_index = reg_builder().clock_domain(cd).reset(index_ty.zero());
             #[hdl]
-                    if let HdlSome(stored_output) = stored_output {
-                        hdl_assert(cd.clk, stored_output.cmp_eq(expected_output), "");
+            let stored_out_data = reg_builder().clock_domain(cd).reset(0u8);
+
+            #[hdl]
+            if let HdlSome(data) = ReadyValid::fire_data(dut.out) {
+                #[hdl]
+                if out_index.cmp_lt(index_max) {
+                    connect_any(out_index, out_index + 1u8);
+                    #[hdl]
+                    if out_index.cmp_eq(index_to_check) {
+                        connect(stored_out_data, data);
+                    }
+                }
+            }
+
+            #[hdl]
+            if out_index.cmp_lt(index_to_check) {
+                hdl_assert(clk, stored_out_data.cmp_eq(0u8), "");
+            }
+
+            hdl_assert(clk, inp_index.cmp_ge(out_index), "");
+
+            #[hdl]
+            if inp_index.cmp_lt(index_max) & out_index.cmp_lt(index_max) {
+                hdl_assert(clk, expected_count.cmp_eq(inp_index - out_index), "");
             } else {
-                        hdl_assert(cd.clk, false.to_expr(), "");
-                    }
-                } else {
-                    hdl_assert(cd.clk, false.to_expr(), "");
+                hdl_assert(clk, expected_count.cmp_ge(inp_index - out_index), "");
             }
+
+            #[hdl]
+            if inp_index.cmp_gt(index_to_check) & out_index.cmp_gt(index_to_check) {
+                hdl_assert(clk, stored_inp_data.cmp_eq(stored_out_data), "");
             }
         }
     }
@@ -328,49 +376,41 @@ mod tests {
         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

@@ -3394,7 +3394,7 @@ 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",
+    "text": "module __fayalite_formal_reset(output rst);\n    assign rst = $initstate;\nendmodule\n",
     "target": "~check_formal|formal_reset"
   }
 ]]
@@ -3407,20 +3407,20 @@ 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]
-        inst formal_reset of formal_reset @[formal.rs 189:24]
+        inst formal_reset of formal_reset @[formal.rs 185: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]
+        inst formal_reset_1 of formal_reset @[formal.rs 185: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]
+        inst formal_reset_2 of formal_reset @[formal.rs 185: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]
+        inst formal_reset_3 of formal_reset @[formal.rs 185: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]
+        inst formal_reset_4 of formal_reset @[formal.rs 185: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]
+        inst formal_reset_5 of formal_reset @[formal.rs 185: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]
+    extmodule formal_reset: @[formal.rs 169:5]
+        output rst: UInt<1> @[formal.rs 172:32]
         defname = __fayalite_formal_reset
 "#,
     };