From aaa2cb193e2147d142f5b5bb9eadb836ba64479a Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Tue, 15 Oct 2024 02:25:35 -0700 Subject: [PATCH] add formal proof for unit_free_regs_tracker --- Cargo.lock | 8 +- .../src/reg_alloc/unit_free_regs_tracker.rs | 351 +++++++++++++++++- 2 files changed, 342 insertions(+), 17 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 5fd33a9..eafe629 100644 --- a/Cargo.lock +++ b/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", diff --git a/crates/cpu/src/reg_alloc/unit_free_regs_tracker.rs b/crates/cpu/src/reg_alloc/unit_free_regs_tracker.rs index 69f8d30..7d3dc0d 100644 --- a/crates/cpu/src/reg_alloc/unit_free_regs_tracker.rs +++ b/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> = - 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::>() .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); + } +}