diff --git a/crates/fayalite/src/util/ready_valid.rs b/crates/fayalite/src/util/ready_valid.rs index 82d3f1e..ac08a64 100644 --- a/crates/fayalite/src/util/ready_valid.rs +++ b/crates/fayalite/src/util/ready_valid.rs @@ -49,6 +49,18 @@ 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, @@ -178,6 +190,22 @@ 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)] @@ -196,13 +224,23 @@ 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, - 14, + 2, 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] @@ -217,6 +255,8 @@ mod tests { rst: formal_reset().to_reset(), }, ); + + // random input data #[hdl] let inp_data: HdlOption> = wire(); #[hdl] @@ -225,16 +265,26 @@ mod tests { } else { connect(inp_data, HdlNone()); } + + // assert output ready at random #[hdl] let out_ready: Bool = wire(); connect(out_ready, any_seq(Bool)); - let index_ty: UInt<32> = UInt::TYPE; + + // 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 #[hdl] - let index_to_check = wire(); + let index_to_check = wire(index_ty); 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_assume(clk, index_to_check.cmp_lt(capacity.get()), ""); + + // instantiate and connect the queue #[hdl] let dut = instance(queue( UInt[ConstUsize::<8>], @@ -245,109 +295,172 @@ 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(0u32); - #[hdl] - let next_expected_count = wire(); - connect(next_expected_count, expected_count_reg); - connect(expected_count_reg, next_expected_count); + let expected_count_reg = reg_builder().clock_domain(cd).reset(count_ty.zero()); #[hdl] if ReadyValid::firing(dut.inp) & !ReadyValid::firing(dut.out) { - connect_any(next_expected_count, expected_count_reg + 1u8); + hdl_assert(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) { - connect_any(next_expected_count, expected_count_reg - 1u8); + hdl_assert(clk, expected_count_reg.cmp_ne(count_ty.zero()), ""); + connect_any(expected_count_reg, expected_count_reg - 1u8); } - 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), - "", - ); + hdl_assert(clk, expected_count_reg.cmp_eq(dut.count), ""); + // 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] - let stored_inp_data_reg = reg_builder().clock_domain(cd).reset(0u8); - - #[hdl] - if let HdlSome(data) = ReadyValid::firing_data(dut.inp) { + if ReadyValid::firing(dut.inp) { #[hdl] - if inp_index_reg.cmp_lt(index_max) { + if inp_index_reg.cmp_ne(capacity.get() - 1) { connect_any(inp_index_reg, inp_index_reg + 1u8); - #[hdl] - if inp_index_reg.cmp_eq(index_to_check) { - connect(stored_inp_data_reg, data); - } + } else { + connect_any(inp_index_reg, 0_hdl_u0); } } - #[hdl] - if inp_index_reg.cmp_lt(index_to_check) { - hdl_assert(clk, stored_inp_data_reg.cmp_eq(0u8), ""); - } - + // keep an independent read index into the FIFO's circular buffer #[hdl] let out_index_reg = reg_builder().clock_domain(cd).reset(index_ty.zero()); #[hdl] - let stored_out_data_reg = reg_builder().clock_domain(cd).reset(0u8); - - #[hdl] - if let HdlSome(data) = ReadyValid::firing_data(dut.out) { + if ReadyValid::firing(dut.out) { #[hdl] - if out_index_reg.cmp_lt(index_max) { + if out_index_reg.cmp_ne(capacity.get() - 1) { 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] - if out_index_reg.cmp_eq(index_to_check) { - connect(stored_out_data_reg, data); + 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); + } } } } + // 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 out_index_reg.cmp_lt(index_to_check) { - hdl_assert(clk, stored_out_data_reg.cmp_eq(0u8), ""); + if let HdlSome(stored) = stored_reg { + hdl_assert(clk, stored.cmp_eq(dut.dbg.stored), ""); } - hdl_assert(clk, inp_index_reg.cmp_ge(out_index_reg), ""); + // 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), ""); + // 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] - 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), - "", - ); + 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); } else { - hdl_assert( - clk, - expected_count_reg.cmp_ge(inp_index_reg - out_index_reg), - "", + connect( + pending_reads, + index_to_check + capacity.get() - out_index_reg, ); } - + // check whether the chosen entry is in the FIFO #[hdl] - 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), ""); - } + 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)), + "", + ); } } @@ -430,4 +543,24 @@ 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); + } }