switch ready_valid::queue formal proofs to use formal_global_clock

Add support to the simulator for running hdl asserts/assumes and being
able to write to the formal global clock/reset and all any/all_const/seq that are used.
This allows you to use the exact same HDL code for running a simulation and for running a formal proof.

crates/fayalite/src/expr/ops.rs

@@ -4884,7 +4884,12 @@ impl<T: Type> ToExpr for TraceAsStringAsInner<T> {
 }
 
 #[derive(Copy, Clone, PartialEq, Eq, Hash)]
-/// The [`Simulation::io()`] equivalent for a global signal, this is a flipped version of a global signal that allows you to e.g. use [`Simulation::write()`] to write to [`formal_global_clock()`]
+/// The [`Simulation::io()`] equivalent for a global signal, this is a flipped version of a global signal
+/// that allows you to e.g. use [`Simulation::write()`] to write to [`formal_global_clock()`].
+///
+/// [`Simulation::io()`]: crate::sim::Simulation::io
+/// [`Simulation::write()`]: crate::sim::Simulation::write
+/// [`formal_global_clock()`]: crate::formal::formal_global_clock
 pub struct SimIoForGlobal {
     global: FormalInput,
 }