crates/fayalite/src/util/ready_valid.rs

@@ -49,6 +49,18 @@ impl<T: Type> ReadyValid<T> {
     }
 }
 
+/// This debug port is only meant to assist the formal proof of the queue.
+#[cfg(test)]
+#[doc(hidden)]
+#[hdl]
+pub struct QueueDebugPort<Element, Index> {
+    #[hdl(flip)]
+    index_to_check: Index,
+    stored: Element,
+    inp_index: Index,
+    out_index: Index,
+}
+
 #[hdl_module]
 pub fn queue<T: Type>(
     ty: T,
@@ -178,6 +190,22 @@ pub fn queue<T: Type>(
             }
         }
     }
+    // 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<T, UInt> = 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<UInt<8>> = 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);
-
+            if ReadyValid::firing(dut.inp) {
                 #[hdl]
-            if let HdlSome(data) = ReadyValid::firing_data(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);
-
+            if ReadyValid::firing(dut.out) {
                 #[hdl]
-            if let HdlSome(data) = ReadyValid::firing_data(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);
-                    }
-                }
-            }
-
-            #[hdl]
-            if out_index_reg.cmp_lt(index_to_check) {
-                hdl_assert(clk, stored_out_data_reg.cmp_eq(0u8), "");
-            }
-
-            hdl_assert(clk, inp_index_reg.cmp_ge(out_index_reg), "");
-
-            #[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),
-                    "",
-                );
+                    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 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 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);
+                        }
+                    }
+                }
+            }
+
+            // 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)),
+                "",
+            );
         }
     }
 
@@ -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);
+    }
 }