From fef7fea3ea4bf10a9c1bb3162b7d54ccb05a690c Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Mon, 23 Dec 2024 08:56:19 -0300 Subject: [PATCH 1/4] Initial queue formal proof based on one-entry FIFO equivalence For now, only check that the basic properties work in bounded model check mode, leave the induction proof for later. Partially replace the previously existing proof. Remove earlier assumptions and bounds that don't apply for this proof. Use parameterized types instead of hard-coded types. --- crates/fayalite/src/util/ready_valid.rs | 190 ++++++++++++++---------- 1 file changed, 112 insertions(+), 78 deletions(-) diff --git a/crates/fayalite/src/util/ready_valid.rs b/crates/fayalite/src/util/ready_valid.rs index 82d3f1e..53279dc 100644 --- a/crates/fayalite/src/util/ready_valid.rs +++ b/crates/fayalite/src/util/ready_valid.rs @@ -195,7 +195,7 @@ mod tests { assert_formal( 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, + FormalMode::BMC, 14, None, ExportOptions { @@ -203,6 +203,16 @@ mod tests { ..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 an 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 +227,8 @@ mod tests { rst: formal_reset().to_reset(), }, ); + + // random input data #[hdl] let inp_data: HdlOption> = wire(); #[hdl] @@ -225,16 +237,25 @@ 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), ""); + + // instantiate and connect the queue #[hdl] let dut = instance(queue( UInt[ConstUsize::<8>], @@ -245,108 +266,121 @@ 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); - #[hdl] - if out_index_reg.cmp_eq(index_to_check) { - connect(stored_out_data_reg, data); - } + } 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] - if out_index_reg.cmp_lt(index_to_check) { - hdl_assert(clk, stored_out_data_reg.cmp_eq(0u8), ""); + 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)); } - hdl_assert(clk, inp_index_reg.cmp_ge(out_index_reg), ""); - + // filter the output data stream, predicated by the write index + // matching the chosen position in the FIFO's circular buffer #[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), - "", - ); - } else { - hdl_assert( - clk, - expected_count_reg.cmp_ge(inp_index_reg - out_index_reg), - "", - ); + 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 an one-entry FIFO and ensure its equivalence to the + // filtered FIFO. + // + // the holding register for our one-entry 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 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); + } + } + } } } } From ad1101934c3f4330867f563cc86312801af4ca34 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Thu, 26 Dec 2024 10:30:16 -0300 Subject: [PATCH 2/4] Add assertions and debug ports in order for the FIFO to pass induction As some proofs involving memories, it is necessary to add more ports to the queue interface, to sync state. These changes are predicated on the test environment, so normal use is not affected. Since some speedup is achieved, use the saved time to test with a deeper FIFO. --- crates/fayalite/src/util/ready_valid.rs | 99 ++++++++++++++++++++++++- 1 file changed, 97 insertions(+), 2 deletions(-) diff --git a/crates/fayalite/src/util/ready_valid.rs b/crates/fayalite/src/util/ready_valid.rs index 53279dc..8007ac3 100644 --- a/crates/fayalite/src/util/ready_valid.rs +++ b/crates/fayalite/src/util/ready_valid.rs @@ -178,6 +178,30 @@ pub fn queue( } } } + // These debug ports expose some internal state during the Induction phase + // of Formal Verification. They are not present in normal use. + // + // TODO: gather the new debug ports in a bundle + #[cfg(test)] + { + // read the memory word currently stored at some fixed index + let debug_port = mem.new_read_port(); + #[hdl] + let dbg_index_to_check: UInt = m.input(index_ty); + #[hdl] + let dbg_stored: T = m.output(ty); + 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 + #[hdl] + let dbg_inp_index: UInt = m.output(index_ty); + #[hdl] + let dbg_out_index: UInt = m.output(index_ty); + connect(dbg_inp_index, inp_index_reg); + connect(dbg_out_index, out_index_reg); + } } #[cfg(test)] @@ -195,8 +219,8 @@ mod tests { assert_formal( 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::BMC, - 14, + FormalMode::Prove, + 2, None, ExportOptions { simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts), @@ -254,6 +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()), ""); // instantiate and connect the queue #[hdl] @@ -382,6 +407,56 @@ mod tests { } } } + + // 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), ""); + } + + // 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] + 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 { + connect( + pending_reads, + index_to_check + capacity.get() - 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)), + "", + ); } } @@ -464,4 +539,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); + } } From 9f0fb0188a8c7eb8d7fa5f99037b0b13d01b7474 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Thu, 26 Dec 2024 14:52:59 -0300 Subject: [PATCH 3/4] Gather the FIFO debug ports in a bundle For some reason, can't mark QueueDebugPort as #[cfg(test)]. --- crates/fayalite/src/util/ready_valid.rs | 39 +++++++++++++------------ 1 file changed, 21 insertions(+), 18 deletions(-) diff --git a/crates/fayalite/src/util/ready_valid.rs b/crates/fayalite/src/util/ready_valid.rs index 8007ac3..84a0dc3 100644 --- a/crates/fayalite/src/util/ready_valid.rs +++ b/crates/fayalite/src/util/ready_valid.rs @@ -49,6 +49,17 @@ impl ReadyValid { } } +/// This debug port is only meant to assist the formal proof of the queue. +#[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, @@ -180,27 +191,19 @@ pub fn queue( } // These debug ports expose some internal state during the Induction phase // of Formal Verification. They are not present in normal use. - // - // TODO: gather the new debug ports in a bundle #[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(); - #[hdl] - let dbg_index_to_check: UInt = m.input(index_ty); - #[hdl] - let dbg_stored: T = m.output(ty); - connect(debug_port.addr, dbg_index_to_check); + 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); + connect(dbg.stored, debug_port.data); // also expose the current read and write indices - #[hdl] - let dbg_inp_index: UInt = m.output(index_ty); - #[hdl] - let dbg_out_index: UInt = m.output(index_ty); - connect(dbg_inp_index, inp_index_reg); - connect(dbg_out_index, out_index_reg); + connect(dbg.inp_index, inp_index_reg); + connect(dbg.out_index, out_index_reg); } } @@ -412,15 +415,15 @@ mod tests { // 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); + 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(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(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... From 8d7c6910029168b1a8cc6e6252dac7fdbe1045ef Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Thu, 26 Dec 2024 19:41:36 -0300 Subject: [PATCH 4/4] Grammar fix. --- crates/fayalite/src/util/ready_valid.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crates/fayalite/src/util/ready_valid.rs b/crates/fayalite/src/util/ready_valid.rs index 84a0dc3..f499d54 100644 --- a/crates/fayalite/src/util/ready_valid.rs +++ b/crates/fayalite/src/util/ready_valid.rs @@ -235,7 +235,7 @@ mod tests { /// 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 an one-entry FIFO. + /// 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 @@ -361,7 +361,7 @@ mod tests { connect(out_firing_data, ReadyValid::firing_data(dut.out)); } - // Implement an one-entry FIFO and ensure its equivalence to the + // Implement a one-entry FIFO and ensure its equivalence to the // filtered FIFO. // // the holding register for our one-entry FIFO