add formal proof for unit_free_regs_tracker

Cargo.lock

@@ -279,7 +279,7 @@ checksum = "e8c02a5121d4ea3eb16a80748c74f5549a5665e4c21333c6098f283870fbdea6"
 [[package]]
 name = "fayalite"
 version = "0.2.0"
-source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#3939ce2360138c75c53972368069c8f882111571"
+source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#3d0f95cfe5a910f79177babf8fe12483f83e96f9"
 dependencies = [
  "bitvec",
  "blake3",
@@ -300,7 +300,7 @@ dependencies = [
 [[package]]
 name = "fayalite-proc-macros"
 version = "0.2.0"
-source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#3939ce2360138c75c53972368069c8f882111571"
+source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#3d0f95cfe5a910f79177babf8fe12483f83e96f9"
 dependencies = [
  "fayalite-proc-macros-impl",
 ]
@@ -308,7 +308,7 @@ dependencies = [
 [[package]]
 name = "fayalite-proc-macros-impl"
 version = "0.2.0"
-source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#3939ce2360138c75c53972368069c8f882111571"
+source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#3d0f95cfe5a910f79177babf8fe12483f83e96f9"
 dependencies = [
  "base16ct",
  "num-bigint",
@@ -323,7 +323,7 @@ dependencies = [
 [[package]]
 name = "fayalite-visit-gen"
 version = "0.2.0"
-source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#3939ce2360138c75c53972368069c8f882111571"
+source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#3d0f95cfe5a910f79177babf8fe12483f83e96f9"
 dependencies = [
  "indexmap",
  "prettyplease",

crates/cpu/src/reg_alloc/unit_free_regs_tracker.rs

@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: LGPL-3.0-or-later
 // See Notices.txt for copyright information
 use crate::util::tree_reduce::tree_reduce;
-use fayalite::{prelude::*, util::ready_valid::ReadyValid};
+use fayalite::{module::wire_with_loc, prelude::*, util::ready_valid::ReadyValid};
 use std::{num::NonZeroUsize, ops::Range};
 
 #[hdl_module]
@@ -17,7 +17,7 @@ pub fn unit_free_regs_tracker(
         m.input(Array[ReadyValid[UInt[reg_num_width]]][free_at_once.get()]);
     #[hdl]
     let alloc_out: Array<ReadyValid<UInt>> =
-        m.input(Array[ReadyValid[UInt[reg_num_width]]][alloc_at_once.get()]);
+        m.output(Array[ReadyValid[UInt[reg_num_width]]][alloc_at_once.get()]);
     assert!(
         reg_num_width <= isize::MAX.ilog2() as usize,
         "too many registers"
@@ -47,7 +47,7 @@ pub fn unit_free_regs_tracker(
     }) = tree_reduce(
         (0..reg_count).map(|index| Summary {
             range: index..index + 1,
-            count: allocated_reg[index]
+            count: (!allocated_reg[index])
                 .cast_to_static::<UInt<1>>()
                 .cast_to(count_ty),
             count_overflowed: false.to_expr(),
@@ -55,25 +55,35 @@ pub fn unit_free_regs_tracker(
         }),
         |l, r| {
             let range = l.range.start..r.range.end;
-            #[hdl]
-            let reduced_count = wire(count_ty);
+            let reduced_count = wire_with_loc(
+                &format!("reduced_count_{}_{}", range.start, range.end),
+                SourceLocation::caller(),
+                count_ty,
+            );
             connect_any(reduced_count, l.count + r.count);
-            #[hdl]
-            let reduced_count_overflowed = wire();
+            let reduced_count_overflowed = wire_with_loc(
+                &format!("reduced_count_overflowed_{}_{}", range.start, range.end),
+                SourceLocation::caller(),
+                Bool,
+            );
             connect(
                 reduced_count_overflowed,
                 (l.count + r.count).cmp_ne(reduced_count) | l.count_overflowed | r.count_overflowed,
             );
-            #[hdl]
-            let reduced_alloc_nums = wire(
+            let reduced_alloc_nums = wire_with_loc(
+                &format!("reduced_alloc_nums_{}_{}", range.start, range.end),
+                SourceLocation::caller(),
                 Array[UInt[Expr::ty(l.alloc_nums).element().width() + 1]][alloc_at_once.get()],
             );
             for alloc_index in 0..alloc_at_once.get() {
                 #[hdl]
-                if l.count_overflowed | l.count.cmp_ge(alloc_at_once) {
+                if l.count_overflowed | l.count.cmp_gt(alloc_index) {
                     connect(reduced_alloc_nums[alloc_index], l.alloc_nums[alloc_index]);
                 } else {
-                    connect(reduced_alloc_nums[alloc_index], r.alloc_nums[alloc_index]);
+                    connect(
+                        reduced_alloc_nums[alloc_index],
+                        r.alloc_nums[alloc_index.to_expr() - l.count] + l.range.len(),
+                    );
                 }
             }
             Summary {
@@ -93,7 +103,7 @@ pub fn unit_free_regs_tracker(
             connect(allocated_reg[alloc_num], true);
         }
         #[hdl]
-        if count_overflowed | count.cmp_ge(alloc_index) {
+        if count_overflowed | count.cmp_gt(alloc_index) {
             connect(
                 alloc_out[alloc_index].data,
                 HdlSome(alloc_nums[alloc_index]),
@@ -107,4 +117,319 @@ pub fn unit_free_regs_tracker(
     }
 }
 
-// TODO: add formal proof of unit_free_regs_tracker
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use fayalite::{
+        cli::FormalMode, firrtl::ExportOptions,
+        module::transform::simplify_enums::SimplifyEnumsKind, testing::assert_formal,
+    };
+    use std::num::NonZero;
+
+    fn test_unit_free_regs_tracker(
+        free_at_once: NonZeroUsize,
+        alloc_at_once: NonZeroUsize,
+        reg_num_width: usize,
+    ) {
+        // enough time to completely allocate all regs, free whatever we please,
+        // allocate one, then completely free the rest
+        let history_len = (3 + 2 * (1 << reg_num_width)).max(5);
+        assert_formal(
+            format_args!(
+                "test_unit_free_regs_tracker_{free_at_once}_{alloc_at_once}_{reg_num_width}"
+            ),
+            unit_free_regs_tracker_test(free_at_once, alloc_at_once, reg_num_width, history_len),
+            FormalMode::Prove,
+            history_len as u64 + 2,
+            None,
+            ExportOptions {
+                simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts),
+                ..ExportOptions::default()
+            },
+        );
+        #[hdl_module]
+        fn unit_free_regs_tracker_test(
+            free_at_once: NonZeroUsize,
+            alloc_at_once: NonZeroUsize,
+            reg_num_width: usize,
+            history_len: usize,
+        ) {
+            #[hdl]
+            let clk: Clock = m.input();
+            #[hdl]
+            let cd = wire();
+            connect(
+                cd,
+                #[hdl]
+                ClockDomain {
+                    clk,
+                    rst: formal_reset().to_reset(),
+                },
+            );
+            #[hdl]
+            let dut = instance(unit_free_regs_tracker(
+                free_at_once,
+                alloc_at_once,
+                reg_num_width,
+            ));
+            connect(dut.cd, cd);
+            let reg_count = 1 << reg_num_width;
+            let reg_num_ty = UInt[reg_num_width];
+            #[hdl]
+            let free_reg = reg_builder().clock_domain(cd).reset(vec![true; reg_count]);
+            for free_index in 0..free_at_once.get() {
+                #[hdl]
+                if any_seq(Bool) {
+                    let data = any_seq(reg_num_ty);
+                    connect(dut.free_in[free_index].data, HdlSome(data));
+                } else {
+                    connect(
+                        dut.free_in[free_index].data,
+                        HdlOption[reg_num_ty].HdlNone(),
+                    );
+                }
+                #[hdl]
+                if let HdlSome(free) = ReadyValid::firing_data(dut.free_in[free_index]) {
+                    hdl_assume(clk, !free_reg[free], "");
+                    connect(free_reg[free], true);
+                }
+            }
+            #[hdl]
+            let free_before_alloc_array = wire(Array[Expr::ty(free_reg)][alloc_at_once.get() + 1]);
+            connect(free_before_alloc_array[0], free_reg);
+            #[hdl]
+            let expected_alloc = wire(Array[HdlOption[reg_num_ty]][alloc_at_once.get()]);
+            for alloc_index in 0..alloc_at_once.get() {
+                let free_before_alloc = free_before_alloc_array[alloc_index];
+                let free_after_alloc = free_before_alloc_array[alloc_index + 1];
+                connect(free_after_alloc, free_before_alloc);
+                connect(dut.alloc_out[alloc_index].ready, any_seq(Bool));
+                connect(expected_alloc[alloc_index], HdlOption[reg_num_ty].HdlNone());
+                for reg_index in (0..reg_count).rev() {
+                    #[hdl]
+                    if free_before_alloc[reg_index] {
+                        connect(
+                            expected_alloc[alloc_index],
+                            HdlSome(reg_index.cast_to(reg_num_ty)),
+                        );
+                    }
+                    #[hdl]
+                    if let HdlSome(alloc) = expected_alloc[alloc_index] {
+                        #[hdl]
+                        if alloc.cmp_eq(reg_index) {
+                            connect(free_after_alloc[reg_index], false);
+                        }
+                    }
+                }
+                #[hdl]
+                if let HdlSome(expected_alloc) = expected_alloc[alloc_index] {
+                    #[hdl]
+                    if let HdlSome(alloc) = dut.alloc_out[alloc_index].data {
+                        hdl_assert(clk, expected_alloc.cmp_eq(alloc), "");
+                    } else {
+                        hdl_assert(clk, false.to_expr(), "");
+                    }
+                } else {
+                    hdl_assert(clk, HdlOption::is_none(dut.alloc_out[alloc_index].data), "");
+                }
+                #[hdl]
+                if let HdlSome(alloc) = ReadyValid::firing_data(dut.alloc_out[alloc_index]) {
+                    connect(free_reg[alloc], false);
+                }
+            }
+            #[hdl]
+            let free_fired_history_reg = reg_builder()
+                .clock_domain(cd)
+                .reset(repeat(!UInt[history_len].zero(), free_at_once.get()));
+            for free_index in 0..free_at_once.get() {
+                connect_any(
+                    free_fired_history_reg[free_index],
+                    (free_fired_history_reg[free_index] << 1)
+                        | ReadyValid::firing(dut.free_in[free_index]).cast_to(UInt[1]),
+                );
+                hdl_assume(clk, free_fired_history_reg[free_index].any_one_bits(), "");
+            }
+            #[hdl]
+            let alloc_fired_history_reg = reg_builder()
+                .clock_domain(cd)
+                .reset(repeat(!UInt[history_len].zero(), alloc_at_once.get()));
+            for alloc_index in 0..alloc_at_once.get() {
+                connect_any(
+                    alloc_fired_history_reg[alloc_index],
+                    (alloc_fired_history_reg[alloc_index] << 1)
+                        | ReadyValid::firing(dut.alloc_out[alloc_index]).cast_to(UInt[1]),
+                );
+                if alloc_index < reg_count {
+                    hdl_assume(clk, alloc_fired_history_reg[alloc_index].any_one_bits(), "");
+                }
+            }
+            #[hdl]
+            let any_free_history_reg = reg_builder()
+                .clock_domain(cd)
+                .reset(UInt[history_len].zero());
+            #[hdl]
+            let any_allocated_history_reg = reg_builder()
+                .clock_domain(cd)
+                .reset(UInt[history_len].zero());
+            #[hdl]
+            let any_free = wire();
+            connect(any_free, false);
+            #[hdl]
+            let any_allocated = wire();
+            connect(any_allocated, false);
+            for reg_index in 0..reg_count {
+                #[hdl]
+                if free_reg[reg_index] {
+                    connect(any_free, true);
+                } else {
+                    connect(any_allocated, true);
+                }
+            }
+            connect_any(
+                any_free_history_reg,
+                (any_free_history_reg << 1) | any_free.cast_to(UInt[1]),
+            );
+            connect_any(
+                any_allocated_history_reg,
+                (any_allocated_history_reg << 1) | any_allocated.cast_to(UInt[1]),
+            );
+            hdl_assume(clk, any_free_history_reg.any_zero_bits(), "");
+            hdl_assume(clk, any_allocated_history_reg.any_zero_bits(), "");
+        }
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_1_1_0() {
+        test_unit_free_regs_tracker(NonZero::new(1).unwrap(), NonZero::new(1).unwrap(), 0);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_1_1_1() {
+        test_unit_free_regs_tracker(NonZero::new(1).unwrap(), NonZero::new(1).unwrap(), 1);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_1_1_2() {
+        test_unit_free_regs_tracker(NonZero::new(1).unwrap(), NonZero::new(1).unwrap(), 2);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_1_1_3() {
+        test_unit_free_regs_tracker(NonZero::new(1).unwrap(), NonZero::new(1).unwrap(), 3);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_1_1_4() {
+        test_unit_free_regs_tracker(NonZero::new(1).unwrap(), NonZero::new(1).unwrap(), 4);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_1_2_0() {
+        test_unit_free_regs_tracker(NonZero::new(1).unwrap(), NonZero::new(2).unwrap(), 0);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_1_2_4() {
+        test_unit_free_regs_tracker(NonZero::new(1).unwrap(), NonZero::new(2).unwrap(), 4);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_1_3_0() {
+        test_unit_free_regs_tracker(NonZero::new(1).unwrap(), NonZero::new(3).unwrap(), 0);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_1_3_1() {
+        test_unit_free_regs_tracker(NonZero::new(1).unwrap(), NonZero::new(3).unwrap(), 1);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_1_3_4() {
+        test_unit_free_regs_tracker(NonZero::new(1).unwrap(), NonZero::new(3).unwrap(), 4);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_1_4_0() {
+        test_unit_free_regs_tracker(NonZero::new(1).unwrap(), NonZero::new(4).unwrap(), 0);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_1_4_1() {
+        test_unit_free_regs_tracker(NonZero::new(1).unwrap(), NonZero::new(4).unwrap(), 1);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_1_4_2() {
+        test_unit_free_regs_tracker(NonZero::new(1).unwrap(), NonZero::new(4).unwrap(), 2);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_1_4_4() {
+        test_unit_free_regs_tracker(NonZero::new(1).unwrap(), NonZero::new(4).unwrap(), 4);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_2_1_4() {
+        test_unit_free_regs_tracker(NonZero::new(2).unwrap(), NonZero::new(1).unwrap(), 4);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_2_2_0() {
+        test_unit_free_regs_tracker(NonZero::new(2).unwrap(), NonZero::new(2).unwrap(), 0);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_2_2_4() {
+        test_unit_free_regs_tracker(NonZero::new(2).unwrap(), NonZero::new(2).unwrap(), 4);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_3_1_4() {
+        test_unit_free_regs_tracker(NonZero::new(3).unwrap(), NonZero::new(1).unwrap(), 4);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_3_3_0() {
+        test_unit_free_regs_tracker(NonZero::new(3).unwrap(), NonZero::new(3).unwrap(), 0);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_3_3_1() {
+        test_unit_free_regs_tracker(NonZero::new(3).unwrap(), NonZero::new(3).unwrap(), 1);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_3_3_2() {
+        test_unit_free_regs_tracker(NonZero::new(3).unwrap(), NonZero::new(3).unwrap(), 2);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_3_3_4() {
+        test_unit_free_regs_tracker(NonZero::new(3).unwrap(), NonZero::new(3).unwrap(), 4);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_4_1_4() {
+        test_unit_free_regs_tracker(NonZero::new(4).unwrap(), NonZero::new(1).unwrap(), 4);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_4_4_0() {
+        test_unit_free_regs_tracker(NonZero::new(4).unwrap(), NonZero::new(4).unwrap(), 0);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_4_4_1() {
+        test_unit_free_regs_tracker(NonZero::new(4).unwrap(), NonZero::new(4).unwrap(), 1);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_4_4_2() {
+        test_unit_free_regs_tracker(NonZero::new(4).unwrap(), NonZero::new(4).unwrap(), 2);
+    }
+
+    #[test]
+    fn test_unit_free_regs_tracker_4_4_4() {
+        test_unit_free_regs_tracker(NonZero::new(4).unwrap(), NonZero::new(4).unwrap(), 4);
+    }
+}