diff --git a/crates/fayalite/src/util/ready_valid.rs b/crates/fayalite/src/util/ready_valid.rs index ac08a64..82d3f1e 100644 --- a/crates/fayalite/src/util/ready_valid.rs +++ b/crates/fayalite/src/util/ready_valid.rs @@ -49,18 +49,6 @@ impl ReadyValid { } } -/// This debug port is only meant to assist the formal proof of the queue. -#[cfg(test)] -#[doc(hidden)] -#[hdl] -pub struct QueueDebugPort { - #[hdl(flip)] - index_to_check: Index, - stored: Element, - inp_index: Index, - out_index: Index, -} - #[hdl_module] pub fn queue( ty: T, @@ -190,22 +178,6 @@ pub fn queue( } } } - // These debug ports expose some internal state during the Induction phase - // of Formal Verification. They are not present in normal use. - #[cfg(test)] - { - #[hdl] - let dbg: QueueDebugPort = m.output(QueueDebugPort[ty][index_ty]); - // read the memory word currently stored at some fixed index - let debug_port = mem.new_read_port(); - connect(debug_port.addr, dbg.index_to_check); - connect(debug_port.en, true); - connect(debug_port.clk, cd.clk); - connect(dbg.stored, debug_port.data); - // also expose the current read and write indices - connect(dbg.inp_index, inp_index_reg); - connect(dbg.out_index, out_index_reg); - } } #[cfg(test)] @@ -224,23 +196,13 @@ mod tests { 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::Prove, - 2, + 14, None, ExportOptions { simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts), ..ExportOptions::default() }, ); - /// Formal verification of the FIFO queue - /// - /// The strategy derives from the observation that, if we filter its - /// input and output streams to consider just one in every N reads and - /// writes (where N is the FIFO capacity), then the FIFO effectively - /// behaves as a one-entry FIFO. - /// - /// In particular, any counterexample of the full FIFO behaving badly - /// will also be caught by one of the filtered versions (one which - /// 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] @@ -255,8 +217,6 @@ mod tests { rst: formal_reset().to_reset(), }, ); - - // random input data #[hdl] let inp_data: HdlOption> = wire(); #[hdl] @@ -265,26 +225,16 @@ mod tests { } else { connect(inp_data, HdlNone()); } - - // assert output ready at random #[hdl] let out_ready: Bool = wire(); connect(out_ready, any_seq(Bool)); - - // The current number of elements in the FIFO ranges from zero to - // maximum capacity, inclusive. - let count_ty = UInt::range_inclusive(0..=capacity.get()); - // type for counters that wrap around at the FIFO capacity - let index_ty = UInt::range(0..capacity.get()); - - // among all entries of the FIFO internal circular memory, choose - // one at random to check + let index_ty: UInt<32> = UInt::TYPE; #[hdl] - let index_to_check = wire(index_ty); + let index_to_check = wire(); connect(index_to_check, any_const(index_ty)); - hdl_assume(clk, index_to_check.cmp_lt(capacity.get()), ""); - - // instantiate and connect the queue + 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>], @@ -295,172 +245,109 @@ 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()), + "", + ); - // Keep an independent count of words in the FIFO. Ensure that - // it's always correct, and never overflows. #[hdl] - let expected_count_reg = reg_builder().clock_domain(cd).reset(count_ty.zero()); + let expected_count_reg = reg_builder().clock_domain(cd).reset(0u32); + #[hdl] + let next_expected_count = wire(); + connect(next_expected_count, expected_count_reg); + connect(expected_count_reg, next_expected_count); #[hdl] if ReadyValid::firing(dut.inp) & !ReadyValid::firing(dut.out) { - hdl_assert(clk, expected_count_reg.cmp_ne(capacity.get()), ""); - connect_any(expected_count_reg, expected_count_reg + 1u8); + connect_any(next_expected_count, 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()), ""); - connect_any(expected_count_reg, expected_count_reg - 1u8); + connect_any(next_expected_count, 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), ""); + + #[hdl] + let prev_out_ready_reg = reg_builder().clock_domain(cd).reset(!0_hdl_u3); + connect_any( + prev_out_ready_reg, + (prev_out_ready_reg << 1) | out_ready.cast_to(UInt[1]), + ); + #[hdl] + let prev_inp_valid_reg = reg_builder().clock_domain(cd).reset(!0_hdl_u3); + connect_any( + prev_inp_valid_reg, + (prev_inp_valid_reg << 1) | HdlOption::is_some(inp_data).cast_to(UInt[1]), + ); + hdl_assume( + clk, + (prev_out_ready_reg & prev_inp_valid_reg).cmp_ne(0u8), + "", + ); - // keep an independent write index into the FIFO's circular buffer #[hdl] let inp_index_reg = reg_builder().clock_domain(cd).reset(index_ty.zero()); #[hdl] - if ReadyValid::firing(dut.inp) { + let stored_inp_data_reg = reg_builder().clock_domain(cd).reset(0u8); + + #[hdl] + if let HdlSome(data) = ReadyValid::firing_data(dut.inp) { #[hdl] - if inp_index_reg.cmp_ne(capacity.get() - 1) { + if inp_index_reg.cmp_lt(index_max) { connect_any(inp_index_reg, inp_index_reg + 1u8); - } else { - connect_any(inp_index_reg, 0_hdl_u0); + #[hdl] + if inp_index_reg.cmp_eq(index_to_check) { + connect(stored_inp_data_reg, data); + } } } - // keep an independent read index into the FIFO's circular buffer + #[hdl] + if inp_index_reg.cmp_lt(index_to_check) { + hdl_assert(clk, stored_inp_data_reg.cmp_eq(0u8), ""); + } + #[hdl] let out_index_reg = reg_builder().clock_domain(cd).reset(index_ty.zero()); #[hdl] - if ReadyValid::firing(dut.out) { + let stored_out_data_reg = reg_builder().clock_domain(cd).reset(0u8); + + #[hdl] + if let HdlSome(data) = ReadyValid::firing_data(dut.out) { #[hdl] - if out_index_reg.cmp_ne(capacity.get() - 1) { + if out_index_reg.cmp_lt(index_max) { connect_any(out_index_reg, out_index_reg + 1u8); - } else { - connect_any(out_index_reg, 0_hdl_u0); - } - } - - // filter the input data stream, predicated by the read index - // matching the chosen position in the FIFO's circular buffer - #[hdl] - let inp_index_matches = wire(); - connect(inp_index_matches, inp_index_reg.cmp_eq(index_to_check)); - #[hdl] - let inp_firing_data = wire(); - connect(inp_firing_data, HdlNone()); - #[hdl] - if inp_index_matches { - connect(inp_firing_data, ReadyValid::firing_data(dut.inp)); - } - - // filter the output data stream, predicated by the write index - // matching the chosen position in the FIFO's circular buffer - #[hdl] - let out_index_matches = wire(); - connect(out_index_matches, out_index_reg.cmp_eq(index_to_check)); - #[hdl] - let out_firing_data = wire(); - connect(out_firing_data, HdlNone()); - #[hdl] - if out_index_matches { - connect(out_firing_data, ReadyValid::firing_data(dut.out)); - } - - // Implement a one-entry FIFO and ensure its equivalence to the - // filtered FIFO. - // - // the holding register for our one-entry FIFO - #[hdl] - let stored_reg = reg_builder().clock_domain(cd).reset(HdlNone()); - #[hdl] - match stored_reg { - // If the holding register is empty... - HdlNone => { #[hdl] - 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), ""), - // If we are indeed receiving some data... - HdlSome(data_in) => { - #[hdl] - match out_firing_data { - // ... 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), ""), - // If we are receiving, but not transmitting, - // store the received data in the holding - // register. - HdlNone => connect(stored_reg, HdlSome(data_in)), - } - } - } - } - // If there is some value stored in the holding register... - HdlSome(stored) => { - #[hdl] - 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), ""), - // 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), ""); - // Also, accept new data, if any. Otherwise, - // let the holding register become empty. - connect(stored_reg, inp_firing_data); - } + if out_index_reg.cmp_eq(index_to_check) { + connect(stored_out_data_reg, data); } } } - // from now on, some extra assertions in order to pass induction - - // sync the holding register, when it's occupied, to the - // corresponding entry in the FIFO's circular buffer - 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), ""); + if out_index_reg.cmp_lt(index_to_check) { + hdl_assert(clk, stored_out_data_reg.cmp_eq(0u8), ""); } - // 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(clk, inp_index_reg.cmp_ge(out_index_reg), ""); - // 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()), ""); - - // strongly constrain the state of the holding register - // - // The holding register is full if and only if the corresponding - // FIFO entry was written to and not yet read. In other words, if - // the number of pending reads until the chosen entry is read out - // is greater than the current FIFO count, then the entry couldn't - // be in the FIFO in the first place. #[hdl] - let pending_reads: UInt = wire(index_ty); - // take care of wrap-around when subtracting indices, add the - // capacity amount to keep the result positive if necessary - #[hdl] - if index_to_check.cmp_ge(out_index_reg) { - connect(pending_reads, index_to_check - out_index_reg); + if inp_index_reg.cmp_lt(index_max) & out_index_reg.cmp_lt(index_max) { + hdl_assert( + clk, + expected_count_reg.cmp_eq(inp_index_reg - out_index_reg), + "", + ); } else { - connect( - pending_reads, - index_to_check + capacity.get() - out_index_reg, + hdl_assert( + clk, + expected_count_reg.cmp_ge(inp_index_reg - out_index_reg), + "", ); } - // check whether the chosen entry is in the FIFO + #[hdl] - let expected_stored: Bool = wire(); - connect(expected_stored, pending_reads.cmp_lt(dut.count)); - // sync with the state of the holding register - hdl_assert( - clk, - expected_stored.cmp_eq(HdlOption::is_some(stored_reg)), - "", - ); + if inp_index_reg.cmp_gt(index_to_check) & out_index_reg.cmp_gt(index_to_check) { + hdl_assert(clk, stored_inp_data_reg.cmp_eq(stored_out_data_reg), ""); + } } } @@ -543,24 +430,4 @@ mod tests { fn test_4_true_true() { test_queue(NonZero::new(4).unwrap(), true, true); } - - #[test] - fn test_many_false_false() { - test_queue(NonZero::new((2 << 16) - 5).unwrap(), false, false); - } - - #[test] - fn test_many_false_true() { - test_queue(NonZero::new((2 << 16) - 5).unwrap(), false, true); - } - - #[test] - fn test_many_true_false() { - test_queue(NonZero::new((2 << 16) - 5).unwrap(), true, false); - } - - #[test] - fn test_many_true_true() { - test_queue(NonZero::new((2 << 16) - 5).unwrap(), true, true); - } }