From ffca1a279d79507c025a8d969bfff18295760c02 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Fri, 5 Jun 2026 00:41:51 -0700 Subject: [PATCH] switch ready_valid::queue formal proofs to use formal_global_clock --- crates/fayalite/src/util/ready_valid.rs | 34 ++++++++++++------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/crates/fayalite/src/util/ready_valid.rs b/crates/fayalite/src/util/ready_valid.rs index a15b837..66f0aea 100644 --- a/crates/fayalite/src/util/ready_valid.rs +++ b/crates/fayalite/src/util/ready_valid.rs @@ -241,15 +241,13 @@ mod tests { /// happens to be in phase with the offending input or output). #[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 cd = wire(); connect( cd, #[hdl] ClockDomain { - clk, + clk: formal_global_clock(), rst: formal_reset().to_reset(), }, ); @@ -280,7 +278,7 @@ mod tests { #[hdl] let index_to_check = wire(index_ty); connect(index_to_check, any_const(index_ty)); - hdl_assume(clk, index_to_check.cmp_lt(capacity.get()), ""); + hdl_assume(cd.clk, index_to_check.cmp_lt(capacity.get()), ""); // instantiate and connect the queue #[hdl] @@ -300,13 +298,13 @@ mod tests { let expected_count_reg = reg_builder().clock_domain(cd).reset(count_ty.zero()); #[hdl] if ReadyValid::firing(dut.inp) & !ReadyValid::firing(dut.out) { - hdl_assert(clk, expected_count_reg.cmp_ne(capacity.get()), ""); + hdl_assert(cd.clk, expected_count_reg.cmp_ne(capacity.get()), ""); connect_any(expected_count_reg, expected_count_reg + 1u8); } else if !ReadyValid::firing(dut.inp) & ReadyValid::firing(dut.out) { - hdl_assert(clk, expected_count_reg.cmp_ne(count_ty.zero()), ""); + hdl_assert(cd.clk, expected_count_reg.cmp_ne(count_ty.zero()), ""); connect_any(expected_count_reg, expected_count_reg - 1u8); } - hdl_assert(clk, expected_count_reg.cmp_eq(dut.count), ""); + hdl_assert(cd.clk, expected_count_reg.cmp_eq(dut.count), ""); // keep an independent write index into the FIFO's circular buffer #[hdl] @@ -374,7 +372,7 @@ mod tests { match inp_firing_data { // ... and we are not receiving data, then we must not // transmit any data. - HdlNone => hdl_assert(clk, HdlOption::is_none(out_firing_data), ""), + HdlNone => hdl_assert(cd.clk, HdlOption::is_none(out_firing_data), ""), // If we are indeed receiving some data... HdlSome(data_in) => { #[hdl] @@ -382,7 +380,9 @@ mod tests { // ... and transmitting at the same time, we // must be transmitting the input data itself, // since the holding register is empty. - HdlSome(data_out) => hdl_assert(clk, data_out.cmp_eq(data_in), ""), + HdlSome(data_out) => { + hdl_assert(cd.clk, data_out.cmp_eq(data_in), "") + } // If we are receiving, but not transmitting, // store the received data in the holding // register. @@ -397,11 +397,11 @@ mod tests { match out_firing_data { // ... and we are not transmitting it, we cannot // receive any more data. - HdlNone => hdl_assert(clk, HdlOption::is_none(inp_firing_data), ""), + HdlNone => hdl_assert(cd.clk, HdlOption::is_none(inp_firing_data), ""), // If we are transmitting a previously stored value... HdlSome(data_out) => { // ... it must be the same data we stored earlier. - hdl_assert(clk, data_out.cmp_eq(stored), ""); + hdl_assert(cd.clk, data_out.cmp_eq(stored), ""); // Also, accept new data, if any. Otherwise, // let the holding register become empty. connect(stored_reg, inp_firing_data); @@ -417,17 +417,17 @@ mod tests { connect(dut.dbg.index_to_check, index_to_check); #[hdl] if let HdlSome(stored) = stored_reg { - hdl_assert(clk, stored.cmp_eq(dut.dbg.stored), ""); + hdl_assert(cd.clk, stored.cmp_eq(dut.dbg.stored), ""); } // sync the read and write indices - hdl_assert(clk, inp_index_reg.cmp_eq(dut.dbg.inp_index), ""); - hdl_assert(clk, out_index_reg.cmp_eq(dut.dbg.out_index), ""); + hdl_assert(cd.clk, inp_index_reg.cmp_eq(dut.dbg.inp_index), ""); + hdl_assert(cd.clk, out_index_reg.cmp_eq(dut.dbg.out_index), ""); // the indices should never go past the capacity, but induction // doesn't know that... - hdl_assert(clk, inp_index_reg.cmp_lt(capacity.get()), ""); - hdl_assert(clk, out_index_reg.cmp_lt(capacity.get()), ""); + hdl_assert(cd.clk, inp_index_reg.cmp_lt(capacity.get()), ""); + hdl_assert(cd.clk, out_index_reg.cmp_lt(capacity.get()), ""); // strongly constrain the state of the holding register // @@ -455,7 +455,7 @@ mod tests { connect(expected_stored, pending_reads.cmp_lt(dut.count)); // sync with the state of the holding register hdl_assert( - clk, + cd.clk, expected_stored.cmp_eq(HdlOption::is_some(stored_reg)), "", );