crates/fayalite/src/util/ready_valid.rs

@@ -178,6 +178,30 @@ 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.
+    //
+    // 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,
+            FormalMode::Prove,
-            14,
+            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);
+    }
 }