diff --git a/crates/fayalite/src/util/ready_valid.rs b/crates/fayalite/src/util/ready_valid.rs
index 28ea691..ac08a64 100644
--- a/crates/fayalite/src/util/ready_valid.rs
+++ b/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,
@@ -180,27 +192,19 @@ 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)]
     {
+        #[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();
-        #[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 +416,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...