diff --git a/crates/fayalite/src/annotations.rs b/crates/fayalite/src/annotations.rs
index 4ca84dd..252a0ce 100644
--- a/crates/fayalite/src/annotations.rs
+++ b/crates/fayalite/src/annotations.rs
@@ -238,7 +238,10 @@ impl TargetedAnnotation {
     }
     #[track_caller]
     pub fn assert_valid_target(target: Interned<Target>) {
-        assert!(target.is_static(), "can't annotate non-static targets");
+        assert!(
+            target.is_valid_annotation_target(),
+            "not a valid annotation target: {target:?}",
+        );
     }
     pub fn target(&self) -> Interned<Target> {
         self.target
diff --git a/crates/fayalite/src/expr.rs b/crates/fayalite/src/expr.rs
index e235cd7..eb4bf0f 100644
--- a/crates/fayalite/src/expr.rs
+++ b/crates/fayalite/src/expr.rs
@@ -6,6 +6,7 @@ use crate::{
     bundle::{Bundle, BundleType},
     enum_::{Enum, EnumType},
     expr::target::{GetTarget, Target},
+    formal::FormalInput,
     int::{Bool, DynSize, IntType, SIntValue, Size, SizeType, UInt, UIntType, UIntValue},
     intern::{Intern, Interned},
     memory::{DynPortType, MemPort, PortType},
@@ -227,6 +228,8 @@ expr_enum! {
         RegSync(Reg<CanonicalType, SyncReset>),
         RegAsync(Reg<CanonicalType, AsyncReset>),
         MemPort(MemPort<DynPortType>),
+        FormalInput(FormalInput),
+        SimIoForGlobal(ops::SimIoForGlobal),
     }
 }
 
@@ -1908,3 +1911,19 @@ impl<T: ?Sized + ValueType> ToTraceAsStringImpl<T::Type, value_category::ValueCa
         Valueless::new(ty.with_new_inner_ty(this.ty().intern_sized()))
     }
 }
+
+impl ToLiteralBits for FormalInput {
+    fn to_literal_bits(&self) -> Result<Interned<BitSlice>, NotALiteralExpr> {
+        Err(NotALiteralExpr)
+    }
+}
+
+impl ToExpr for FormalInput {
+    fn to_expr(&self) -> Expr<Self::Type> {
+        Expr {
+            __enum: ExprEnum::FormalInput(*self).intern_sized(),
+            __ty: self.ty(),
+            __flow: self.flow(),
+        }
+    }
+}
diff --git a/crates/fayalite/src/expr/ops.rs b/crates/fayalite/src/expr/ops.rs
index b2e20ad..ae1a7ce 100644
--- a/crates/fayalite/src/expr/ops.rs
+++ b/crates/fayalite/src/expr/ops.rs
@@ -17,6 +17,7 @@ use crate::{
         },
         value_category::ValueCategoryExpr,
     },
+    formal::FormalInput,
     int::{
         Bool, BoolOrIntType, DynSize, IntType, KnownSize, SInt, SIntType, SIntValue, Size, UInt,
         UIntType, UIntValue,
@@ -4881,3 +4882,64 @@ 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()`]
+pub struct SimIoForGlobal {
+    global: FormalInput,
+}
+
+impl fmt::Debug for SimIoForGlobal {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.debug_tuple("SimIoForGlobal").field(&self.global).finish()
+    }
+}
+
+impl SimIoForGlobal {
+    pub fn new(global: FormalInput) -> Self {
+        Self { global }
+    }
+    pub fn global(self) -> FormalInput {
+        self.global
+    }
+    pub(crate) fn must_connect_to(self) -> bool {
+        true
+    }
+    pub fn flow(self) -> Flow {
+        self.global.flow().flip()
+    }
+    pub(crate) fn source_location(self) -> crate::source_location::SourceLocation {
+        self.global.source_location()
+    }
+}
+
+impl GetTarget for SimIoForGlobal {
+    fn target(&self) -> Option<Interned<Target>> {
+        Some(Target::from(*self).intern_sized())
+    }
+}
+
+impl ToLiteralBits for SimIoForGlobal {
+    fn to_literal_bits(&self) -> Result<Interned<BitSlice>, NotALiteralExpr> {
+        Err(NotALiteralExpr)
+    }
+}
+
+impl ValueType for SimIoForGlobal {
+    type Type = CanonicalType;
+    type ValueCategory = ValueCategoryExpr;
+
+    fn ty(&self) -> Self::Type {
+        self.global.ty()
+    }
+}
+
+impl ToExpr for SimIoForGlobal {
+    fn to_expr(&self) -> Expr<Self::Type> {
+        Expr {
+            __enum: ExprEnum::SimIoForGlobal(*self).intern(),
+            __ty: self.ty(),
+            __flow: self.flow(),
+        }
+    }
+}
diff --git a/crates/fayalite/src/expr/target.rs b/crates/fayalite/src/expr/target.rs
index 9016111..d7775ec 100644
--- a/crates/fayalite/src/expr/target.rs
+++ b/crates/fayalite/src/expr/target.rs
@@ -4,6 +4,7 @@ use crate::{
     array::Array,
     bundle::{Bundle, BundleField},
     expr::{Expr, Flow, ToExpr, ValueType, value_category::ValueCategoryExpr},
+    formal::FormalInput,
     intern::{Intern, Interned},
     memory::{DynPortType, MemPort},
     module::{Instance, ModuleIO, TargetName},
@@ -295,6 +296,14 @@ impl_target_base! {
         #[is = is_instance]
         #[to = instance]
         Instance(Instance<Bundle>),
+        #[from = from]
+        #[is = is_formal_input]
+        #[to = formal_input]
+        FormalInput(FormalInput),
+        #[from = from]
+        #[is = is_sim_io_for_global]
+        #[to = sim_io_for_global]
+        SimIoForGlobal(crate::expr::ops::SimIoForGlobal),
     }
 }
 
@@ -343,6 +352,8 @@ impl TargetBase {
             TargetBase::RegAsync(v) => TargetName(v.scoped_name(), None),
             TargetBase::Wire(v) => TargetName(v.scoped_name(), None),
             TargetBase::Instance(v) => TargetName(v.scoped_name(), None),
+            TargetBase::FormalInput(v) => TargetName(v.scoped_name(), None),
+            TargetBase::SimIoForGlobal(v) => TargetName(v.global().scoped_name(), None),
         }
     }
     pub fn canonical_ty(&self) -> CanonicalType {
@@ -354,6 +365,21 @@ impl TargetBase {
             TargetBase::RegAsync(v) => v.ty(),
             TargetBase::Wire(v) => v.ty(),
             TargetBase::Instance(v) => v.ty().canonical(),
+            TargetBase::FormalInput(v) => v.ty(),
+            TargetBase::SimIoForGlobal(v) => v.ty(),
+        }
+    }
+    pub fn is_valid_annotation_target(&self) -> bool {
+        match self {
+            Self::ModuleIO(_) => true,
+            Self::MemPort(_) => true,
+            Self::Reg(_) => true,
+            Self::RegSync(_) => true,
+            Self::RegAsync(_) => true,
+            Self::Wire(_) => true,
+            Self::Instance(_) => true,
+            Self::FormalInput(_) => false,
+            Self::SimIoForGlobal(_) => false,
         }
     }
 }
@@ -548,6 +574,16 @@ impl Target {
             }
         }
     }
+    pub fn is_valid_annotation_target(&self) -> bool {
+        let mut target = self;
+        loop {
+            match target {
+                Self::Base(target_base) => return target_base.is_valid_annotation_target(),
+                Self::Child(v) if !v.path_element().is_static() => return false,
+                Self::Child(v) => target = &v.parent,
+            }
+        }
+    }
     #[must_use]
     pub fn join(&self, path_element: Interned<TargetPathElement>) -> Self {
         TargetChild::new(self.intern(), path_element).into()
@@ -664,6 +700,18 @@ pub trait GetTarget {
     fn target(&self) -> Option<Interned<Target>>;
 }
 
+impl GetTarget for Target {
+    fn target(&self) -> Option<Interned<Target>> {
+        Some(self.intern())
+    }
+}
+
+impl GetTarget for TargetBase {
+    fn target(&self) -> Option<Interned<Target>> {
+        Some(Target::Base(self.intern()).intern_sized())
+    }
+}
+
 impl GetTarget for bool {
     fn target(&self) -> Option<Interned<Target>> {
         None
diff --git a/crates/fayalite/src/firrtl.rs b/crates/fayalite/src/firrtl.rs
index e2f33ae..60cc0d1 100644
--- a/crates/fayalite/src/firrtl.rs
+++ b/crates/fayalite/src/firrtl.rs
@@ -2,7 +2,7 @@
 // See Notices.txt for copyright information
 #![allow(clippy::type_complexity)]
 use crate::{
-    annotations::{Annotation, TargetedAnnotation},
+    annotations::{Annotation, IntoAnnotations, TargetedAnnotation},
     build::{ToArgs, WriteArgs},
     bundle::{BundleField, BundleType},
     enum_::{EnumType, EnumVariant},
@@ -14,18 +14,19 @@ use crate::{
             TargetPathTraceAsStringInner,
         },
     },
-    formal::FormalKind,
+    formal::{FormalInput, FormalInputKind, FormalKind},
     int::IntType,
     intern::{Intern, Interned},
     memory::{PortKind, PortName},
     module::{
         AnnotatedModuleIO, Block, ExternModuleBody, ExternModuleParameter,
         ExternModuleParameterValue, ModuleBody, ModuleIO, NameId, NameOptId, NormalModuleBody,
-        Stmt, StmtConnect, StmtDeclaration, StmtFormal, StmtIf, StmtInstance, StmtMatch, StmtReg,
-        StmtWire,
+        ScopedNameId, Stmt, StmtConnect, StmtDeclaration, StmtFormal, StmtIf, StmtInstance,
+        StmtMatch, StmtReg, StmtWire,
         transform::{
             simplify_enums::{SimplifyEnumsError, SimplifyEnumsKind, simplify_enums},
             simplify_memories::simplify_memories,
+            visit::Folder,
         },
     },
     prelude::*,
@@ -44,6 +45,7 @@ use std::{
     cell::{Cell, RefCell},
     cmp::Ordering,
     collections::{BTreeMap, VecDeque},
+    convert::Infallible,
     error::Error,
     ffi::OsString,
     fmt::{self, Write},
@@ -53,6 +55,7 @@ use std::{
     ops::{ControlFlow, Range},
     path::{Path, PathBuf},
     rc::Rc,
+    sync::OnceLock,
 };
 
 #[derive(Clone, Debug)]
@@ -385,77 +388,66 @@ struct BlockDefinitionsCache {
     cast_bits_to_enum_exprs: RefCell<HashMap<(String, Enum), String>>,
     cast_bits_to_array_exprs: RefCell<HashMap<(String, Array), String>>,
     cast_bits_to_phantom_const_exprs: RefCell<HashMap<(String, PhantomConst), String>>,
-}
-
-struct BlockDefinitionsState<'a> {
-    rc_definitions: RcDefinitions,
-    parent: &'a BlockDefinitions<'a>,
-    cache: BlockDefinitionsCache,
+    per_module_formal_inputs: RefCell<HashMap<(FormalInput, bool), String>>,
 }
 
 struct BlockDefinitions<'a> {
-    state: Option<BlockDefinitionsState<'a>>,
+    rc_definitions: RcDefinitions,
+    parent: Option<&'a BlockDefinitions<'a>>,
+    cache: BlockDefinitionsCache,
 }
 
 impl<'a> BlockDefinitions<'a> {
     fn new(parent: &'a BlockDefinitions<'a>) -> Self {
         Self {
-            state: Some(BlockDefinitionsState {
-                rc_definitions: RcDefinitions::default(),
-                parent,
-                cache: Default::default(),
-            }),
+            rc_definitions: RcDefinitions::default(),
+            parent: Some(parent),
+            cache: Default::default(),
         }
     }
-    fn none() -> Self {
-        Self { state: None }
+    fn module() -> Self {
+        Self {
+            rc_definitions: RcDefinitions::default(),
+            parent: None,
+            cache: Default::default(),
+        }
     }
     fn get_or_write_definition<K: Hash + Eq>(
-        &mut self,
+        &self,
         key: K,
         field: impl Fn(&BlockDefinitionsCache) -> &RefCell<HashMap<K, String>>,
         write_definition: impl FnOnce(BlockDefinitionsWriter<'_, '_>, &K) -> Result<String>,
     ) -> Result<String> {
-        let state = self.state.as_ref().expect("should be some");
-        let mut cur_state = state;
+        let mut current = self;
         loop {
-            let field = field(&cur_state.cache).borrow();
+            let field = field(&current.cache).borrow();
             if let Some(retval) = field.get(&key) {
                 return Ok(retval.clone());
             }
-            let Some(parent_state) = &cur_state.parent.state else {
+            let Some(parent) = current.parent else {
                 break;
             };
-            cur_state = parent_state;
+            current = parent;
         }
         let retval = write_definition(BlockDefinitionsWriter { definitions: self }, &key)?;
-        Ok(field(&self.state.as_ref().expect("should be some").cache)
+        Ok(field(&self.cache)
             .borrow_mut()
             .entry(key)
             .or_insert(retval)
             .clone())
     }
-    fn write_out(&mut self, indent: Indent<'_>, out: &mut String) {
-        self.state
-            .as_ref()
-            .expect("should be some")
-            .rc_definitions
-            .write_and_clear(indent, out);
+    fn write_out(&self, indent: Indent<'_>, out: &mut String) {
+        self.rc_definitions.write_and_clear(indent, out);
     }
 }
 
 struct BlockDefinitionsWriter<'a, 'b> {
-    definitions: &'b mut BlockDefinitions<'a>,
+    definitions: &'b BlockDefinitions<'a>,
 }
 
 impl BlockDefinitionsWriter<'_, '_> {
-    fn add_definition_line(&mut self, v: impl fmt::Display) {
-        self.definitions
-            .state
-            .as_ref()
-            .expect("should be some")
-            .rc_definitions
-            .add_definition_line(v);
+    fn add_definition_line(&self, v: impl fmt::Display) {
+        self.definitions.rc_definitions.add_definition_line(v);
     }
 }
 
@@ -467,12 +459,6 @@ impl<'a> std::ops::Deref for BlockDefinitionsWriter<'a, '_> {
     }
 }
 
-impl std::ops::DerefMut for BlockDefinitionsWriter<'_, '_> {
-    fn deref_mut(&mut self) -> &mut Self::Target {
-        &mut self.definitions
-    }
-}
-
 struct EnumDef {
     variants: RefCell<Namespace>,
     body: String,
@@ -592,15 +578,19 @@ impl TypeState {
 }
 
 struct ModuleState {
+    module: Interned<Module<Bundle>>,
     ns: Namespace,
     match_arm_values: HashMap<VariantAccess<CanonicalType>, Ident>,
+    block_definitions: Rc<BlockDefinitions<'static>>,
 }
 
-impl Default for ModuleState {
-    fn default() -> Self {
+impl ModuleState {
+    fn new(module: Interned<Module<Bundle>>) -> Self {
         Self {
+            module,
             ns: Default::default(),
             match_arm_values: Default::default(),
+            block_definitions: Rc::new(BlockDefinitions::module()),
         }
     }
 }
@@ -836,6 +826,15 @@ struct FirrtlAnnotation {
     target: AnnotationTarget,
 }
 
+struct ResetSourceLocation;
+
+impl Folder for ResetSourceLocation {
+    type Error = Infallible;
+    fn fold_source_location(&mut self, _v: SourceLocation) -> Result<SourceLocation, Self::Error> {
+        Ok(SourceLocation::builtin())
+    }
+}
+
 struct Exporter<'a> {
     file_backend: &'a mut dyn WrappedFileBackendTrait,
     indent: Indent<'a>,
@@ -968,7 +967,7 @@ impl<'a> Exporter<'a> {
         &mut self,
         value: Expr<FromTy>,
         to_ty: ToTy,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         const_ty: bool,
     ) -> Result<String> {
         let from_ty = value.ty();
@@ -1003,7 +1002,7 @@ impl<'a> Exporter<'a> {
         &mut self,
         firrtl_cast_fn: Option<&str>,
         value: Expr<FromTy>,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         const_ty: bool,
     ) -> Result<String> {
         let value = self.expr(Expr::canonical(value), definitions, const_ty)?;
@@ -1017,7 +1016,7 @@ impl<'a> Exporter<'a> {
         &mut self,
         base: Expr<T>,
         range: Range<usize>,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         const_ty: bool,
     ) -> Result<String> {
         let base_width = base.ty().width();
@@ -1035,20 +1034,19 @@ impl<'a> Exporter<'a> {
     fn array_literal_expr(
         &mut self,
         expr: ops::ArrayLiteral<CanonicalType, DynSize>,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         const_ty: bool,
     ) -> Result<String> {
         definitions.get_or_write_definition(
             (expr, const_ty),
             |c| &c.array_literal_exprs,
-            |mut definitions, &(expr, const_ty)| {
+            |definitions, &(expr, const_ty)| {
                 let ident = self.module.ns.make_new("_array_literal_expr");
                 let ty_str = self.type_state.ty(expr.ty())?;
                 let const_ = if const_ty { "const " } else { "" };
                 definitions.add_definition_line(format_args!("wire {ident}: {const_}{ty_str}"));
                 for (index, element) in expr.element_values().into_iter().enumerate() {
-                    let element =
-                        self.expr(Expr::canonical(element), &mut definitions, const_ty)?;
+                    let element = self.expr(Expr::canonical(element), &definitions, const_ty)?;
                     definitions
                         .add_definition_line(format_args!("connect {ident}[{index}], {element}"));
                 }
@@ -1062,13 +1060,13 @@ impl<'a> Exporter<'a> {
     fn bundle_literal_expr(
         &mut self,
         expr: ops::BundleLiteral<Bundle>,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         const_ty: bool,
     ) -> Result<String> {
         definitions.get_or_write_definition(
             (expr, const_ty),
             |c| &c.bundle_literal_exprs,
-            |mut definitions, &(expr, const_ty)| {
+            |definitions, &(expr, const_ty)| {
                 let ident = self.module.ns.make_new("_bundle_literal_expr");
                 let ty = expr.ty();
                 let (ty_ident, bundle_ns) = self.type_state.bundle_def(ty)?;
@@ -1090,7 +1088,7 @@ impl<'a> Exporter<'a> {
                     );
                     let name = bundle_ns.borrow_mut().get(name);
                     let field_value =
-                        self.expr(Expr::canonical(field_value), &mut definitions, const_ty)?;
+                        self.expr(Expr::canonical(field_value), &definitions, const_ty)?;
                     definitions
                         .add_definition_line(format_args!("connect {ident}.{name}, {field_value}"));
                 }
@@ -1104,13 +1102,13 @@ impl<'a> Exporter<'a> {
     fn uninit_expr(
         &mut self,
         expr: ops::Uninit,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         const_ty: bool,
     ) -> Result<String> {
         definitions.get_or_write_definition(
             (expr, const_ty),
             |c| &c.uninit_exprs,
-            |mut definitions, &(expr, const_ty)| {
+            |definitions, &(expr, const_ty)| {
                 let ident = self.module.ns.make_new("_uninit_expr");
                 let ty = expr.ty();
                 let ty_ident = self.type_state.ty(ty)?;
@@ -1124,7 +1122,7 @@ impl<'a> Exporter<'a> {
     fn enum_literal_expr(
         &mut self,
         expr: ops::EnumLiteral<Enum>,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         const_ty: bool,
     ) -> Result<String> {
         let variant_expr = expr
@@ -1137,13 +1135,13 @@ impl<'a> Exporter<'a> {
         &mut self,
         value_str: String,
         ty: Bundle,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         extra_indent: Indent<'_>,
     ) -> Result<String> {
         definitions.get_or_write_definition(
             (value_str, ty),
             |c| &c.cast_bundle_to_bits_exprs,
-            |mut definitions, &(ref value_str, ty)| {
+            |definitions, &(ref value_str, ty)| {
                 if ty.fields().is_empty() {
                     return Ok("UInt<0>(0)".into());
                 }
@@ -1152,7 +1150,7 @@ impl<'a> Exporter<'a> {
                     return self.expr_cast_to_bits(
                         format!("{value_str}.{field_ident}"),
                         field.ty,
-                        &mut definitions,
+                        &definitions,
                         extra_indent,
                     );
                 }
@@ -1181,7 +1179,7 @@ impl<'a> Exporter<'a> {
                     let field_bits = self.expr_cast_to_bits(
                         format!("{value_str}.{field_ident}"),
                         field.ty,
-                        &mut definitions,
+                        &definitions,
                         extra_indent,
                     )?;
                     definitions.add_definition_line(format_args!(
@@ -1210,13 +1208,13 @@ impl<'a> Exporter<'a> {
         &mut self,
         value_str: String,
         ty: Enum,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         extra_indent: Indent<'_>,
     ) -> Result<String> {
         definitions.get_or_write_definition(
             (value_str, ty),
             |c| &c.cast_enum_to_bits_exprs,
-            |mut definitions, &(ref value_str, ty)| {
+            |definitions, &(ref value_str, ty)| {
                 if ty.variants().is_empty() {
                     return Ok("UInt<0>(0)".into());
                 }
@@ -1241,7 +1239,7 @@ impl<'a> Exporter<'a> {
                         let variant_bits = self.expr_cast_to_bits(
                             variant_value.to_string(),
                             variant_ty,
-                            &mut definitions,
+                            &definitions,
                             extra_indent,
                         )?;
                         definitions.add_definition_line(format_args!(
@@ -1270,13 +1268,13 @@ impl<'a> Exporter<'a> {
         &mut self,
         value_str: String,
         ty: Array,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         extra_indent: Indent<'_>,
     ) -> Result<String> {
         definitions.get_or_write_definition(
             (value_str, ty),
             |c| &c.cast_array_to_bits_exprs,
-            |mut definitions, &(ref value_str, ty)| {
+            |definitions, &(ref value_str, ty)| {
                 if ty.is_empty() {
                     return Ok("UInt<0>(0)".into());
                 }
@@ -1284,7 +1282,7 @@ impl<'a> Exporter<'a> {
                     return self.expr_cast_to_bits(
                         value_str.clone() + "[0]",
                         ty.element(),
-                        &mut definitions,
+                        &definitions,
                         extra_indent,
                     );
                 }
@@ -1299,7 +1297,7 @@ impl<'a> Exporter<'a> {
                     let element_bits = self.expr_cast_to_bits(
                         format!("{value_str}[{index}]"),
                         ty.element(),
-                        &mut definitions,
+                        &definitions,
                         extra_indent,
                     )?;
                     definitions.add_definition_line(format_args!(
@@ -1328,7 +1326,7 @@ impl<'a> Exporter<'a> {
         &mut self,
         value_str: String,
         ty: CanonicalType,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         extra_indent: Indent<'_>,
     ) -> Result<String> {
         match ty.unwrap_transparent_types() {
@@ -1357,13 +1355,13 @@ impl<'a> Exporter<'a> {
         &mut self,
         value_str: String,
         ty: Bundle,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         extra_indent: Indent<'_>,
     ) -> Result<String> {
         definitions.get_or_write_definition(
             (value_str, ty),
             |c| &c.cast_bits_to_bundle_exprs,
-            |mut definitions, &(ref value_str, ty)| {
+            |definitions, &(ref value_str, ty)| {
                 let (ty_ident, _) = self.type_state.bundle_def(ty)?;
                 let retval = self.module.ns.make_new("_cast_bits_to_bundle_expr");
                 definitions
@@ -1420,7 +1418,7 @@ impl<'a> Exporter<'a> {
                     let field_value = self.expr_cast_bits_to(
                         format!("{flattened_ident}.{flattened_field_ident}"),
                         field.ty,
-                        &mut definitions,
+                        &definitions,
                         extra_indent,
                     )?;
                     definitions.add_definition_line(format_args!(
@@ -1435,13 +1433,13 @@ impl<'a> Exporter<'a> {
         &mut self,
         value_str: String,
         ty: Enum,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         extra_indent: Indent<'_>,
     ) -> Result<String> {
         definitions.get_or_write_definition(
             (value_str, ty),
             |c| &c.cast_bits_to_enum_exprs,
-            |mut definitions, &(ref value_str, ty)| {
+            |definitions, &(ref value_str, ty)| {
                 let (ty_ident, enum_def) = self.type_state.enum_def(ty)?;
                 let retval = self.module.ns.make_new("_cast_bits_to_enum_expr");
                 definitions
@@ -1457,7 +1455,7 @@ impl<'a> Exporter<'a> {
                         let variant_value = self.expr_cast_bits_to(
                             value_str.clone(),
                             variant_ty,
-                            &mut definitions,
+                            &definitions,
                             extra_indent,
                         )?;
                         definitions.add_definition_line(format_args!(
@@ -1507,7 +1505,7 @@ impl<'a> Exporter<'a> {
                         let variant_value = self.expr_cast_bits_to(
                             body_value.clone(),
                             variant_ty,
-                            &mut definitions,
+                            &definitions,
                             extra_indent,
                         )?;
                         definitions.add_definition_line(format_args!(
@@ -1530,13 +1528,13 @@ impl<'a> Exporter<'a> {
         &mut self,
         value_str: String,
         ty: Array,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         extra_indent: Indent<'_>,
     ) -> Result<String> {
         definitions.get_or_write_definition(
             (value_str, ty),
             |c| &c.cast_bits_to_array_exprs,
-            |mut definitions, &(ref value_str, ty)| {
+            |definitions, &(ref value_str, ty)| {
                 let retval = self.module.ns.make_new("_cast_bits_to_array_expr");
                 let array_ty = self.type_state.ty(ty)?;
                 definitions
@@ -1565,7 +1563,7 @@ impl<'a> Exporter<'a> {
                     let element_value = self.expr_cast_bits_to(
                         format!("{flattened_ident}[{index}]"),
                         ty.element(),
-                        &mut definitions,
+                        &definitions,
                         extra_indent,
                     )?;
                     definitions.add_definition_line(format_args!(
@@ -1580,7 +1578,7 @@ impl<'a> Exporter<'a> {
         &mut self,
         value_str: String,
         ty: CanonicalType,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         extra_indent: Indent<'_>,
     ) -> Result<String> {
         match ty.unwrap_transparent_types() {
@@ -1603,7 +1601,7 @@ impl<'a> Exporter<'a> {
             CanonicalType::PhantomConst(ty) => definitions.get_or_write_definition(
                 (value_str, ty),
                 |c| &c.cast_bits_to_phantom_const_exprs,
-                |mut definitions, &(ref _value_str, _ty)| {
+                |definitions, &(ref _value_str, _ty)| {
                     let retval = self.module.ns.make_new("_cast_bits_to_phantom_const_expr");
                     definitions
                         .add_definition_line(format_args!("{extra_indent}wire {retval}: {{}}"));
@@ -1620,7 +1618,7 @@ impl<'a> Exporter<'a> {
         &mut self,
         func: &str,
         arg: Expr<T>,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         const_ty: bool,
     ) -> Result<String> {
         Ok(format!(
@@ -1633,7 +1631,7 @@ impl<'a> Exporter<'a> {
         func: &str,
         lhs: Expr<Lhs>,
         rhs: Expr<Rhs>,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         const_ty: bool,
     ) -> Result<String> {
         Ok(format!(
@@ -1642,10 +1640,144 @@ impl<'a> Exporter<'a> {
             rhs = self.expr(Expr::canonical(rhs), definitions, const_ty)?,
         ))
     }
+    #[hdl]
+    fn expr_formal_input(&mut self, formal_input: FormalInput, const_ty: bool) -> Result<String> {
+        let definitions = self.module.block_definitions.clone();
+        definitions.get_or_write_definition(
+            (formal_input, const_ty),
+            |c| &c.per_module_formal_inputs,
+            |definitions, &(formal_input, const_ty)| match formal_input.kind() {
+                FormalInputKind::FormalGlobalClock => {
+                    let reg = Reg::new_unchecked(
+                        ScopedNameId(self.module.module.name_id().into(), formal_input.name_id()),
+                        formal_input.source_location(),
+                        Bool,
+                        #[hdl]
+                        ClockDomain {
+                            clk: false.to_clock(),
+                            rst: false.to_sync_reset(),
+                        },
+                        None,
+                    );
+                    let module_name = self.global_ns.get(self.module.module.name_id());
+                    self.targeted_annotations(
+                        module_name,
+                        vec![],
+                        &Vec::from_iter(
+                            [
+                                SVAttributeAnnotation {
+                                    text: "gclk".intern(),
+                                }
+                                .into_annotations(),
+                                DontTouchAnnotation.into_annotations(),
+                            ]
+                            .into_annotations()
+                            .map(|a| {
+                                TargetedAnnotation::new(
+                                    Target::from(reg.canonical()).intern_sized(),
+                                    a,
+                                )
+                            }),
+                        ),
+                    )?;
+                    definitions.add_definition_line(self.reg(reg.canonical(), &definitions)?);
+                    self.expr(
+                        Expr::canonical(reg.to_expr().to_clock()),
+                        &definitions,
+                        const_ty,
+                    )
+                }
+                FormalInputKind::FormalReset => {
+                    #[hdl_module(extern)]
+                    fn formal_reset() {
+                        #[hdl]
+                        let rst: SyncReset = m.output();
+                        m.annotate_module(BlackBoxInlineAnnotation {
+                            path: "fayalite_formal_reset.v".intern(),
+                            text: r"module __fayalite_formal_reset(output rst);
+    assign rst = $initstate;
+endmodule
+"
+                            .intern(),
+                        });
+                        m.verilog_name("__fayalite_formal_reset");
+                    }
+                    static MOD: OnceLock<Interned<Module<formal_reset>>> = OnceLock::new();
+                    let formal_reset = Instance::new_unchecked(
+                        ScopedNameId(self.module.module.name_id().into(), formal_input.name_id()),
+                        *MOD.get_or_init(|| {
+                            let module = formal_reset();
+                            let Ok(module) = ResetSourceLocation.fold_module(*module);
+                            module.intern_sized()
+                        }),
+                        formal_input.source_location(),
+                    );
+                    definitions.add_definition_line(self.instance(formal_reset.canonical())?);
+                    self.expr(
+                        Expr::canonical(formal_reset.to_expr().rst),
+                        &definitions,
+                        const_ty,
+                    )
+                }
+                FormalInputKind::AnyConst
+                | FormalInputKind::AnySeq
+                | FormalInputKind::AllConst
+                | FormalInputKind::AllSeq => {
+                    match formal_input.ty() {
+                        CanonicalType::UInt(_)
+                        | CanonicalType::SInt(_)
+                        | CanonicalType::Bool(_) => {}
+                        _ => panic!(
+                            "{}() -- unsupported type: {formal_input:#?}",
+                            formal_input.name()
+                        ),
+                    }
+                    if formal_input.ty().size().is_empty() {
+                        return self.expr(formal_input.ty().uninit(), &definitions, const_ty);
+                    }
+                    let reg = Reg::new_unchecked(
+                        ScopedNameId(self.module.module.name_id().into(), formal_input.name_id()),
+                        formal_input.source_location(),
+                        formal_input.ty(),
+                        #[hdl]
+                        ClockDomain {
+                            clk: false.to_clock(),
+                            rst: false.to_sync_reset(),
+                        },
+                        None,
+                    );
+                    let module_name = self.global_ns.get(self.module.module.name_id());
+                    self.targeted_annotations(
+                        module_name,
+                        vec![],
+                        &Vec::from_iter(
+                            [
+                                SVAttributeAnnotation {
+                                    text: match formal_input.kind() {
+                                        FormalInputKind::AnyConst => "anyconst".intern(),
+                                        FormalInputKind::AnySeq => "anyseq".intern(),
+                                        FormalInputKind::AllConst => "allconst".intern(),
+                                        FormalInputKind::AllSeq => "allseq".intern(),
+                                        _ => unreachable!(),
+                                    },
+                                }
+                                .into_annotations(),
+                                DontTouchAnnotation.into_annotations(),
+                            ]
+                            .into_annotations()
+                            .map(|a| TargetedAnnotation::new(Target::from(reg).intern_sized(), a)),
+                        ),
+                    )?;
+                    definitions.add_definition_line(self.reg(reg, &definitions)?);
+                    self.expr(Expr::canonical(reg.to_expr()), &definitions, const_ty)
+                }
+            },
+        )
+    }
     fn expr(
         &mut self,
         expr: Expr<CanonicalType>,
-        definitions: &mut BlockDefinitions<'_>,
+        definitions: &BlockDefinitions<'_>,
         const_ty: bool,
     ) -> Result<String> {
         match *Expr::expr_enum(expr) {
@@ -2012,6 +2144,10 @@ impl<'a> Exporter<'a> {
                 let port_name = Ident::from(expr.port_name());
                 Ok(format!("{mem_name}.{port_name}"))
             }
+            ExprEnum::FormalInput(expr) => self.expr_formal_input(expr, const_ty),
+            ExprEnum::SimIoForGlobal(_) => {
+                unreachable!("Module is known to not contain SimIoForGlobal from validation")
+            }
         }
     }
     fn write_mem_init(
@@ -2126,6 +2262,9 @@ impl<'a> Exporter<'a> {
                     TargetBase::RegAsync(v) => self.module.ns.get(v.name_id()),
                     TargetBase::Wire(v) => self.module.ns.get(v.name_id()),
                     TargetBase::Instance(v) => self.module.ns.get(v.name_id()),
+                    TargetBase::FormalInput(_) | TargetBase::SimIoForGlobal(_) => {
+                        unreachable!("base.is_valid_annotation_target() is known to be false")
+                    }
                 };
                 Ok(AnnotationTargetRef { base, segments })
             }
@@ -2237,38 +2376,51 @@ impl<'a> Exporter<'a> {
         drop(memory_indent);
         Ok(body)
     }
-    fn stmt_reg<R: ResetType>(
+    fn reg<R: ResetType>(
         &mut self,
-        stmt_reg: StmtReg<R>,
-        module_name: Ident,
-        definitions: &mut BlockDefinitions<'_>,
-        body: &mut String,
-    ) -> Result<()> {
-        let StmtReg { annotations, reg } = stmt_reg;
-        let indent = self.indent;
-        self.targeted_annotations(module_name, vec![], &annotations)?;
+        reg: Reg<CanonicalType, R>,
+        definitions: &BlockDefinitions<'_>,
+    ) -> Result<String> {
         let name = self.module.ns.get(reg.name_id());
         let ty = self.type_state.ty(reg.ty())?;
         let clk = self.expr(Expr::canonical(reg.clock_domain().clk), definitions, false)?;
         if let Some(init) = reg.init() {
             let rst = self.expr(Expr::canonical(reg.clock_domain().rst), definitions, false)?;
             let init = self.expr(init, definitions, false)?;
-            writeln!(
-                body,
-                "{indent}regreset {name}: {ty}, {clk}, {rst}, {init}{}",
+            Ok(format!(
+                "regreset {name}: {ty}, {clk}, {rst}, {init}{}",
                 FileInfo::new(reg.source_location()),
-            )
-            .unwrap();
+            ))
         } else {
-            writeln!(
-                body,
-                "{indent}reg {name}: {ty}, {clk}{}",
+            Ok(format!(
+                "reg {name}: {ty}, {clk}{}",
                 FileInfo::new(reg.source_location()),
-            )
-            .unwrap();
+            ))
         }
+    }
+    fn stmt_reg<R: ResetType>(
+        &mut self,
+        stmt_reg: StmtReg<R>,
+        module_name: Ident,
+        definitions: &BlockDefinitions<'_>,
+        body: &mut String,
+    ) -> Result<()> {
+        let StmtReg { annotations, reg } = stmt_reg;
+        let indent = self.indent;
+        self.targeted_annotations(module_name, vec![], &annotations)?;
+        writeln!(body, "{indent}{}", self.reg(reg, definitions)?).unwrap();
         Ok(())
     }
+    fn instance(&mut self, instance: Instance<Bundle>) -> Result<String> {
+        let name = self.module.ns.get(instance.name_id());
+        let instantiated = instance.instantiated();
+        self.add_module(instantiated);
+        let module_name = self.global_ns.get(instantiated.name_id());
+        Ok(format!(
+            "inst {name} of {module_name}{}",
+            FileInfo::new(instance.source_location()),
+        ))
+    }
     fn block(
         &mut self,
         module: Interned<Module<Bundle>>,
@@ -2277,7 +2429,7 @@ impl<'a> Exporter<'a> {
         parent_definitions: &BlockDefinitions,
     ) -> Result<String> {
         let indent = self.indent;
-        let mut definitions = BlockDefinitions::new(parent_definitions);
+        let definitions = BlockDefinitions::new(parent_definitions);
         let mut body = String::new();
         let mut out = String::new();
         let Block { memories, stmts } = block;
@@ -2301,8 +2453,8 @@ impl<'a> Exporter<'a> {
                         )
                         .unwrap();
                     }
-                    let lhs = self.expr(lhs, &mut definitions, false)?;
-                    let rhs = self.expr(rhs, &mut definitions, false)?;
+                    let lhs = self.expr(lhs, &definitions, false)?;
+                    let rhs = self.expr(rhs, &definitions, false)?;
                     writeln!(
                         body,
                         "{indent}connect {lhs}, {rhs}{}",
@@ -2318,9 +2470,9 @@ impl<'a> Exporter<'a> {
                     text,
                     source_location,
                 }) => {
-                    let clk = self.expr(Expr::canonical(clk), &mut definitions, false)?;
-                    let pred = self.expr(Expr::canonical(pred), &mut definitions, false)?;
-                    let en = self.expr(Expr::canonical(en), &mut definitions, false)?;
+                    let clk = self.expr(Expr::canonical(clk), &definitions, false)?;
+                    let pred = self.expr(Expr::canonical(pred), &definitions, false)?;
+                    let en = self.expr(Expr::canonical(en), &definitions, false)?;
                     let kind = match kind {
                         FormalKind::Assert => "assert",
                         FormalKind::Assume => "assume",
@@ -2345,7 +2497,7 @@ impl<'a> Exporter<'a> {
                     let mut when = "when";
                     let mut pushed_indent;
                     loop {
-                        let cond_str = self.expr(Expr::canonical(cond), &mut definitions, false)?;
+                        let cond_str = self.expr(Expr::canonical(cond), &definitions, false)?;
                         writeln!(
                             body,
                             "{indent}{when} {cond_str}:{}",
@@ -2388,7 +2540,7 @@ impl<'a> Exporter<'a> {
                     writeln!(
                         body,
                         "{indent}match {}:{}",
-                        self.expr(Expr::canonical(expr), &mut definitions, false)?,
+                        self.expr(Expr::canonical(expr), &definitions, false)?,
                         FileInfo::new(source_location),
                     )
                     .unwrap();
@@ -2442,29 +2594,20 @@ impl<'a> Exporter<'a> {
                     .unwrap();
                 }
                 Stmt::Declaration(StmtDeclaration::Reg(stmt_reg)) => {
-                    self.stmt_reg(stmt_reg, module_name, &mut definitions, &mut body)?;
+                    self.stmt_reg(stmt_reg, module_name, &definitions, &mut body)?;
                 }
                 Stmt::Declaration(StmtDeclaration::RegSync(stmt_reg)) => {
-                    self.stmt_reg(stmt_reg, module_name, &mut definitions, &mut body)?;
+                    self.stmt_reg(stmt_reg, module_name, &definitions, &mut body)?;
                 }
                 Stmt::Declaration(StmtDeclaration::RegAsync(stmt_reg)) => {
-                    self.stmt_reg(stmt_reg, module_name, &mut definitions, &mut body)?;
+                    self.stmt_reg(stmt_reg, module_name, &definitions, &mut body)?;
                 }
                 Stmt::Declaration(StmtDeclaration::Instance(StmtInstance {
                     annotations,
                     instance,
                 })) => {
                     self.targeted_annotations(module_name, vec![], &annotations)?;
-                    let name = self.module.ns.get(instance.name_id());
-                    let instantiated = instance.instantiated();
-                    self.add_module(instantiated);
-                    let module_name = self.global_ns.get(instantiated.name_id());
-                    writeln!(
-                        body,
-                        "{indent}inst {name} of {module_name}{}",
-                        FileInfo::new(instance.source_location()),
-                    )
-                    .unwrap();
+                    writeln!(body, "{indent}{}", self.instance(instance)?).unwrap();
                 }
             }
             definitions.write_out(indent, &mut out);
@@ -2474,7 +2617,8 @@ impl<'a> Exporter<'a> {
         Ok(out)
     }
     fn module(&mut self, module: Interned<Module<Bundle>>) -> Result<String> {
-        self.module = ModuleState::default();
+        self.module = ModuleState::new(module);
+        let module_definitions = self.module.block_definitions.clone();
         let indent = self.indent;
         let module_name = self.global_ns.get(module.name_id());
         let mut body = String::new();
@@ -2543,12 +2687,10 @@ impl<'a> Exporter<'a> {
                 "extmodule"
             }
             ModuleBody::Normal(NormalModuleBody { body: top_block }) => {
-                body.push_str(&self.block(
-                    module,
-                    top_block,
-                    &module_indent,
-                    &BlockDefinitions::none(),
-                )?);
+                let body_str =
+                    self.block(module, top_block, &module_indent, &module_definitions)?;
+                module_definitions.write_out(indent, &mut body);
+                body.push_str(&body_str);
                 "module"
             }
         };
@@ -2895,7 +3037,7 @@ fn export_impl(
         seen_modules: HashSet::default(),
         unwritten_modules: VecDeque::new(),
         global_ns,
-        module: ModuleState::default(),
+        module: ModuleState::new(top_module),
         type_state: TypeState::default(),
         circuit_name,
         annotations: vec![],
diff --git a/crates/fayalite/src/formal.rs b/crates/fayalite/src/formal.rs
index 17d3122..77ef808 100644
--- a/crates/fayalite/src/formal.rs
+++ b/crates/fayalite/src/formal.rs
@@ -1,11 +1,189 @@
 // SPDX-License-Identifier: LGPL-3.0-or-later
 // See Notices.txt for copyright information
 use crate::{
+    expr::target::{GetTarget, Target},
     int::BoolOrIntType,
-    intern::{Intern, Interned, Memoize},
+    intern::{Intern, Interned},
+    module::{NameId, NameIdOrGlobal, ScopedNameId},
     prelude::*,
 };
-use std::sync::OnceLock;
+use std::{fmt, sync::OnceLock};
+
+#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
+pub enum FormalInputKind {
+    FormalGlobalClock,
+    FormalReset,
+    AnyConst,
+    AnySeq,
+    AllConst,
+    AllSeq,
+}
+
+impl FormalInputKind {
+    pub fn fixed_ty(self) -> Option<CanonicalType> {
+        match self {
+            Self::FormalGlobalClock => Some(Clock.into()),
+            Self::FormalReset => Some(SyncReset.into()),
+            Self::AnyConst => None,
+            Self::AnySeq => None,
+            Self::AllConst => None,
+            Self::AllSeq => None,
+        }
+    }
+    pub fn fixed_id(self) -> Option<crate::module::Id> {
+        struct Cache {
+            formal_global_clock: crate::module::Id,
+            formal_reset: crate::module::Id,
+        }
+        static CACHE: OnceLock<Cache> = OnceLock::new();
+        let cache = || {
+            CACHE.get_or_init(
+                #[cold]
+                || Cache {
+                    formal_global_clock: crate::module::Id::new(),
+                    formal_reset: crate::module::Id::new(),
+                },
+            )
+        };
+        match self {
+            Self::FormalGlobalClock => Some(cache().formal_global_clock),
+            Self::FormalReset => Some(cache().formal_reset),
+            Self::AnyConst => None,
+            Self::AnySeq => None,
+            Self::AllConst => None,
+            Self::AllSeq => None,
+        }
+    }
+    pub fn fixed_source_location(self) -> Option<SourceLocation> {
+        match self {
+            Self::FormalGlobalClock | Self::FormalReset => Some(SourceLocation::builtin()),
+            Self::AnyConst | Self::AnySeq | Self::AllConst | Self::AllSeq => None,
+        }
+    }
+    pub fn name(self) -> &'static str {
+        match self {
+            Self::FormalGlobalClock => "formal_global_clock",
+            Self::FormalReset => "formal_reset",
+            Self::AnyConst => "any_const",
+            Self::AnySeq => "any_seq",
+            Self::AllConst => "all_const",
+            Self::AllSeq => "all_seq",
+        }
+    }
+    pub fn interned_name(self) -> Interned<str> {
+        macro_rules! impl_interned_name {
+            ($($variant:ident,)*) => {
+                match self {
+                    $(Self::$variant => {
+                        static CACHE: OnceLock<Interned<str>> = OnceLock::new();
+                        *CACHE.get_or_init(|| Self::$variant.name().intern())
+                    })*
+                }
+            };
+        }
+        impl_interned_name! {
+            FormalGlobalClock,
+            FormalReset,
+            AnyConst,
+            AnySeq,
+            AllConst,
+            AllSeq,
+        }
+    }
+}
+
+#[derive(Clone, PartialEq, Eq, Hash)]
+struct FormalInputData {
+    kind: FormalInputKind,
+    name_id: NameId,
+    ty: CanonicalType,
+    source_location: SourceLocation,
+}
+
+#[derive(Copy, Clone, PartialEq, Eq, Hash)]
+pub struct FormalInput(Interned<FormalInputData>);
+
+impl fmt::Debug for FormalInput {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        if self.kind().fixed_ty().is_some() {
+            f.write_str(&self.name())
+        } else {
+            f.debug_tuple(&self.name()).field(&self.0.ty).finish()
+        }
+    }
+}
+
+impl FormalInput {
+    #[track_caller]
+    pub fn new(
+        kind: FormalInputKind,
+        name_id: NameId,
+        ty: CanonicalType,
+        source_location: SourceLocation,
+    ) -> Self {
+        let NameId(name, id) = name_id;
+        assert_eq!(kind.interned_name(), name);
+        if let Some(fixed_ty) = kind.fixed_ty() {
+            assert_eq!(ty, fixed_ty);
+        } else {
+            assert!(
+                ty.is_castable_from_bits(),
+                "{name} type must be castable from bits. got:\n{ty:#?}",
+            );
+        }
+        if let Some(fixed_source_location) = kind.fixed_source_location() {
+            assert_eq!(source_location, fixed_source_location);
+        }
+        if let Some(fixed_id) = kind.fixed_id() {
+            assert_eq!(id, fixed_id);
+        }
+        Self(
+            FormalInputData {
+                kind,
+                name_id,
+                ty,
+                source_location,
+            }
+            .intern_sized(),
+        )
+    }
+    pub fn kind(self) -> FormalInputKind {
+        self.0.kind
+    }
+    pub fn name(self) -> Interned<str> {
+        self.0.name_id.0
+    }
+    pub fn name_id(self) -> NameId {
+        self.0.name_id
+    }
+    pub fn scoped_name(self) -> ScopedNameId {
+        ScopedNameId(NameIdOrGlobal::Global, self.name_id())
+    }
+    pub fn source_location(self) -> SourceLocation {
+        self.0.source_location
+    }
+    pub(crate) fn must_connect_to(self) -> bool {
+        false
+    }
+    pub(crate) fn flow(self) -> crate::expr::Flow {
+        crate::expr::Flow::Source
+    }
+}
+
+impl ValueType for FormalInput {
+    type Type = CanonicalType;
+    type ValueCategory = crate::expr::value_category::ValueCategoryExpr;
+
+    fn ty(&self) -> Self::Type {
+        self.0.ty
+    }
+}
+
+impl GetTarget for FormalInput {
+    fn target(&self) -> Option<Interned<Target>> {
+        Some(Target::from(*self).intern_sized())
+    }
+}
 
 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
 pub enum FormalKind {
@@ -138,110 +316,76 @@ make_formal!(
     hdl_cover
 );
 
-pub trait MakeFormalExpr: Type {}
-
-impl<T: Type> MakeFormalExpr for T {}
-
 #[hdl]
 pub fn formal_global_clock() -> Expr<Clock> {
-    #[hdl_module(extern)]
-    fn formal_global_clock() {
-        #[hdl]
-        let clk: Clock = m.output();
-        m.annotate_module(BlackBoxInlineAnnotation {
-            path: "fayalite_formal_global_clock.v".intern(),
-            text: r"module __fayalite_formal_global_clock(output clk);
-    (* gclk *)
-    reg clk;
-endmodule
-"
-            .intern(),
-        });
-        m.verilog_name("__fayalite_formal_global_clock");
-    }
-    #[hdl]
-    let formal_global_clock = instance(formal_global_clock());
-    formal_global_clock.clk
+    static CACHE: OnceLock<Expr<Clock>> = OnceLock::new();
+    *CACHE.get_or_init(|| {
+        let kind = FormalInputKind::FormalGlobalClock;
+        Expr::from_canonical(
+            FormalInput::new(
+                kind,
+                NameId(
+                    kind.interned_name(),
+                    kind.fixed_id().expect("known to have a fixed Id"),
+                ),
+                Clock.into(),
+                kind.fixed_source_location()
+                    .expect("known to have a fixed SourceLocation"),
+            )
+            .to_expr(),
+        )
+    })
 }
 
 #[hdl]
 pub fn formal_reset() -> Expr<SyncReset> {
-    #[hdl_module(extern)]
-    fn formal_reset() {
-        #[hdl]
-        let rst: SyncReset = m.output();
-        m.annotate_module(BlackBoxInlineAnnotation {
-            path: "fayalite_formal_reset.v".intern(),
-            text: r"module __fayalite_formal_reset(output rst);
-    assign rst = $initstate;
-endmodule
-"
-            .intern(),
-        });
-        m.verilog_name("__fayalite_formal_reset");
-    }
-    static MOD: OnceLock<Interned<Module<formal_reset>>> = OnceLock::new();
-    #[hdl]
-    let formal_reset = instance(*MOD.get_or_init(formal_reset));
-    formal_reset.rst
+    static CACHE: OnceLock<Expr<SyncReset>> = OnceLock::new();
+    *CACHE.get_or_init(|| {
+        let kind = FormalInputKind::FormalReset;
+        Expr::from_canonical(
+            FormalInput::new(
+                kind,
+                NameId(
+                    kind.interned_name(),
+                    kind.fixed_id().expect("known to have a fixed Id"),
+                ),
+                SyncReset.into(),
+                kind.fixed_source_location()
+                    .expect("known to have a fixed SourceLocation"),
+            )
+            .to_expr(),
+        )
+    })
 }
 
 macro_rules! make_any_const_fn {
-    ($ident:ident, $verilog_attribute:literal) => {
+    ($ident:ident, $ident_with_loc:ident, $verilog_attribute:literal, $kind:ident) => {
+        #[track_caller]
         #[hdl]
         pub fn $ident<T: BoolOrIntType>(ty: T) -> Expr<T> {
-            #[hdl_module(extern)]
-            pub(super) fn $ident<T: BoolOrIntType>(ty: T) {
-                #[hdl]
-                let out: T = m.output(ty);
-                let width = ty.width();
-                let verilog_bitslice = if width == 1 {
-                    String::new()
-                } else {
-                    format!(" [{}:0]", width - 1)
-                };
-                m.annotate_module(BlackBoxInlineAnnotation {
-                    path: Intern::intern_owned(format!(
-                        "fayalite_{}_{width}.v",
-                        stringify!($ident),
-                    )),
-                    text: Intern::intern_owned(format!(
-                        r"module __fayalite_{}_{width}(output{verilog_bitslice} out);
-    (* {} *)
-    reg{verilog_bitslice} out;
-endmodule
-",
-                        stringify!($ident),
-                        $verilog_attribute,
-                    )),
-                });
-                m.verilog_name(format!("__fayalite_{}_{width}", stringify!($ident)));
-            }
-            #[derive(Copy, Clone, PartialEq, Eq, Hash)]
-            struct TheMemoize<T>(T);
-            impl<T: BoolOrIntType> Memoize for TheMemoize<T> {
-                type Input = ();
-                type InputOwned = ();
-                type Output = Option<Interned<Module<$ident<T>>>>;
-                fn inner(self, _input: &Self::Input) -> Self::Output {
-                    if self.0.width() == 0 {
-                        None
-                    } else {
-                        Some($ident(self.0))
-                    }
-                }
-            }
-            let Some(module) = TheMemoize(ty).get_owned(()) else {
-                return 0_hdl_u0.cast_bits_to(ty);
-            };
-            #[hdl]
-            let $ident = instance(module);
-            $ident.out
+            $ident_with_loc(ty, SourceLocation::caller())
+        }
+        #[track_caller]
+        #[hdl]
+        pub fn $ident_with_loc<T: BoolOrIntType>(
+            ty: T,
+            source_location: SourceLocation,
+        ) -> Expr<T> {
+            let kind = FormalInputKind::$kind;
+            Expr::from_canonical(
+                FormalInput::new(
+                    kind,
+                    NameId(kind.interned_name(), crate::module::Id::new()),
+                    ty.canonical(),
+                    source_location,
+                )
+                .to_expr(),
+            )
         }
     };
 }
 
-make_any_const_fn!(any_const, "anyconst");
-make_any_const_fn!(any_seq, "anyseq");
-make_any_const_fn!(all_const, "allconst");
-make_any_const_fn!(all_seq, "allseq");
+make_any_const_fn!(any_const, any_const_with_loc, "anyconst", AnyConst);
+make_any_const_fn!(any_seq, any_seq_with_loc, "anyseq", AnySeq);
+make_any_const_fn!(all_const, all_const_with_loc, "allconst", AllConst);
+make_any_const_fn!(all_seq, all_seq_with_loc, "allseq", AllSeq);
diff --git a/crates/fayalite/src/intern.rs b/crates/fayalite/src/intern.rs
index b78aa59..89cc53d 100644
--- a/crates/fayalite/src/intern.rs
+++ b/crates/fayalite/src/intern.rs
@@ -682,27 +682,62 @@ impl<T: ?Sized + 'static + Send + Sync + AsRef<U>, U: ?Sized> AsRef<U> for Inter
 
 #[derive(Clone, Debug)]
 pub struct InternedSliceIter<T: Clone + 'static + Send + Sync> {
-    slice: Interned<[T]>,
-    index: std::ops::Range<usize>,
+    iter: std::iter::Cloned<std::slice::Iter<'static, T>>,
+}
+
+impl<T: Clone + 'static + Send + Sync> Default for InternedSliceIter<T> {
+    fn default() -> Self {
+        Self {
+            iter: [].iter().cloned(),
+        }
+    }
 }
 
 impl<T: Clone + 'static + Send + Sync> Iterator for InternedSliceIter<T> {
     type Item = T;
 
     fn next(&mut self) -> Option<Self::Item> {
-        self.index.next().map(|index| self.slice[index].clone())
+        self.iter.next()
     }
 
     fn size_hint(&self) -> (usize, Option<usize>) {
-        self.index.size_hint()
+        self.iter.size_hint()
+    }
+
+    fn count(self) -> usize {
+        self.iter.count()
+    }
+
+    fn last(mut self) -> Option<Self::Item> {
+        self.next_back()
+    }
+
+    fn nth(&mut self, n: usize) -> Option<Self::Item> {
+        self.iter.nth(n)
+    }
+
+    fn fold<B, F>(self, init: B, f: F) -> B
+    where
+        F: FnMut(B, Self::Item) -> B,
+    {
+        self.iter.fold(init, f)
     }
 }
 
 impl<T: Clone + 'static + Send + Sync> DoubleEndedIterator for InternedSliceIter<T> {
     fn next_back(&mut self) -> Option<Self::Item> {
-        self.index
-            .next_back()
-            .map(|index| self.slice[index].clone())
+        self.iter.next_back()
+    }
+
+    fn nth_back(&mut self, n: usize) -> Option<Self::Item> {
+        self.iter.nth_back(n)
+    }
+
+    fn rfold<B, F>(self, init: B, f: F) -> B
+    where
+        F: FnMut(B, Self::Item) -> B,
+    {
+        self.iter.rfold(init, f)
     }
 }
 
@@ -716,8 +751,7 @@ impl<T: Clone + 'static + Send + Sync> IntoIterator for Interned<[T]> {
 
     fn into_iter(self) -> Self::IntoIter {
         InternedSliceIter {
-            index: 0..self.len(),
-            slice: self,
+            iter: Interned::into_inner(self).iter().cloned(),
         }
     }
 }
diff --git a/crates/fayalite/src/module.rs b/crates/fayalite/src/module.rs
index 86fdd40..2535694 100644
--- a/crates/fayalite/src/module.rs
+++ b/crates/fayalite/src/module.rs
@@ -727,7 +727,57 @@ impl fmt::Display for NameId {
 }
 
 #[derive(Copy, Clone, Eq, PartialEq, Hash)]
-pub struct ScopedNameId(pub NameId, pub NameId);
+pub enum NameIdOrGlobal {
+    Global,
+    NameId(NameId),
+}
+
+impl NameIdOrGlobal {
+    pub fn name_id(self) -> Option<NameId> {
+        match self {
+            Self::Global => None,
+            Self::NameId(v) => Some(v),
+        }
+    }
+    #[track_caller]
+    pub fn assert_is_name_id(self) {
+        match self {
+            Self::Global => panic!("expected a NameId, got NameIdOrGlobal::Global"),
+            Self::NameId(_) => {}
+        }
+    }
+    #[track_caller]
+    pub fn unwrap_name_id(self) -> NameId {
+        match self {
+            Self::Global => panic!("expected a NameId, got NameIdOrGlobal::Global"),
+            Self::NameId(v) => v,
+        }
+    }
+}
+
+impl fmt::Debug for NameIdOrGlobal {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        fmt::Display::fmt(self, f)
+    }
+}
+
+impl fmt::Display for NameIdOrGlobal {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Self::Global => f.write_str("<<Global>>"),
+            Self::NameId(name_id) => fmt::Display::fmt(name_id, f),
+        }
+    }
+}
+
+impl From<NameId> for NameIdOrGlobal {
+    fn from(value: NameId) -> Self {
+        Self::NameId(value)
+    }
+}
+
+#[derive(Copy, Clone, Eq, PartialEq, Hash)]
+pub struct ScopedNameId(pub NameIdOrGlobal, pub NameId);
 
 impl fmt::Debug for ScopedNameId {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
@@ -805,7 +855,7 @@ impl<T: BundleType> Instance<T> {
         self.containing_module_name_id().0
     }
     pub fn containing_module_name_id(self) -> NameId {
-        self.scoped_name.0
+        self.scoped_name.0.unwrap_name_id()
     }
     pub fn name(self) -> Interned<str> {
         self.name_id().0
@@ -822,11 +872,13 @@ impl<T: BundleType> Instance<T> {
     pub fn source_location(self) -> SourceLocation {
         self.source_location
     }
+    #[track_caller]
     pub fn new_unchecked(
         scoped_name: ScopedNameId,
         instantiated: Interned<Module<T>>,
         source_location: SourceLocation,
     ) -> Self {
+        scoped_name.0.assert_is_name_id();
         Self {
             scoped_name,
             instantiated,
@@ -1650,6 +1702,12 @@ struct AssertValidityState {
     target_states: HashMap<Interned<TargetBase>, TargetState>,
 }
 
+enum GetTargetStatesError {
+    NotFound,
+    IsGlobal,
+    FoundSimIoForGlobal(crate::expr::ops::SimIoForGlobal),
+}
+
 impl AssertValidityState {
     fn make_block_index(&mut self, block: Block) -> usize {
         let retval = self.blocks.len();
@@ -1660,7 +1718,7 @@ impl AssertValidityState {
         &'a self,
         target: Target,
         process_target_state: &dyn Fn(&'a TargetState, bool),
-    ) -> Result<(), ()> {
+    ) -> Result<(), GetTargetStatesError> {
         let mut target = target.unwrap_transparent_types();
         loop {
             break match target {
@@ -1713,8 +1771,24 @@ impl AssertValidityState {
             };
         }
     }
-    fn get_base_state(&self, target_base: Interned<TargetBase>) -> Result<&TargetState, ()> {
-        self.target_states.get(&target_base).ok_or(())
+    fn get_base_state(
+        &self,
+        target_base: Interned<TargetBase>,
+    ) -> Result<&TargetState, GetTargetStatesError> {
+        match *target_base {
+            TargetBase::ModuleIO(_)
+            | TargetBase::MemPort(_)
+            | TargetBase::Reg(_)
+            | TargetBase::RegSync(_)
+            | TargetBase::RegAsync(_)
+            | TargetBase::Wire(_)
+            | TargetBase::Instance(_) => self
+                .target_states
+                .get(&target_base)
+                .ok_or(GetTargetStatesError::NotFound),
+            TargetBase::FormalInput(_) => Err(GetTargetStatesError::IsGlobal),
+            TargetBase::SimIoForGlobal(v) => Err(GetTargetStatesError::FoundSimIoForGlobal(v)),
+        }
     }
     #[track_caller]
     fn insert_new_base(&mut self, target_base: Interned<TargetBase>, declared_in_block: usize) {
@@ -1807,13 +1881,26 @@ impl AssertValidityState {
         let result = self.get_target_states(*target, &|target_state, exact_target_unknown| {
             Self::set_connect_target_written(target_state, is_lhs, block, exact_target_unknown);
         });
-        if result.is_err() {
-            if is_lhs {
-                panic!("at {source_location}: tried to connect to not-yet-defined item: {target}");
-            } else {
+        match result {
+            Ok(()) => {}
+            Err(GetTargetStatesError::NotFound) => {
+                if is_lhs {
+                    panic!(
+                        "at {source_location}: tried to connect to not-yet-defined item: {target}"
+                    );
+                } else {
+                    panic!(
+                        "at {source_location}: tried to connect from not-yet-defined item: {target}"
+                    );
+                }
+            }
+            Err(GetTargetStatesError::IsGlobal) => {
+                // no error
+            }
+            Err(GetTargetStatesError::FoundSimIoForGlobal(v)) => {
                 panic!(
-                    "at {source_location}: tried to connect from not-yet-defined item: {target}"
-                );
+                    "at {source_location}: fayalite::expr::ops::SimIoForGlobal is not allowed in Modules: {v:?}"
+                )
             }
         }
     }
@@ -2118,7 +2205,8 @@ impl transform::visit::Visitor for AssertExprValidity<'_> {
             | ExprEnum::CastToBits(_)
             | ExprEnum::CastBitsTo(_)
             | ExprEnum::ToTraceAsString(_)
-            | ExprEnum::TraceAsStringAsInner(_) => v.default_visit(self),
+            | ExprEnum::TraceAsStringAsInner(_)
+            | ExprEnum::FormalInput(_) => v.default_visit(self),
             ExprEnum::VariantAccess(_)
             | ExprEnum::ModuleIO(_)
             | ExprEnum::Instance(_)
@@ -2134,6 +2222,7 @@ impl transform::visit::Visitor for AssertExprValidity<'_> {
                     Err(InvalidExpr::ExprIsNotVisible(v.to_expr()))
                 }
             }
+            ExprEnum::SimIoForGlobal(_) => Err(InvalidExpr::ExprIsNotVisible(v.to_expr())),
         }
     }
 }
@@ -2369,7 +2458,7 @@ impl<T: Type, R: ResetType> RegBuilder<Expr<ClockDomain<R>>, Option<Expr<T>>, T>
             ty,
         } = self;
         ModuleBuilder::with(|module_builder| {
-            let scoped_name = ScopedNameId(module_builder.name, NameId(name, Id::new()));
+            let scoped_name = ScopedNameId(module_builder.name.into(), NameId(name, Id::new()));
             let reg = Reg::new_unchecked(scoped_name, source_location, ty, clock_domain, init);
             let retval = reg.to_expr();
             // convert before borrow_mut since ModuleBuilder could be reentered by T::canonical()
@@ -2765,6 +2854,9 @@ pub fn annotate<T: Type>(target: Expr<T>, annotations: impl IntoAnnotations) {
             instance,
         }
         .into(),
+        TargetBase::FormalInput(_) | TargetBase::SimIoForGlobal(_) => {
+            unreachable!("not a valid annotation target")
+        }
     };
     ModuleBuilder::with(|m| {
         unwrap!(m.impl_.borrow_mut().body.builder_normal_body_opt())
@@ -2779,7 +2871,7 @@ pub fn annotate<T: Type>(target: Expr<T>, annotations: impl IntoAnnotations) {
 #[track_caller]
 pub fn wire_with_loc<T: Type>(name: &str, source_location: SourceLocation, ty: T) -> Expr<T> {
     ModuleBuilder::with(|m| {
-        let scoped_name = ScopedNameId(m.name, NameId(name.intern(), Id::new()));
+        let scoped_name = ScopedNameId(m.name.into(), NameId(name.intern(), Id::new()));
         let wire = Wire::<T>::new_unchecked(scoped_name, source_location, ty);
         let retval = wire.to_expr();
         let canonical_wire = wire.canonical();
@@ -2811,7 +2903,7 @@ fn incomplete_declaration(
     source_location: SourceLocation,
 ) -> Rc<RefCell<IncompleteDeclaration>> {
     ModuleBuilder::with(|m| {
-        let scoped_name = ScopedNameId(m.name, NameId(name.intern(), Id::new()));
+        let scoped_name = ScopedNameId(m.name.into(), NameId(name.intern(), Id::new()));
         let retval = Rc::new(RefCell::new(IncompleteDeclaration::Incomplete {
             name: scoped_name,
             source_location,
@@ -2987,7 +3079,7 @@ pub fn instance_with_loc<T: BundleType>(
     source_location: SourceLocation,
 ) -> Expr<T> {
     ModuleBuilder::with(|m| {
-        let scoped_name = ScopedNameId(m.name, NameId(name.intern(), Id::new()));
+        let scoped_name = ScopedNameId(m.name.into(), NameId(name.intern(), Id::new()));
         let instance = Instance::<T> {
             scoped_name,
             instantiated,
@@ -3026,7 +3118,7 @@ fn memory_impl<Element: Type, Len: Size>(
     source_location: SourceLocation,
 ) -> MemBuilder<Element, Len> {
     ModuleBuilder::with(|m| {
-        let scoped_name = ScopedNameId(m.name, NameId(name.intern(), Id::new()));
+        let scoped_name = ScopedNameId(m.name.into(), NameId(name.intern(), Id::new()));
         let (retval, target_mem) = MemBuilder::new(scoped_name, source_location, mem_element_type);
         let mut impl_ = m.impl_.borrow_mut();
         let body = impl_.body.builder_normal_body();
@@ -3181,7 +3273,7 @@ impl<T: Type> ModuleIO<T> {
         NameId(self.bundle_field.name, self.id)
     }
     pub fn scoped_name(&self) -> ScopedNameId {
-        ScopedNameId(self.containing_module_name, self.name_id())
+        ScopedNameId(self.containing_module_name.into(), self.name_id())
     }
     pub fn source_location(&self) -> SourceLocation {
         self.source_location
@@ -3254,10 +3346,102 @@ impl fmt::Debug for InstantiatedModule {
     }
 }
 
+#[derive(PartialEq, Eq, Hash, Clone, Copy)]
+pub enum InstantiatedModuleOrGlobal {
+    Global,
+    InstantiatedModule(InstantiatedModule),
+}
+
+impl InstantiatedModuleOrGlobal {
+    pub fn leaf_module_source_location(self) -> SourceLocation {
+        match self {
+            Self::Global => SourceLocation::builtin(),
+            Self::InstantiatedModule(v) => v.leaf_module().source_location(),
+        }
+    }
+}
+
+impl From<InstantiatedModule> for InstantiatedModuleOrGlobal {
+    fn from(value: InstantiatedModule) -> Self {
+        Self::InstantiatedModule(value)
+    }
+}
+
+impl fmt::Debug for InstantiatedModuleOrGlobal {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Self::Global => f.write_str("Global"),
+            Self::InstantiatedModule(v) => v.fmt(f),
+        }
+    }
+}
+
 #[derive(Debug, PartialEq, Eq, Hash, Clone, Copy)]
-pub struct TargetInInstantiatedModule {
-    pub instantiated_module: InstantiatedModule,
-    pub target: Target,
+pub struct TargetInInstantiatedModuleOrGlobal {
+    instantiated_module_or_global: InstantiatedModuleOrGlobal,
+    target: Target,
+}
+
+impl TargetInInstantiatedModuleOrGlobal {
+    #[track_caller]
+    pub fn new(instantiated_module_or_global: InstantiatedModuleOrGlobal, target: Target) -> Self {
+        match (
+            instantiated_module_or_global,
+            target.base().target_name().0.0,
+        ) {
+            (InstantiatedModuleOrGlobal::Global, NameIdOrGlobal::Global)
+            | (InstantiatedModuleOrGlobal::InstantiatedModule(_), NameIdOrGlobal::NameId(_)) => {
+                Self {
+                    instantiated_module_or_global,
+                    target,
+                }
+            }
+            (InstantiatedModuleOrGlobal::Global, NameIdOrGlobal::NameId(_))
+            | (InstantiatedModuleOrGlobal::InstantiatedModule(_), NameIdOrGlobal::Global) => {
+                panic!(
+                    "instantiated_module_or_global doesn't match target.base().target_name().0.0:\n\
+                    instantiated_module_or_global: {instantiated_module_or_global:?}\n\
+                    target: {target:?}"
+                )
+            }
+        }
+    }
+    #[track_caller]
+    pub fn from_target(
+        instantiated_module: impl Into<InstantiatedModuleOrGlobal>,
+        target: Target,
+    ) -> Self {
+        let instantiated_module = instantiated_module.into();
+        Self {
+            instantiated_module_or_global: match target.base().target_name().0.0 {
+                NameIdOrGlobal::Global => InstantiatedModuleOrGlobal::Global,
+                NameIdOrGlobal::NameId(name_id) => {
+                    let InstantiatedModuleOrGlobal::InstantiatedModule(instantiated_module) =
+                        instantiated_module
+                    else {
+                        panic!(
+                            "target is in a module, but no InstantiatedModule was provided: {target:#?}"
+                        );
+                    };
+                    assert_eq!(
+                        name_id,
+                        instantiated_module.leaf_module().name_id(),
+                        "target isn't contained in module:\n\
+                        target: {target:#?}\n\
+                        instantiated_module: {instantiated_module:?}",
+                    );
+                    InstantiatedModuleOrGlobal::InstantiatedModule(instantiated_module)
+                }
+            },
+            target,
+        }
+    }
+    pub fn instantiated_module_or_global(self) -> InstantiatedModuleOrGlobal {
+        self.instantiated_module_or_global
+    }
+    pub fn target(self) -> Target {
+        self.target
+    }
 }
 
 #[derive(Debug, PartialEq, Eq, Hash, Clone, Copy)]
diff --git a/crates/fayalite/src/module/transform/deduce_resets.rs b/crates/fayalite/src/module/transform/deduce_resets.rs
index 4595e84..611401b 100644
--- a/crates/fayalite/src/module/transform/deduce_resets.rs
+++ b/crates/fayalite/src/module/transform/deduce_resets.rs
@@ -1215,6 +1215,10 @@ impl<P: Pass> RunPass<P> for ExprEnum {
             ExprEnum::RegSync(expr) => reg_expr_run_pass(expr, pass_args),
             ExprEnum::RegAsync(expr) => reg_expr_run_pass(expr, pass_args),
             ExprEnum::MemPort(expr) => Ok(expr.run_pass(pass_args)?.map(ExprEnum::from)),
+            ExprEnum::FormalInput(expr) => Ok(expr.run_pass(pass_args)?.map(ExprEnum::from)),
+            ExprEnum::SimIoForGlobal(_) => {
+                unreachable!("Module is known to not contain SimIoForGlobal from validation")
+            }
         }
     }
 }
@@ -1932,6 +1936,7 @@ impl_run_pass_copy!([] SVAttributeAnnotation);
 impl_run_pass_copy!([] UInt);
 impl_run_pass_copy!([] usize);
 impl_run_pass_copy!([] FormalKind);
+impl_run_pass_copy!([] crate::formal::FormalInput);
 impl_run_pass_copy!([] PhantomConst);
 
 macro_rules! impl_run_pass_for_struct {
@@ -2248,6 +2253,12 @@ impl<P: Pass> RunPass<P> for TargetBase {
             &TargetBase::RegAsync(v) => v.into(),
             TargetBase::Wire(v) => return Ok(v.run_pass(pass_args)?.map(TargetBase::Wire)),
             TargetBase::Instance(v) => return Ok(v.run_pass(pass_args)?.map(TargetBase::Instance)),
+            TargetBase::FormalInput(v) => {
+                return Ok(v.run_pass(pass_args)?.map(TargetBase::FormalInput));
+            }
+            TargetBase::SimIoForGlobal(_) => {
+                unreachable!("Module is known to not contain SimIoForGlobal from validation")
+            }
         };
         Ok(reg.run_pass(pass_args)?.map(|reg| match reg {
             AnyReg::Reg(reg) => TargetBase::Reg(reg),
diff --git a/crates/fayalite/src/module/transform/simplify_enums.rs b/crates/fayalite/src/module/transform/simplify_enums.rs
index c52939c..280701d 100644
--- a/crates/fayalite/src/module/transform/simplify_enums.rs
+++ b/crates/fayalite/src/module/transform/simplify_enums.rs
@@ -101,7 +101,7 @@ struct ModuleState {
 
 impl ModuleState {
     fn gen_name(&mut self, name: &str) -> ScopedNameId {
-        ScopedNameId(self.module_name, NameId(name.intern(), Id::new()))
+        ScopedNameId(self.module_name.into(), NameId(name.intern(), Id::new()))
     }
 }
 
@@ -824,7 +824,9 @@ impl Folder for State {
             | ExprEnum::Wire(_)
             | ExprEnum::Reg(_)
             | ExprEnum::RegSync(_)
-            | ExprEnum::RegAsync(_) => op.default_fold(self)?,
+            | ExprEnum::RegAsync(_)
+            | ExprEnum::FormalInput(_)
+            | ExprEnum::SimIoForGlobal(_) => op.default_fold(self)?,
         };
         self.module_state_stack
             .last_mut()
diff --git a/crates/fayalite/src/module/transform/visit.rs b/crates/fayalite/src/module/transform/visit.rs
index 7b4cd2a..17fd88c 100644
--- a/crates/fayalite/src/module/transform/visit.rs
+++ b/crates/fayalite/src/module/transform/visit.rs
@@ -18,13 +18,13 @@ use crate::{
             TargetPathTraceAsStringInner,
         },
     },
-    formal::FormalKind,
+    formal::{FormalInput, FormalInputKind, FormalKind},
     int::{Bool, SIntType, SIntValue, Size, UIntType, UIntValue},
     intern::{Intern, Interned},
     memory::{Mem, MemPort, PortKind, PortName, PortType, ReadUnderWrite},
     module::{
         AnnotatedModuleIO, Block, BlockId, ExternModuleBody, ExternModuleParameter,
-        ExternModuleParameterValue, Instance, Module, ModuleBody, ModuleIO, NameId,
+        ExternModuleParameterValue, Instance, Module, ModuleBody, ModuleIO, NameId, NameIdOrGlobal,
         NormalModuleBody, ScopedNameId, Stmt, StmtConnect, StmtDeclaration, StmtFormal, StmtIf,
         StmtInstance, StmtMatch, StmtReg, StmtWire,
     },
@@ -482,4 +482,30 @@ impl<T: ?Sized + Visit<State>, State: ?Sized + Visitor> Visit<State> for &'_ mut
     }
 }
 
+impl<State: ?Sized + Visitor> Visit<State> for NameIdOrGlobal {
+    fn visit(&self, state: &mut State) -> Result<(), <State>::Error> {
+        state.visit_name_id_or_global(self)
+    }
+
+    fn default_visit(&self, state: &mut State) -> Result<(), <State>::Error> {
+        match self {
+            Self::Global => Ok(()),
+            Self::NameId(name_id) => name_id.visit(state),
+        }
+    }
+}
+
+impl<State: ?Sized + Folder> Fold<State> for NameIdOrGlobal {
+    fn fold(self, state: &mut State) -> Result<Self, <State>::Error> {
+        state.fold_name_id_or_global(self)
+    }
+
+    fn default_fold(self, state: &mut State) -> Result<Self, <State>::Error> {
+        match self {
+            Self::Global => Ok(Self::Global),
+            Self::NameId(name_id) => Ok(Self::NameId(name_id.fold(state)?)),
+        }
+    }
+}
+
 include!(concat!(env!("OUT_DIR"), "/visit.rs"));
diff --git a/crates/fayalite/src/prelude.rs b/crates/fayalite/src/prelude.rs
index 42038ca..69feeb5 100644
--- a/crates/fayalite/src/prelude.rs
+++ b/crates/fayalite/src/prelude.rs
@@ -16,8 +16,8 @@ pub use crate::{
         ReduceBits, ToExpr, ToTraceAsString, ValueType, repeat,
     },
     formal::{
-        MakeFormalExpr, all_const, all_seq, any_const, any_seq, formal_global_clock, formal_reset,
-        hdl_assert, hdl_assert_with_enable, hdl_assume, hdl_assume_with_enable, hdl_cover,
+        all_const, all_seq, any_const, any_seq, formal_global_clock, formal_reset, hdl_assert,
+        hdl_assert_with_enable, hdl_assume, hdl_assume_with_enable, hdl_cover,
         hdl_cover_with_enable,
     },
     hdl, hdl_module,
@@ -37,7 +37,7 @@ pub use crate::{
         value::{SimOnly, SimOnlyValue, SimValue, ToSimValue, ToSimValueWithType},
     },
     source_location::SourceLocation,
-    testing::{FormalMode, assert_formal},
+    testing::{FormalMode, assert_formal, checked_vcd_output},
     ty::{AsMask, CanonicalType, TraceAsString, Type},
     util::{ConstUsize, GenericConstUsize},
     wire::Wire,
diff --git a/crates/fayalite/src/reg.rs b/crates/fayalite/src/reg.rs
index 7f50655..2e4ab16 100644
--- a/crates/fayalite/src/reg.rs
+++ b/crates/fayalite/src/reg.rs
@@ -79,6 +79,7 @@ impl<T: Type, R: ResetType> Reg<T, R> {
         if let Some(init) = init {
             assert_eq!(ty, init.ty(), "register's type must match init type");
         }
+        scoped_name.0.assert_is_name_id();
         Self {
             name: scoped_name,
             source_location,
@@ -94,7 +95,7 @@ impl<T: Type, R: ResetType> Reg<T, R> {
         self.containing_module_name_id().0
     }
     pub fn containing_module_name_id(&self) -> NameId {
-        self.name.0
+        self.name.0.unwrap_name_id()
     }
     pub fn name(&self) -> Interned<str> {
         self.name_id().0
diff --git a/crates/fayalite/src/sim.rs b/crates/fayalite/src/sim.rs
index 1247fd8..b628d5b 100644
--- a/crates/fayalite/src/sim.rs
+++ b/crates/fayalite/src/sim.rs
@@ -6,15 +6,18 @@
 use crate::{
     bundle::{BundleField, BundleType},
     expr::{
-        Flow,
+        ExprEnum, Flow,
+        ops::SimIoForGlobal,
         target::{
-            GetTarget, Target, TargetPathArrayElement, TargetPathBundleField, TargetPathElement,
-            TargetPathTraceAsStringInner,
+            GetTarget, Target, TargetBase, TargetChild, TargetPathArrayElement,
+            TargetPathBundleField, TargetPathElement, TargetPathTraceAsStringInner,
         },
     },
+    formal::FormalInput,
     int::BoolOrIntType,
     intern::{
-        Intern, InternSlice, Interned, InternedCompare, PtrEqWithTypeId, SupportsPtrEqWithTypeId,
+        Intern, InternSlice, Interned, InternedCompare, InternedSliceIter, Memoize,
+        PtrEqWithTypeId, SupportsPtrEqWithTypeId,
     },
     module::{
         ModuleIO,
@@ -315,6 +318,14 @@ impl_trace_decl! {
             ty: CanonicalType,
             flow: Flow,
         }),
+        FormalInput(TraceFormalInput {
+            fn children(self) -> _ {
+                [*self.child].intern_slice()
+            }
+            name: Interned<str>,
+            child: Interned<TraceDecl>,
+            formal_input: FormalInput,
+        }),
         Bundle(TraceBundle {
             fn children(self) -> _ {
                 self.fields
@@ -1288,9 +1299,14 @@ impl SimulationModuleState {
     #[track_caller]
     fn get_io(
         &self,
-        mut target: Target,
-        which_module: WhichModule,
+        target: &mut Interned<Target>,
+        which_module: WhichModule<'_>,
     ) -> CompiledValue<CanonicalType> {
+        match which_module {
+            WhichModule::Main { global_io } => *target = global_io.to_sim_io_target(*target),
+            WhichModule::Extern { .. } => {}
+        }
+        let mut target = **target;
         assert!(
             target.canonical_ty().is_passive(),
             "simulator read/write expression must have a passive type \
@@ -1317,9 +1333,9 @@ impl SimulationModuleState {
             };
         }
         match which_module {
-            WhichModule::Main => panic!(
+            WhichModule::Main { .. } => panic!(
                 "simulator read/write expression must be \
-                an array element/field of `Simulation::io()`"
+                an array element/field of `Simulation::io()` or `Simulation::global_io()`"
             ),
             WhichModule::Extern { .. } => panic!(
                 "simulator read/write expression must be \
@@ -1329,18 +1345,18 @@ impl SimulationModuleState {
         }
     }
     #[track_caller]
-    fn is_reset_async(&self, io: Expr<CanonicalType>, which_module: WhichModule) -> bool {
-        let Some(target) = io.target() else {
+    fn is_reset_async(&self, io: Expr<CanonicalType>, which_module: WhichModule<'_>) -> bool {
+        let Some(mut target) = io.target() else {
             match which_module {
-                WhichModule::Main => panic!(
-                    "can't read from an expression that's not a field/element of `Simulation::io()`"
+                WhichModule::Main { .. } => panic!(
+                    "can't read from an expression that's not a field/element of `Simulation::io()` or `Simulation::global_io()`"
                 ),
                 WhichModule::Extern { .. } => panic!(
                     "can't read from an expression that's not based on one of this module's inputs/outputs"
                 ),
             }
         };
-        match self.get_io(*target, which_module).layout.ty {
+        match self.get_io(&mut target, which_module).layout.ty {
             CanonicalType::UInt(_)
             | CanonicalType::SInt(_)
             | CanonicalType::Bool(_)
@@ -1360,24 +1376,24 @@ impl SimulationModuleState {
     fn read_helper_current(
         &self,
         io: Expr<CanonicalType>,
-        which_module: WhichModule,
+        which_module: WhichModule<'_>,
     ) -> MaybeNeedsSettle<CompiledValue<CanonicalType>> {
-        let Some(target) = io.target() else {
+        let Some(mut target) = io.target() else {
             match which_module {
-                WhichModule::Main => panic!(
-                    "can't read from an expression that's not a field/element of `Simulation::io()`"
+                WhichModule::Main { .. } => panic!(
+                    "can't read from an expression that's not a field/element of `Simulation::io()` or `Simulation::global_io()`"
                 ),
                 WhichModule::Extern { .. } => panic!(
                     "can't read from an expression that's not based on one of this module's inputs/outputs"
                 ),
             }
         };
-        let compiled_value = self.get_io(*target, which_module);
+        let compiled_value = self.get_io(&mut target, which_module);
         match target.flow() {
             Flow::Source => {
                 if !self.uninitialized_ios.is_empty() {
                     match which_module {
-                        WhichModule::Main => {
+                        WhichModule::Main { .. } => {
                             panic!(
                                 "can't read from an output before initializing all inputs\nuninitialized_ios={:#?}",
                                 SortedSetDebug(&self.uninitialized_ios),
@@ -1396,7 +1412,9 @@ impl SimulationModuleState {
             Flow::Sink => {
                 if self.uninitialized_ios.contains_key(&*target) {
                     match which_module {
-                        WhichModule::Main => panic!("can't read from an uninitialized input"),
+                        WhichModule::Main { .. } => {
+                            panic!("can't read from an uninitialized input")
+                        }
                         WhichModule::Extern { .. } => {
                             panic!("can't read from an uninitialized output");
                         }
@@ -1412,7 +1430,7 @@ impl SimulationModuleState {
         &self,
         io: Expr<CanonicalType>,
         read_time: ReadTime,
-        which_module: WhichModule,
+        which_module: WhichModule<'_>,
     ) -> MaybeNeedsSettle<CompiledValue<CanonicalType>> {
         match read_time {
             ReadTime::Current => self.read_helper_current(io, which_module),
@@ -1438,22 +1456,22 @@ impl SimulationModuleState {
     fn write_helper(
         &mut self,
         io: Expr<CanonicalType>,
-        which_module: WhichModule,
+        which_module: WhichModule<'_>,
     ) -> CompiledValue<CanonicalType> {
-        let Some(target) = io.target() else {
+        let Some(mut target) = io.target() else {
             match which_module {
-                WhichModule::Main => panic!(
-                    "can't write to an expression that's not a field/element of `Simulation::io()`"
+                WhichModule::Main { .. } => panic!(
+                    "can't write to an expression that's not a field/element of `Simulation::io()` or `Simulation::global_io()`"
                 ),
                 WhichModule::Extern { .. } => panic!(
                     "can't write to an expression that's not based on one of this module's outputs"
                 ),
             }
         };
-        let compiled_value = self.get_io(*target, which_module);
+        let compiled_value = self.get_io(&mut target, which_module);
         match target.flow() {
             Flow::Source => match which_module {
-                WhichModule::Main => panic!("can't write to an output"),
+                WhichModule::Main { .. } => panic!("can't write to an output"),
                 WhichModule::Extern { .. } => panic!("can't write to an input"),
             },
             Flow::Sink => {}
@@ -1573,9 +1591,9 @@ impl fmt::Debug for SimulationExternModuleState {
     }
 }
 
-#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
-enum WhichModule {
-    Main,
+#[derive(Copy, Clone)]
+enum WhichModule<'a> {
+    Main { global_io: &'a SimulationGlobalIo },
     Extern { module_index: usize },
 }
 
@@ -1986,6 +2004,7 @@ impl SensitivitySet {
 struct SimulationImpl {
     state: interpreter::State,
     io: Expr<Bundle>,
+    global_io: SimulationGlobalIo,
     main_module: SimulationModuleState,
     extern_modules: Box<[SimulationExternModuleState]>,
     trace_decls: TraceModule,
@@ -2082,6 +2101,7 @@ impl SimulationImpl {
         let Self {
             state,
             io: self_io,
+            global_io,
             main_module,
             extern_modules,
             trace_decls,
@@ -2099,6 +2119,10 @@ impl SimulationImpl {
         f.debug_struct("Simulation")
             .field("state", state)
             .field("io", io.unwrap_or(self_io))
+            .field(
+                "global_io",
+                &fmt::from_fn(|f| f.debug_map().entries(global_io.global_io).finish()),
+            )
             .field("main_module", main_module)
             .field("extern_modules", extern_modules)
             .field("trace_decls", trace_decls)
@@ -2160,22 +2184,29 @@ impl SimulationImpl {
         Self {
             state: State::new(compiled.insns),
             io: compiled.io.to_expr(),
+            global_io: SimulationGlobalIo::new(compiled.global_io),
             main_module: SimulationModuleState::new(
                 compiled
-                    .io
-                    .ty()
-                    .fields()
-                    .into_iter()
-                    .zip(compiled.base_module.module_io)
-                    .map(|(BundleField { name, .. }, value)| {
-                        (
-                            io_target.join(
-                                TargetPathElement::from(TargetPathBundleField { name })
-                                    .intern_sized(),
-                            ),
-                            value,
-                        )
-                    }),
+                    .global_io
+                    .iter()
+                    .map(|&(global_io, value)| (global_io.into(), value))
+                    .chain(
+                        compiled
+                            .io
+                            .ty()
+                            .fields()
+                            .into_iter()
+                            .zip(compiled.base_module.module_io)
+                            .map(|(BundleField { name, .. }, value)| {
+                                (
+                                    io_target.join(
+                                        TargetPathElement::from(TargetPathBundleField { name })
+                                            .intern_sized(),
+                                    ),
+                                    value,
+                                )
+                            }),
+                    ),
                 &[],
             ),
             extern_modules,
@@ -2852,18 +2883,23 @@ impl SimulationImpl {
     fn settle(this_ref: &Rc<RefCell<Self>>) {
         Self::run_until(this_ref, &mut Some);
     }
-    fn get_module(&self, which_module: WhichModule) -> &SimulationModuleState {
+    fn get_module(&self, which_module: WhichModule<'_>) -> &SimulationModuleState {
         match which_module {
-            WhichModule::Main => &self.main_module,
+            WhichModule::Main { .. } => &self.main_module,
             WhichModule::Extern { module_index } => &self.extern_modules[module_index].module_state,
         }
     }
-    fn get_module_mut(&mut self, which_module: WhichModule) -> &mut SimulationModuleState {
+    fn get_module_mut_and_which_module(
+        &mut self,
+        which_module: impl for<'a> Fn(&'a SimulationGlobalIo) -> WhichModule<'a>,
+    ) -> (&mut SimulationModuleState, WhichModule<'_>) {
+        let which_module = which_module(&self.global_io);
         match which_module {
-            WhichModule::Main => &mut self.main_module,
-            WhichModule::Extern { module_index } => {
-                &mut self.extern_modules[module_index].module_state
-            }
+            WhichModule::Main { .. } => (&mut self.main_module, which_module),
+            WhichModule::Extern { module_index } => (
+                &mut self.extern_modules[module_index].module_state,
+                which_module,
+            ),
         }
     }
     #[track_caller]
@@ -2871,18 +2907,23 @@ impl SimulationImpl {
         &mut self,
         io: Expr<CanonicalType>,
         read_time: ReadTime,
-        which_module: WhichModule,
+        which_module: impl for<'a> Fn(&'a SimulationGlobalIo) -> WhichModule<'a>,
     ) -> MaybeNeedsSettle<ReadBitFn, bool> {
+        let which_module = which_module(&self.global_io);
         self.get_module(which_module)
             .read_helper(Expr::canonical(io), read_time, which_module)
             .map(|compiled_value| ReadBitFn { compiled_value })
             .apply_no_settle(&mut self.state)
     }
     #[track_caller]
-    fn write_bit(&mut self, io: Expr<CanonicalType>, value: bool, which_module: WhichModule) {
-        let compiled_value = self
-            .get_module_mut(which_module)
-            .write_helper(io, which_module);
+    fn write_bit(
+        &mut self,
+        io: Expr<CanonicalType>,
+        value: bool,
+        which_module: impl for<'a> Fn(&'a SimulationGlobalIo) -> WhichModule<'a>,
+    ) {
+        let (module, which_module) = self.get_module_mut_and_which_module(which_module);
+        let compiled_value = module.write_helper(io, which_module);
         self.event_queue.add_event_for_now(EventKind::State);
         match compiled_value.range.len().as_single() {
             Some(TypeLenSingle::SmallSlot) => {
@@ -2900,8 +2941,9 @@ impl SimulationImpl {
         &mut self,
         io: Expr<I>,
         read_time: ReadTime,
-        which_module: WhichModule,
+        which_module: impl for<'a> Fn(&'a SimulationGlobalIo) -> WhichModule<'a>,
     ) -> MaybeNeedsSettle<ReadBoolOrIntFn<I>, I::Value> {
+        let which_module = which_module(&self.global_io);
         self.get_module(which_module)
             .read_helper(Expr::canonical(io), read_time, which_module)
             .map(|compiled_value| ReadBoolOrIntFn { compiled_value, io })
@@ -2912,11 +2954,10 @@ impl SimulationImpl {
         &mut self,
         io: Expr<I>,
         value: I::Value,
-        which_module: WhichModule,
+        which_module: impl for<'a> Fn(&'a SimulationGlobalIo) -> WhichModule<'a>,
     ) {
-        let compiled_value = self
-            .get_module_mut(which_module)
-            .write_helper(Expr::canonical(io), which_module);
+        let (module, which_module) = self.get_module_mut_and_which_module(which_module);
+        let compiled_value = module.write_helper(Expr::canonical(io), which_module);
         self.event_queue.add_event_for_now(EventKind::State);
         let value: BigInt = value.into();
         match compiled_value.range.len().as_single() {
@@ -3148,7 +3189,12 @@ impl SimulationImpl {
         any_change.get()
     }
     #[track_caller]
-    fn is_reset_async(&self, io: Expr<CanonicalType>, which_module: WhichModule) -> bool {
+    fn is_reset_async(
+        &self,
+        io: Expr<CanonicalType>,
+        which_module: impl for<'a> Fn(&'a SimulationGlobalIo) -> WhichModule<'a>,
+    ) -> bool {
+        let which_module = which_module(&self.global_io);
         self.get_module(which_module)
             .is_reset_async(io, which_module)
     }
@@ -3157,11 +3203,12 @@ impl SimulationImpl {
         &mut self,
         io: Expr<CanonicalType>,
         read_time: ReadTime,
-        which_module: WhichModule,
+        which_module: impl for<'a> Fn(&'a SimulationGlobalIo) -> WhichModule<'a>,
     ) -> (
         CompiledValue<CanonicalType>,
         MaybeNeedsSettle<ReadFn, SimValue<CanonicalType>>,
     ) {
+        let which_module = which_module(&self.global_io);
         let compiled_value = self
             .get_module(which_module)
             .read_helper(io, read_time, which_module);
@@ -3189,11 +3236,10 @@ impl SimulationImpl {
         &mut self,
         io: Expr<CanonicalType>,
         value: &SimValue<CanonicalType>,
-        which_module: WhichModule,
+        which_module: impl for<'a> Fn(&'a SimulationGlobalIo) -> WhichModule<'a>,
     ) {
-        let compiled_value = self
-            .get_module_mut(which_module)
-            .write_helper(io, which_module);
+        let (module, which_module) = self.get_module_mut_and_which_module(which_module);
+        let compiled_value = module.write_helper(io, which_module);
         self.event_queue.add_event_for_now(EventKind::State);
         assert_eq!(io.ty(), value.ty());
         Self::read_write_sim_value_helper(
@@ -3370,6 +3416,318 @@ impl Drop for SimulationImpl {
     }
 }
 
+#[derive(Clone)]
+pub struct SimulationGlobalIo {
+    global_io: Interned<[(SimIoForGlobal, CompiledValue<CanonicalType>)]>,
+    global_io_map: Rc<HashMap<SimIoForGlobal, usize>>,
+}
+
+impl Default for SimulationGlobalIo {
+    fn default() -> Self {
+        Self {
+            global_io: Interned::default(),
+            global_io_map: Rc::default(),
+        }
+    }
+}
+
+impl fmt::Debug for SimulationGlobalIo {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.debug_map().entries(self.global_io).finish()
+    }
+}
+
+impl SimulationGlobalIo {
+    fn new(global_io: Interned<[(SimIoForGlobal, CompiledValue<CanonicalType>)]>) -> Self {
+        Self {
+            global_io,
+            global_io_map: Rc::new(HashMap::from_iter(
+                global_io
+                    .iter()
+                    .enumerate()
+                    .map(|(index, &(global, _))| (global, index)),
+            )),
+        }
+    }
+    #[must_use]
+    pub fn iter(&self) -> SimulationGlobalIoIter {
+        SimulationGlobalIoIter {
+            global_io: self.global_io.into_iter(),
+        }
+    }
+    #[must_use]
+    pub fn globals(&self) -> SimulationGlobalIoGlobalsIter {
+        SimulationGlobalIoGlobalsIter {
+            global_io: self.global_io.into_iter(),
+        }
+    }
+    #[must_use]
+    pub fn exprs(&self) -> SimulationGlobalIoExprsIter {
+        SimulationGlobalIoExprsIter {
+            global_io: self.global_io.into_iter(),
+        }
+    }
+    #[must_use]
+    pub fn len(&self) -> usize {
+        self.global_io.len()
+    }
+    #[must_use]
+    pub fn is_empty(&self) -> bool {
+        self.len() == 0
+    }
+    #[must_use]
+    pub fn contains(&self, global: FormalInput) -> bool {
+        self.global_io_map
+            .contains_key(&SimIoForGlobal::new(global))
+    }
+    #[must_use]
+    pub fn get(&self, global: FormalInput) -> Option<Expr<CanonicalType>> {
+        self.contains(global)
+            .then(|| SimIoForGlobal::new(global).to_expr())
+    }
+    #[must_use]
+    pub fn expr_to_global(&self, expr: Expr<CanonicalType>) -> Option<FormalInput> {
+        let global = match *Expr::expr_enum(expr) {
+            ExprEnum::FormalInput(global) => global,
+            ExprEnum::SimIoForGlobal(expr) => expr.global(),
+            _ => return None,
+        };
+        self.global_io_map
+            .contains_key(&SimIoForGlobal::new(global))
+            .then_some(global)
+    }
+    #[must_use]
+    fn to_sim_io_target(&self, target: Interned<Target>) -> Interned<Target> {
+        #[derive(Copy, Clone, PartialEq, Eq, Hash)]
+        struct FormalInputExprToSimIoExpr;
+        impl Memoize for FormalInputExprToSimIoExpr {
+            type Input = Interned<Target>;
+            type InputOwned = Interned<Target>;
+            type Output = Interned<Target>;
+
+            fn inner(self, input: &Self::Input) -> Self::Output {
+                match **input {
+                    Target::Base(base) => match *base {
+                        TargetBase::ModuleIO(_)
+                        | TargetBase::MemPort(_)
+                        | TargetBase::Reg(_)
+                        | TargetBase::RegSync(_)
+                        | TargetBase::RegAsync(_)
+                        | TargetBase::Wire(_)
+                        | TargetBase::Instance(_)
+                        | TargetBase::SimIoForGlobal(_) => *input,
+                        TargetBase::FormalInput(global) => {
+                            Target::from(SimIoForGlobal::new(global)).intern()
+                        }
+                    },
+                    Target::Child(child) => Target::Child(TargetChild::new(
+                        self.get_owned(child.parent()),
+                        child.path_element(),
+                    ))
+                    .intern_sized(),
+                }
+            }
+        }
+        match *target.base() {
+            TargetBase::ModuleIO(_)
+            | TargetBase::MemPort(_)
+            | TargetBase::Reg(_)
+            | TargetBase::RegSync(_)
+            | TargetBase::RegAsync(_)
+            | TargetBase::Wire(_)
+            | TargetBase::Instance(_)
+            | TargetBase::SimIoForGlobal(_) => target,
+            TargetBase::FormalInput(global) => {
+                if self.contains(global) {
+                    FormalInputExprToSimIoExpr.get_owned(target)
+                } else {
+                    target
+                }
+            }
+        }
+    }
+}
+
+impl IntoIterator for SimulationGlobalIo {
+    type Item = (FormalInput, Expr<CanonicalType>);
+    type IntoIter = SimulationGlobalIoIter;
+
+    fn into_iter(self) -> Self::IntoIter {
+        self.iter()
+    }
+}
+
+impl IntoIterator for &'_ SimulationGlobalIo {
+    type Item = (FormalInput, Expr<CanonicalType>);
+    type IntoIter = SimulationGlobalIoIter;
+
+    fn into_iter(self) -> Self::IntoIter {
+        self.iter()
+    }
+}
+
+impl IntoIterator for &'_ mut SimulationGlobalIo {
+    type Item = (FormalInput, Expr<CanonicalType>);
+    type IntoIter = SimulationGlobalIoIter;
+
+    fn into_iter(self) -> Self::IntoIter {
+        self.iter()
+    }
+}
+
+macro_rules! make_simulation_global_io_iter {
+    (
+        impl $SimulationGlobalIoIter:ident {
+            fn $global_io_to_item:ident(
+                $global_io_to_item_arg:ident: (SimIoForGlobal, CompiledValue<CanonicalType>),
+            ) -> $item_ty:ty
+            $global_io_to_item_block:block
+        }
+    ) => {
+        #[derive(Clone, Default)]
+        pub struct $SimulationGlobalIoIter {
+            global_io: InternedSliceIter<(SimIoForGlobal, CompiledValue<CanonicalType>)>,
+        }
+
+        impl $SimulationGlobalIoIter {
+            fn $global_io_to_item(
+                $global_io_to_item_arg: (SimIoForGlobal, CompiledValue<CanonicalType>),
+            ) -> $item_ty
+            $global_io_to_item_block
+        }
+
+        impl Iterator for $SimulationGlobalIoIter {
+            type Item = $item_ty;
+
+            fn next(&mut self) -> Option<Self::Item> {
+                self.global_io.next().map(Self::global_io_to_item)
+            }
+
+            fn size_hint(&self) -> (usize, Option<usize>) {
+                self.global_io.size_hint()
+            }
+
+            fn count(self) -> usize {
+                self.global_io.count()
+            }
+
+            fn last(mut self) -> Option<Self::Item> {
+                self.next_back()
+            }
+
+            fn nth(&mut self, n: usize) -> Option<Self::Item> {
+                self.global_io.nth(n).map(Self::global_io_to_item)
+            }
+
+            fn fold<B, F>(self, init: B, f: F) -> B
+            where
+                F: FnMut(B, Self::Item) -> B,
+            {
+                self.global_io.map(Self::global_io_to_item).fold(init, f)
+            }
+        }
+
+        impl std::iter::FusedIterator for $SimulationGlobalIoIter {}
+
+        impl DoubleEndedIterator for $SimulationGlobalIoIter {
+            fn next_back(&mut self) -> Option<Self::Item> {
+                self.global_io.next_back().map(Self::global_io_to_item)
+            }
+
+            fn nth_back(&mut self, n: usize) -> Option<Self::Item> {
+                self.global_io.nth_back(n).map(Self::global_io_to_item)
+            }
+
+            fn rfold<B, F>(self, init: B, f: F) -> B
+            where
+                F: FnMut(B, Self::Item) -> B,
+            {
+                self.global_io.map(Self::global_io_to_item).rfold(init, f)
+            }
+        }
+
+        impl ExactSizeIterator for $SimulationGlobalIoIter {}
+    };
+}
+
+make_simulation_global_io_iter! {
+    impl SimulationGlobalIoIter {
+        fn global_io_to_item(
+            v: (SimIoForGlobal, CompiledValue<CanonicalType>),
+        ) -> (FormalInput, Expr<CanonicalType>) {
+            let (global, _) = v;
+            (global.global(), global.to_expr())
+        }
+    }
+}
+
+impl SimulationGlobalIoIter {
+    #[must_use]
+    pub fn globals(self) -> SimulationGlobalIoGlobalsIter {
+        SimulationGlobalIoGlobalsIter {
+            global_io: self.global_io,
+        }
+    }
+    #[must_use]
+    pub fn exprs(self) -> SimulationGlobalIoExprsIter {
+        SimulationGlobalIoExprsIter {
+            global_io: self.global_io,
+        }
+    }
+}
+
+impl fmt::Debug for SimulationGlobalIoIter {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.debug_tuple("SimulationGlobalIoIter")
+            .field(&fmt::from_fn(|f| {
+                f.debug_map().entries(self.clone()).finish()
+            }))
+            .finish()
+    }
+}
+
+make_simulation_global_io_iter! {
+    impl SimulationGlobalIoGlobalsIter {
+        fn global_io_to_item(
+            v: (SimIoForGlobal, CompiledValue<CanonicalType>),
+        ) -> FormalInput {
+            let (global, _) = v;
+            global.global()
+        }
+    }
+}
+
+impl fmt::Debug for SimulationGlobalIoGlobalsIter {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.debug_tuple("SimulationGlobalIoGlobalsIter")
+            .field(&fmt::from_fn(|f| {
+                f.debug_set().entries(self.clone()).finish()
+            }))
+            .finish()
+    }
+}
+
+make_simulation_global_io_iter! {
+    impl SimulationGlobalIoExprsIter {
+        fn global_io_to_item(
+            v: (SimIoForGlobal, CompiledValue<CanonicalType>),
+        ) -> Expr<CanonicalType> {
+            let (global, _) = v;
+            global.to_expr()
+        }
+    }
+}
+
+impl fmt::Debug for SimulationGlobalIoExprsIter {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.debug_tuple("SimulationGlobalIoExprsIter")
+            .field(&fmt::from_fn(|f| {
+                f.debug_set().entries(self.clone()).finish()
+            }))
+            .finish()
+    }
+}
+
 pub struct Simulation<T: BundleType> {
     sim_impl: Rc<RefCell<SimulationImpl>>,
     io: Expr<T>,
@@ -3444,14 +3802,15 @@ macro_rules! impl_simulation_methods {
     (
         async_await = ($($async:tt, $await:tt)?),
         track_caller = ($(#[$track_caller:tt])?),
-        which_module = |$self:ident| $which_module:expr,
+        which_module = |$self:ident, $global_io:ident| $which_module:expr,
     ) => {
         $(#[$track_caller])?
         pub $($async)? fn read_bool_or_int<I: BoolOrIntType>(&mut $self, io: Expr<I>) -> I::Value {
-            let retval = $self
-                .sim_impl
-                .borrow_mut()
-                .read_bool_or_int(io, ReadTime::Current, $which_module);
+            let retval = $self.sim_impl.borrow_mut().read_bool_or_int(
+                io,
+                ReadTime::Current,
+                |$global_io: &SimulationGlobalIo| $which_module,
+            );
             $self.settle_if_needed(retval)$(.$await)?
         }
         $(#[$track_caller])?
@@ -3464,64 +3823,74 @@ macro_rules! impl_simulation_methods {
             $self.sim_impl.borrow_mut().write_bool_or_int(
                 io,
                 SimValue::into_value(value),
-                $which_module,
+                |$global_io: &SimulationGlobalIo| $which_module,
             );
         }
         $(#[$track_caller])?
         pub $($async)? fn write_clock(&mut $self, io: Expr<Clock>, value: bool) {
-            $self.sim_impl
-                .borrow_mut()
-                .write_bit(Expr::canonical(io), value, $which_module);
+            $self.sim_impl.borrow_mut().write_bit(
+                Expr::canonical(io),
+                value,
+                |$global_io: &SimulationGlobalIo| $which_module,
+            );
         }
         $(#[$track_caller])?
         pub $($async)? fn read_clock(&mut $self, io: Expr<Clock>) -> bool {
-            let retval = $self
-                .sim_impl
-                .borrow_mut()
-                .read_bit(Expr::canonical(io), ReadTime::Current, $which_module);
+            let retval = $self.sim_impl.borrow_mut().read_bit(
+                Expr::canonical(io),
+                ReadTime::Current,
+                |$global_io: &SimulationGlobalIo| $which_module,
+            );
             $self.settle_if_needed(retval)$(.$await)?
         }
         $(#[$track_caller])?
         pub $($async)? fn write_bool(&mut $self, io: Expr<Bool>, value: bool) {
-            $self.sim_impl
-                .borrow_mut()
-                .write_bit(Expr::canonical(io), value, $which_module);
+            $self.sim_impl.borrow_mut().write_bit(
+                Expr::canonical(io),
+                value,
+                |$global_io: &SimulationGlobalIo| $which_module,
+            );
         }
         $(#[$track_caller])?
         pub $($async)? fn read_bool(&mut $self, io: Expr<Bool>) -> bool {
-            let retval = $self
-                .sim_impl
-                .borrow_mut()
-                .read_bit(Expr::canonical(io), ReadTime::Current, $which_module);
+            let retval = $self.sim_impl.borrow_mut().read_bit(
+                Expr::canonical(io),
+                ReadTime::Current,
+                |$global_io: &SimulationGlobalIo| $which_module,
+            );
             $self.settle_if_needed(retval)$(.$await)?
         }
         $(#[$track_caller])?
         pub $($async)? fn write_reset<R: ResetType>(&mut $self, io: Expr<R>, value: bool) {
-            $self.sim_impl
-                .borrow_mut()
-                .write_bit(Expr::canonical(io), value, $which_module);
+            $self.sim_impl.borrow_mut().write_bit(
+                Expr::canonical(io),
+                value,
+                |$global_io: &SimulationGlobalIo| $which_module,
+            );
         }
         $(#[$track_caller])?
         pub $($async)? fn read_reset<R: ResetType>(&mut $self, io: Expr<R>) -> bool {
-            let retval = $self
-                .sim_impl
-                .borrow_mut()
-                .read_bit(Expr::canonical(io), ReadTime::Current, $which_module);
+            let retval = $self.sim_impl.borrow_mut().read_bit(
+                Expr::canonical(io),
+                ReadTime::Current,
+                |$global_io: &SimulationGlobalIo| $which_module,
+            );
             $self.settle_if_needed(retval)$(.$await)?
         }
         #[track_caller]
         pub fn is_reset_async<R: ResetType>(&$self, io: Expr<R>) -> bool {
-            $self
-                .sim_impl
-                .borrow_mut()
-                .is_reset_async(Expr::canonical(io), $which_module)
+            $self.sim_impl.borrow().is_reset_async(
+                Expr::canonical(io),
+                |$global_io: &SimulationGlobalIo| $which_module,
+            )
         }
         $(#[$track_caller])?
         pub $($async)? fn read<IO: Type>(&mut $self, io: Expr<IO>) -> SimValue<IO> {
-            let retval = $self
-                .sim_impl
-                .borrow_mut()
-                .read(Expr::canonical(io), ReadTime::Current, $which_module).1;
+            let retval = $self.sim_impl.borrow_mut().read(
+                Expr::canonical(io),
+                ReadTime::Current,
+                |$global_io: &SimulationGlobalIo| $which_module,
+            ).1;
             SimValue::from_canonical($self.settle_if_needed(retval)$(.$await)?)
         }
         $(#[$track_caller])?
@@ -3529,7 +3898,7 @@ macro_rules! impl_simulation_methods {
             $self.sim_impl.borrow_mut().write(
                 Expr::canonical(io),
                 &SimValue::into_canonical(value.into_sim_value_with_type(io.ty())),
-                $which_module,
+                |$global_io: &SimulationGlobalIo| $which_module,
             );
         }
     };
@@ -3568,6 +3937,9 @@ impl<T: BundleType> Simulation<T> {
     pub fn io(&self) -> Expr<T> {
         self.io.to_expr()
     }
+    pub fn global_io(&self) -> SimulationGlobalIo {
+        self.sim_impl.borrow().global_io.clone()
+    }
     pub fn from_compiled(compiled: Compiled<T>) -> Self {
         let sim_impl = SimulationImpl::new(compiled.canonical());
         Self {
@@ -3593,7 +3965,7 @@ impl<T: BundleType> Simulation<T> {
     impl_simulation_methods!(
         async_await = (),
         track_caller = (#[track_caller]),
-        which_module = |self| WhichModule::Main,
+        which_module = |self, global_io| WhichModule::Main { global_io },
     );
     #[doc(hidden)]
     /// This is explicitly unstable and may be changed/removed at any time
@@ -3662,7 +4034,7 @@ impl ExternModuleSimulationState {
             let (key, value) = self
                 .sim_impl
                 .borrow_mut()
-                .read(io, ReadTime::Current, which_module);
+                .read(io, ReadTime::Current, |_| which_module);
             let value = self.settle_if_needed(value).await;
             let key = Rc::new(key);
             if sensitivity_set.compiled_values.insert(key.clone()) {
@@ -3934,7 +4306,7 @@ impl ExternModuleSimulationState {
         let retval = self.sim_impl.borrow_mut().read_bool_or_int(
             io,
             ReadTime::Past { clock_for_past },
-            WhichModule::Extern {
+            |_| WhichModule::Extern {
                 module_index: self.module_index,
             },
         );
@@ -3950,7 +4322,7 @@ impl ExternModuleSimulationState {
         let retval = self.sim_impl.borrow_mut().read_bit(
             Expr::canonical(io),
             ReadTime::Past { clock_for_past },
-            WhichModule::Extern {
+            |_| WhichModule::Extern {
                 module_index: self.module_index,
             },
         );
@@ -3966,7 +4338,7 @@ impl ExternModuleSimulationState {
         let retval = self.sim_impl.borrow_mut().read_bit(
             Expr::canonical(io),
             ReadTime::Past { clock_for_past },
-            WhichModule::Extern {
+            |_| WhichModule::Extern {
                 module_index: self.module_index,
             },
         );
@@ -3986,7 +4358,7 @@ impl ExternModuleSimulationState {
         let retval = self.sim_impl.borrow_mut().read_bit(
             Expr::canonical(io),
             ReadTime::Past { clock_for_past },
-            WhichModule::Extern {
+            |_| WhichModule::Extern {
                 module_index: self.module_index,
             },
         );
@@ -4009,7 +4381,7 @@ impl ExternModuleSimulationState {
             .read(
                 Expr::canonical(io),
                 ReadTime::Past { clock_for_past },
-                WhichModule::Extern {
+                |_| WhichModule::Extern {
                     module_index: self.module_index,
                 },
             )
@@ -4019,7 +4391,7 @@ impl ExternModuleSimulationState {
     impl_simulation_methods!(
         async_await = (async, await),
         track_caller = (),
-        which_module = |self| WhichModule::Extern { module_index: self.module_index },
+        which_module = |self, _global_io| WhichModule::Extern { module_index: self.module_index },
     );
 }
 
diff --git a/crates/fayalite/src/sim/compiler.rs b/crates/fayalite/src/sim/compiler.rs
index 4d6d9bc..4c4cfab 100644
--- a/crates/fayalite/src/sim/compiler.rs
+++ b/crates/fayalite/src/sim/compiler.rs
@@ -7,7 +7,8 @@ use crate::{
     bundle::{BundleField, BundleType},
     enum_::{EnumType, EnumVariant},
     expr::{
-        ExprEnum, Flow, ValueType, ops,
+        ExprEnum, Flow, ValueType,
+        ops::{self, SimIoForGlobal},
         target::{
             GetTarget, Target, TargetBase, TargetPathArrayElement, TargetPathBundleField,
             TargetPathElement, TargetPathToTraceAsString, TargetPathTraceAsStringInner,
@@ -17,20 +18,20 @@ use crate::{
     intern::{Intern, InternSlice, Interned, Memoize},
     memory::PortKind,
     module::{
-        AnnotatedModuleIO, Block, ExternModuleBody, Id, InstantiatedModule, ModuleBody, NameId,
-        NormalModuleBody, ScopedNameId, Stmt, StmtConnect, StmtDeclaration, StmtFormal, StmtIf,
-        StmtInstance, StmtMatch, StmtReg, StmtWire, TargetInInstantiatedModule,
-        transform::deduce_resets::deduce_resets,
+        AnnotatedModuleIO, Block, ExternModuleBody, Id, InstantiatedModule,
+        InstantiatedModuleOrGlobal, ModuleBody, NameId, NormalModuleBody, ScopedNameId, Stmt,
+        StmtConnect, StmtDeclaration, StmtFormal, StmtIf, StmtInstance, StmtMatch, StmtReg,
+        StmtWire, TargetInInstantiatedModuleOrGlobal, transform::deduce_resets::deduce_resets,
     },
     prelude::*,
     reset::{ResetType, ResetTypeDispatch},
     sim::{
         ExternModuleSimulation, SimTrace, SimTraceKind, SimTraces, TraceArray, TraceAsyncReset,
         TraceBool, TraceBundle, TraceClock, TraceDecl, TraceEnumDiscriminant, TraceEnumWithFields,
-        TraceFieldlessEnum, TraceInstance, TraceLocation, TraceMem, TraceMemPort, TraceMemoryId,
-        TraceMemoryLocation, TraceModule, TraceModuleIO, TracePhantomConst, TraceReg, TraceSInt,
-        TraceScalarId, TraceScope, TraceSimOnly, TraceSyncReset, TraceTraceAsString, TraceUInt,
-        TraceWire,
+        TraceFieldlessEnum, TraceFormalInput, TraceInstance, TraceLocation, TraceMem, TraceMemPort,
+        TraceMemoryId, TraceMemoryLocation, TraceModule, TraceModuleIO, TracePhantomConst,
+        TraceReg, TraceSInt, TraceScalarId, TraceScope, TraceSimOnly, TraceSyncReset,
+        TraceTraceAsString, TraceUInt, TraceWire,
         interpreter::{
             self, Insn, InsnField, InsnFieldKind, InsnFieldType, InsnOrLabel, Insns, InsnsBuilding,
             InsnsBuildingDone, InsnsBuildingKind, Label, PrefixLinesWrapper, SmallUInt,
@@ -44,7 +45,7 @@ use crate::{
         },
     },
     ty::{OpaqueSimValueSize, StaticType, TraceAsString},
-    util::{HashMap, chain},
+    util::{HashMap, HashSet, chain},
 };
 use bitvec::vec::BitVec;
 use num_bigint::BigInt;
@@ -1802,10 +1803,10 @@ pub struct Compiler {
     base_module: Interned<Module<Bundle>>,
     modules: HashMap<InstantiatedModule, CompiledModule>,
     extern_modules: Vec<CompiledExternModule>,
-    compiled_values: HashMap<TargetInInstantiatedModule, CompiledValue<CanonicalType>>,
+    compiled_values: HashMap<TargetInInstantiatedModuleOrGlobal, CompiledValue<CanonicalType>>,
     compiled_exprs: HashMap<Expr<CanonicalType>, CompiledExpr<CanonicalType>>,
     compiled_exprs_to_values: HashMap<CompiledExpr<CanonicalType>, CompiledValue<CanonicalType>>,
-    decl_conditions: HashMap<TargetInInstantiatedModule, Interned<[Cond]>>,
+    decl_conditions: HashMap<TargetInInstantiatedModuleOrGlobal, Interned<[Cond]>>,
     compiled_values_to_dyn_array_indexes:
         HashMap<CompiledValue<UInt>, StatePartIndex<StatePartKindSmallSlots>>,
     compiled_value_bool_dest_is_small_map:
@@ -1818,6 +1819,9 @@ pub struct Compiler {
     traces: SimTraces<Vec<SimTrace<SimTraceKind, ()>>>,
     memories: Vec<Memory>,
     dump_assignments_dot: Option<DebugOpaque<Box<dyn Fn(&dyn fmt::Debug)>>>,
+    global_io: Vec<(SimIoForGlobal, CompiledValue<CanonicalType>)>,
+    global_io_set: HashSet<SimIoForGlobal>,
+    global_trace_decls: Vec<TraceDecl>,
 }
 
 macro_rules! impl_compiler {
@@ -1833,7 +1837,7 @@ macro_rules! impl_compiler {
         impl Compiler {
             fn make_trace_scalar_helper(
                 &mut self,
-                instantiated_module: InstantiatedModule,
+                instantiated_module_or_global: InstantiatedModuleOrGlobal,
                 target: MakeTraceDeclTarget,
                 source_location: SourceLocation,
                 empty_kind: impl FnOnce() -> SimTraceKind,
@@ -1841,7 +1845,7 @@ macro_rules! impl_compiler {
             ) -> TraceLocation {
                 match target {
                     MakeTraceDeclTarget::Expr(target) => {
-                        let compiled_value = self.compile_expr(instantiated_module, target);
+                        let compiled_value = self.compile_expr(instantiated_module_or_global, target);
                         let compiled_value = self.compiled_expr_to_value(compiled_value, source_location);
                         if compiled_value.range.is_empty() {
                             TraceLocation::Scalar(self.new_sim_trace(empty_kind()))
@@ -1871,7 +1875,7 @@ macro_rules! impl_compiler {
             }
             fn make_trace_scalar(
                 &mut self,
-                instantiated_module: InstantiatedModule,
+                instantiated_module_or_global: InstantiatedModuleOrGlobal,
                 target: MakeTraceDeclTarget,
                 name: Interned<str>,
                 source_location: SourceLocation,
@@ -1880,7 +1884,7 @@ macro_rules! impl_compiler {
                 match target.ty() {
                     CanonicalType::UInt(ty) => TraceUInt {
                         location: self.make_trace_scalar_helper(
-                            instantiated_module,
+                            instantiated_module_or_global,
                             target,
                             source_location,
                             || unreachable!(),
@@ -1895,7 +1899,7 @@ macro_rules! impl_compiler {
                     .into(),
                     CanonicalType::SInt(ty) => TraceSInt {
                         location: self.make_trace_scalar_helper(
-                            instantiated_module,
+                            instantiated_module_or_global,
                             target,
                             source_location,
                             || unreachable!(),
@@ -1910,7 +1914,7 @@ macro_rules! impl_compiler {
                     .into(),
                     CanonicalType::Bool(_) => TraceBool {
                         location: self.make_trace_scalar_helper(
-                            instantiated_module,
+                            instantiated_module_or_global,
                             target,
                             source_location,
                             || unreachable!(),
@@ -1927,7 +1931,7 @@ macro_rules! impl_compiler {
                         assert_eq!(ty.discriminant_bit_width(), ty.type_properties().bit_width);
                         let location = match target {
                             MakeTraceDeclTarget::Expr(target) => {
-                                let compiled_value = self.compile_expr(instantiated_module, target);
+                                let compiled_value = self.compile_expr(instantiated_module_or_global, target);
                                 let compiled_value =
                                     self.compiled_expr_to_value(compiled_value, source_location);
                                 let discriminant = self.compile_enum_discriminant(
@@ -1964,7 +1968,7 @@ macro_rules! impl_compiler {
                     CanonicalType::Bundle(_) => unreachable!(),
                     CanonicalType::AsyncReset(_) => TraceAsyncReset {
                         location: self.make_trace_scalar_helper(
-                            instantiated_module,
+                            instantiated_module_or_global,
                             target,
                             source_location,
                             || unreachable!(),
@@ -1978,7 +1982,7 @@ macro_rules! impl_compiler {
                     .into(),
                     CanonicalType::SyncReset(_) => TraceSyncReset {
                         location: self.make_trace_scalar_helper(
-                            instantiated_module,
+                            instantiated_module_or_global,
                             target,
                             source_location,
                             || unreachable!(),
@@ -1993,7 +1997,7 @@ macro_rules! impl_compiler {
                     CanonicalType::Reset(_) => unreachable!(),
                     CanonicalType::Clock(_) => TraceClock {
                         location: self.make_trace_scalar_helper(
-                            instantiated_module,
+                            instantiated_module_or_global,
                             target,
                             source_location,
                             || unreachable!(),
@@ -2007,7 +2011,7 @@ macro_rules! impl_compiler {
                     .into(),
                     CanonicalType::PhantomConst(ty) => TracePhantomConst {
                         location: self.make_trace_scalar_helper(
-                            instantiated_module,
+                            instantiated_module_or_global,
                             target,
                             source_location,
                             || SimTraceKind::PhantomConst { ty },
@@ -2022,7 +2026,7 @@ macro_rules! impl_compiler {
                     .into(),
                     CanonicalType::DynSimOnly(ty) => TraceSimOnly {
                         location: self.make_trace_scalar_helper(
-                            instantiated_module,
+                            instantiated_module_or_global,
                             target,
                             source_location,
                             || unreachable!(),
@@ -2038,7 +2042,7 @@ macro_rules! impl_compiler {
                     CanonicalType::TraceAsString(ty) => {
                         let location = match target {
                             MakeTraceDeclTarget::Expr(target) => {
-                                let compiled_value = self.compile_expr(instantiated_module, target);
+                                let compiled_value = self.compile_expr(instantiated_module_or_global, target);
                                 let CompiledValue { layout, range, write: _ } =
                                     self.compiled_expr_to_value(compiled_value, source_location).map_ty(Type::from_canonical);
                                 TraceLocation::Scalar(self.new_sim_trace(SimTraceKind::TraceAsString {
@@ -2314,6 +2318,9 @@ impl Compiler {
             traces: SimTraces(Vec::new()),
             memories: Vec::new(),
             dump_assignments_dot: None,
+            global_io: Vec::new(),
+            global_io_set: HashSet::default(),
+            global_trace_decls: Vec::new(),
         }
     }
     #[doc(hidden)]
@@ -2333,16 +2340,17 @@ impl Compiler {
     }
     fn make_trace_decl_child(
         &mut self,
-        instantiated_module: InstantiatedModule,
+        instantiated_module_or_global: impl Into<InstantiatedModuleOrGlobal>,
         target: MakeTraceDeclTarget,
         name: Interned<str>,
         source_location: SourceLocation,
     ) -> TraceDecl {
+        let instantiated_module_or_global = instantiated_module_or_global.into();
         match target.ty() {
             CanonicalType::Array(ty) => {
                 let elements = Interned::from_iter((0..ty.len()).map(|index| {
                     self.make_trace_decl_child(
-                        instantiated_module,
+                        instantiated_module_or_global,
                         match target {
                             MakeTraceDeclTarget::Expr(target) => MakeTraceDeclTarget::Expr(
                                 Expr::<Array>::from_canonical(target)[index],
@@ -2375,12 +2383,18 @@ impl Compiler {
             }
             CanonicalType::Enum(ty) => {
                 if ty.variants().iter().all(|v| v.ty.is_none()) {
-                    self.make_trace_scalar(instantiated_module, target, name, source_location)
+                    self.make_trace_scalar(
+                        instantiated_module_or_global,
+                        target,
+                        name,
+                        source_location,
+                    )
                 } else {
                     let flow = target.flow();
                     let location = match target {
                         MakeTraceDeclTarget::Expr(target) => {
-                            let compiled_value = self.compile_expr(instantiated_module, target);
+                            let compiled_value =
+                                self.compile_expr(instantiated_module_or_global, target);
                             let compiled_value =
                                 self.compiled_expr_to_value(compiled_value, source_location);
                             let discriminant = self.compile_enum_discriminant(
@@ -2419,7 +2433,7 @@ impl Compiler {
                             |(variant_index, variant)| {
                                 variant.ty.map(|variant_ty| {
                                     self.make_trace_decl_child(
-                                        instantiated_module,
+                                        instantiated_module_or_global,
                                         match target {
                                             MakeTraceDeclTarget::Expr(target) => {
                                                 MakeTraceDeclTarget::Expr(
@@ -2464,7 +2478,7 @@ impl Compiler {
                 let fields = Interned::from_iter(ty.fields().iter().zip(ty.field_offsets()).map(
                     |(field, field_offset)| {
                         self.make_trace_decl_child(
-                            instantiated_module,
+                            instantiated_module_or_global,
                             match target {
                                 MakeTraceDeclTarget::Expr(target) => {
                                     MakeTraceDeclTarget::Expr(Expr::field(
@@ -2514,22 +2528,23 @@ impl Compiler {
             | CanonicalType::DynSimOnly(_)
             | CanonicalType::PhantomConst(_)
             | CanonicalType::TraceAsString(_) => {
-                self.make_trace_scalar(instantiated_module, target, name, source_location)
+                self.make_trace_scalar(instantiated_module_or_global, target, name, source_location)
             }
         }
     }
     fn make_trace_decl(
         &mut self,
-        instantiated_module: InstantiatedModule,
+        instantiated_module_or_global: impl Into<InstantiatedModuleOrGlobal>,
         target_base: TargetBase,
     ) -> TraceDecl {
+        let instantiated_module_or_global = instantiated_module_or_global.into();
         let target = MakeTraceDeclTarget::Expr(target_base.to_expr());
         match target_base {
             TargetBase::ModuleIO(module_io) => TraceModuleIO {
                 name: module_io.name(),
                 child: self
                     .make_trace_decl_child(
-                        instantiated_module,
+                        instantiated_module_or_global,
                         target,
                         module_io.name(),
                         module_io.source_location(),
@@ -2542,7 +2557,7 @@ impl Compiler {
             TargetBase::MemPort(mem_port) => {
                 let name = Intern::intern_owned(mem_port.port_name().to_string());
                 let TraceDecl::Scope(TraceScope::Bundle(bundle)) = self.make_trace_decl_child(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     target,
                     name,
                     mem_port.source_location(),
@@ -2560,7 +2575,7 @@ impl Compiler {
                 name: reg.name(),
                 child: self
                     .make_trace_decl_child(
-                        instantiated_module,
+                        instantiated_module_or_global,
                         target,
                         reg.name(),
                         reg.source_location(),
@@ -2573,7 +2588,7 @@ impl Compiler {
                 name: reg.name(),
                 child: self
                     .make_trace_decl_child(
-                        instantiated_module,
+                        instantiated_module_or_global,
                         target,
                         reg.name(),
                         reg.source_location(),
@@ -2586,7 +2601,7 @@ impl Compiler {
                 name: reg.name(),
                 child: self
                     .make_trace_decl_child(
-                        instantiated_module,
+                        instantiated_module_or_global,
                         target,
                         reg.name(),
                         reg.source_location(),
@@ -2599,7 +2614,7 @@ impl Compiler {
                 name: wire.name(),
                 child: self
                     .make_trace_decl_child(
-                        instantiated_module,
+                        instantiated_module_or_global,
                         target,
                         wire.name(),
                         wire.source_location(),
@@ -2610,13 +2625,18 @@ impl Compiler {
             .into(),
             TargetBase::Instance(instance) => {
                 let TraceDecl::Scope(TraceScope::Bundle(instance_io)) = self.make_trace_decl_child(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     target,
                     instance.name(),
                     instance.source_location(),
                 ) else {
                     unreachable!()
                 };
+                let InstantiatedModuleOrGlobal::InstantiatedModule(instantiated_module) =
+                    instantiated_module_or_global
+                else {
+                    unreachable!();
+                };
                 let compiled_module = &self.modules[&InstantiatedModule::Child {
                     parent: instantiated_module.intern(),
                     instance: instance.intern(),
@@ -2629,23 +2649,45 @@ impl Compiler {
                 }
                 .into()
             }
+            TargetBase::FormalInput(formal_input) => TraceFormalInput {
+                name: formal_input.name(),
+                child: self
+                    .make_trace_decl_child(
+                        instantiated_module_or_global,
+                        target,
+                        formal_input.name(),
+                        formal_input.source_location(),
+                    )
+                    .intern(),
+                formal_input,
+            }
+            .into(),
+            TargetBase::SimIoForGlobal(_) => {
+                unreachable!("Module is known to not contain SimIoForGlobal from validation")
+            }
         }
     }
     fn compile_value(
         &mut self,
-        target: TargetInInstantiatedModule,
+        target: TargetInInstantiatedModuleOrGlobal,
     ) -> CompiledValue<CanonicalType> {
         if let Some(&retval) = self.compiled_values.get(&target) {
             return retval;
         }
-        let retval = match target.target {
+        let mut new_global_io = None;
+        let retval = match target.target() {
             Target::Base(base) => {
                 let unprefixed_layout = CompiledTypeLayout::get(base.canonical_ty());
-                let layout = unprefixed_layout.with_prefixed_debug_names(&format!(
-                    "{:?}.{:?}",
-                    target.instantiated_module,
-                    base.target_name()
-                ));
+                let layout = unprefixed_layout.with_prefixed_debug_names(&match target
+                    .instantiated_module_or_global()
+                {
+                    InstantiatedModuleOrGlobal::Global => {
+                        format!("{:?}", base.target_name())
+                    }
+                    InstantiatedModuleOrGlobal::InstantiatedModule(instantiated_module) => {
+                        format!("{instantiated_module:?}.{:?}", base.target_name())
+                    }
+                });
                 let range = self.insns.allocate_variable(&layout.layout);
                 let write = match *base {
                     TargetBase::ModuleIO(_)
@@ -2655,7 +2697,7 @@ impl Compiler {
                     TargetBase::Reg(_) | TargetBase::RegSync(_) | TargetBase::RegAsync(_) => {
                         let write_layout = unprefixed_layout.with_prefixed_debug_names(&format!(
                             "{:?}.{:?}$next",
-                            target.instantiated_module,
+                            target.instantiated_module_or_global(),
                             base.target_name()
                         ));
                         Some((
@@ -2663,6 +2705,18 @@ impl Compiler {
                             self.insns.allocate_variable(&write_layout.layout),
                         ))
                     }
+                    TargetBase::FormalInput(formal_input) => {
+                        if self.global_io_set.insert(SimIoForGlobal::new(formal_input)) {
+                            new_global_io = Some(formal_input);
+                            let trace_decl =
+                                self.make_trace_decl(target.instantiated_module_or_global(), *base);
+                            self.global_trace_decls.push(trace_decl);
+                        }
+                        None
+                    }
+                    TargetBase::SimIoForGlobal(_) => unreachable!(
+                        "Module is known to not contain SimIoForGlobal from validation"
+                    ),
                 };
                 CompiledValue {
                     range,
@@ -2671,10 +2725,10 @@ impl Compiler {
                 }
             }
             Target::Child(target_child) => {
-                let parent = self.compile_value(TargetInInstantiatedModule {
-                    instantiated_module: target.instantiated_module,
-                    target: *target_child.parent(),
-                });
+                let parent = self.compile_value(TargetInInstantiatedModuleOrGlobal::new(
+                    target.instantiated_module_or_global(),
+                    *target_child.parent(),
+                ));
                 match *target_child.path_element() {
                     TargetPathElement::BundleField(TargetPathBundleField { name }) => {
                         parent.map_ty(Bundle::from_canonical).field_by_name(name)
@@ -2693,6 +2747,10 @@ impl Compiler {
             }
         };
         self.compiled_values.insert(target, retval);
+        if let Some(new_global_io) = new_global_io {
+            self.global_io
+                .push((SimIoForGlobal::new(new_global_io), retval));
+        }
         retval
     }
     fn add_assignment<T: Into<InsnOrLabel>>(
@@ -2707,18 +2765,20 @@ impl Compiler {
     }
     fn simple_big_expr_input(
         &mut self,
-        instantiated_module: InstantiatedModule,
+        instantiated_module_or_global: InstantiatedModuleOrGlobal,
         input: Expr<CanonicalType>,
     ) -> StatePartIndex<StatePartKindBigSlots> {
-        let input = self.compile_expr(instantiated_module, input);
-        let input =
-            self.compiled_expr_to_value(input, instantiated_module.leaf_module().source_location());
+        let input = self.compile_expr(instantiated_module_or_global, input);
+        let input = self.compiled_expr_to_value(
+            input,
+            instantiated_module_or_global.leaf_module_source_location(),
+        );
         assert_eq!(input.range.len(), TypeLen::big_slot());
         input.range.big_slots.start
     }
     fn compile_expr_helper(
         &mut self,
-        instantiated_module: InstantiatedModule,
+        instantiated_module_or_global: InstantiatedModuleOrGlobal,
         dest_ty: CanonicalType,
         make_insns: impl FnOnce(&mut Self, TypeIndexRange) -> Vec<Insn>,
     ) -> CompiledValue<CanonicalType> {
@@ -2733,24 +2793,24 @@ impl Compiler {
         self.add_assignment(
             Interned::default(),
             insns,
-            instantiated_module.leaf_module().source_location(),
+            instantiated_module_or_global.leaf_module_source_location(),
         );
         retval
     }
     fn simple_nary_big_expr_helper(
         &mut self,
-        instantiated_module: InstantiatedModule,
+        instantiated_module_or_global: InstantiatedModuleOrGlobal,
         dest_ty: CanonicalType,
         make_insns: impl FnOnce(StatePartIndex<StatePartKindBigSlots>) -> Vec<Insn>,
     ) -> CompiledValue<CanonicalType> {
-        self.compile_expr_helper(instantiated_module, dest_ty, |_, dest| {
+        self.compile_expr_helper(instantiated_module_or_global, dest_ty, |_, dest| {
             assert_eq!(dest.len(), TypeLen::big_slot());
             make_insns(dest.big_slots.start)
         })
     }
     fn simple_nary_big_expr<const N: usize>(
         &mut self,
-        instantiated_module: InstantiatedModule,
+        instantiated_module_or_global: InstantiatedModuleOrGlobal,
         dest_ty: CanonicalType,
         inputs: [Expr<CanonicalType>; N],
         make_insns: impl FnOnce(
@@ -2758,8 +2818,9 @@ impl Compiler {
             [StatePartIndex<StatePartKindBigSlots>; N],
         ) -> Vec<Insn>,
     ) -> CompiledValue<CanonicalType> {
-        let inputs = inputs.map(|input| self.simple_big_expr_input(instantiated_module, input));
-        self.simple_nary_big_expr_helper(instantiated_module, dest_ty, |dest| {
+        let inputs =
+            inputs.map(|input| self.simple_big_expr_input(instantiated_module_or_global, input));
+        self.simple_nary_big_expr_helper(instantiated_module_or_global, dest_ty, |dest| {
             make_insns(dest, inputs)
         })
     }
@@ -2851,20 +2912,22 @@ impl Compiler {
     }
     fn compile_cast_scalar_to_bits<T: Type>(
         &mut self,
-        instantiated_module: InstantiatedModule,
+        instantiated_module_or_global: InstantiatedModuleOrGlobal,
         arg: Expr<CanonicalType>,
         cast_fn: impl FnOnce(Expr<T>) -> Expr<UInt>,
     ) -> CompiledValue<UInt> {
         let arg = Expr::<T>::from_canonical(arg);
         let retval = cast_fn(arg);
-        let retval = self.compile_expr(instantiated_module, Expr::canonical(retval));
-        let retval = self
-            .compiled_expr_to_value(retval, instantiated_module.leaf_module().source_location());
+        let retval = self.compile_expr(instantiated_module_or_global, Expr::canonical(retval));
+        let retval = self.compiled_expr_to_value(
+            retval,
+            instantiated_module_or_global.leaf_module_source_location(),
+        );
         retval.map_ty(UInt::from_canonical)
     }
     fn compile_cast_aggregate_to_bits(
         &mut self,
-        instantiated_module: InstantiatedModule,
+        instantiated_module_or_global: InstantiatedModuleOrGlobal,
         parts: impl IntoIterator<Item = Expr<CanonicalType>>,
     ) -> CompiledValue<UInt> {
         let retval = parts
@@ -2872,22 +2935,26 @@ impl Compiler {
             .map(|part| part.cast_to_bits())
             .reduce(|accumulator, part| accumulator | (part << accumulator.ty().width))
             .unwrap_or_else(|| UInt[0].zero().to_expr());
-        let retval = self.compile_expr(instantiated_module, Expr::canonical(retval));
-        let retval = self
-            .compiled_expr_to_value(retval, instantiated_module.leaf_module().source_location());
+        let retval = self.compile_expr(instantiated_module_or_global, Expr::canonical(retval));
+        let retval = self.compiled_expr_to_value(
+            retval,
+            instantiated_module_or_global.leaf_module_source_location(),
+        );
         retval.map_ty(UInt::from_canonical)
     }
     fn compile_cast_to_bits(
         &mut self,
-        instantiated_module: InstantiatedModule,
+        instantiated_module_or_global: InstantiatedModuleOrGlobal,
         expr: ops::CastToBits,
     ) -> CompiledValue<UInt> {
         match expr.arg().ty() {
             CanonicalType::UInt(_) => {
-                self.compile_cast_scalar_to_bits(instantiated_module, expr.arg(), |arg| arg)
+                self.compile_cast_scalar_to_bits(instantiated_module_or_global, expr.arg(), |arg| {
+                    arg
+                })
             }
             CanonicalType::SInt(ty) => self.compile_cast_scalar_to_bits(
-                instantiated_module,
+                instantiated_module_or_global,
                 expr.arg(),
                 |arg: Expr<SInt>| arg.cast_to(ty.as_same_width_uint()),
             ),
@@ -2896,33 +2963,33 @@ impl Compiler {
             | CanonicalType::SyncReset(_)
             | CanonicalType::Reset(_)
             | CanonicalType::Clock(_) => self.compile_cast_scalar_to_bits(
-                instantiated_module,
+                instantiated_module_or_global,
                 expr.arg(),
                 |arg: Expr<Bool>| arg.cast_to(UInt[1]),
             ),
             CanonicalType::Array(ty) => self.compile_cast_aggregate_to_bits(
-                instantiated_module,
+                instantiated_module_or_global,
                 (0..ty.len()).map(|index| Expr::<Array>::from_canonical(expr.arg())[index]),
             ),
             CanonicalType::Enum(ty) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     UInt[ty.type_properties().bit_width].canonical(),
                     [Expr::canonical(expr.arg())],
                     |dest, [src]| vec![Insn::Copy { dest, src }],
                 )
                 .map_ty(UInt::from_canonical),
             CanonicalType::Bundle(ty) => self.compile_cast_aggregate_to_bits(
-                instantiated_module,
+                instantiated_module_or_global,
                 ty.fields().iter().map(|field| {
                     Expr::field(Expr::<Bundle>::from_canonical(expr.arg()), &field.name)
                 }),
             ),
             CanonicalType::PhantomConst(_) | CanonicalType::DynSimOnly(_) => {
-                self.compile_cast_aggregate_to_bits(instantiated_module, [])
+                self.compile_cast_aggregate_to_bits(instantiated_module_or_global, [])
             }
             CanonicalType::TraceAsString(_) => self.compile_cast_to_bits(
-                instantiated_module,
+                instantiated_module_or_global,
                 ops::CastToBits::new(
                     ops::TraceAsStringAsInner::new(Expr::from_canonical(expr.arg())).to_expr(),
                 ),
@@ -2931,7 +2998,7 @@ impl Compiler {
     }
     fn compile_cast_bits_to_or_uninit(
         &mut self,
-        instantiated_module: InstantiatedModule,
+        instantiated_module_or_global: InstantiatedModuleOrGlobal,
         arg: Option<Expr<UInt>>,
         ty: CanonicalType,
     ) -> CompiledValue<CanonicalType> {
@@ -2960,7 +3027,7 @@ impl Compiler {
             }
             ty @ CanonicalType::Enum(_) => {
                 return self.simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     ty,
                     [Expr::canonical(arg.unwrap_or_else(|| {
                         UInt::new_dyn(ty.bit_width()).zero().to_expr()
@@ -3005,16 +3072,20 @@ impl Compiler {
             ),
             CanonicalType::PhantomConst(ty) => {
                 if let Some(arg) = arg {
-                    let _ = self.compile_expr(instantiated_module, Expr::canonical(arg));
+                    let _ = self.compile_expr(instantiated_module_or_global, Expr::canonical(arg));
                 }
                 Expr::canonical(ty.to_expr())
             }
             CanonicalType::DynSimOnly(ty) => {
                 assert!(arg.is_none(), "can't cast bits to SimOnly");
-                return self.compile_expr_helper(instantiated_module, ty.canonical(), |_, dest| {
-                    assert_eq!(dest.len(), TypeLen::sim_only_slot());
-                    vec![]
-                });
+                return self.compile_expr_helper(
+                    instantiated_module_or_global,
+                    ty.canonical(),
+                    |_, dest| {
+                        assert_eq!(dest.len(), TypeLen::sim_only_slot());
+                        vec![]
+                    },
+                );
             }
             CanonicalType::TraceAsString(ty) => Expr::canonical(
                 ops::ToTraceAsString::new(
@@ -3027,24 +3098,27 @@ impl Compiler {
                 .to_expr(),
             ),
         };
-        let retval = self.compile_expr(instantiated_module, Expr::canonical(retval));
-        self.compiled_expr_to_value(retval, instantiated_module.leaf_module().source_location())
+        let retval = self.compile_expr(instantiated_module_or_global, Expr::canonical(retval));
+        self.compiled_expr_to_value(
+            retval,
+            instantiated_module_or_global.leaf_module_source_location(),
+        )
     }
     fn compile_aggregate_literal(
         &mut self,
-        instantiated_module: InstantiatedModule,
+        instantiated_module_or_global: InstantiatedModuleOrGlobal,
         dest_ty: CanonicalType,
         inputs: Interned<[Expr<CanonicalType>]>,
     ) -> CompiledValue<CanonicalType> {
-        self.compile_expr_helper(instantiated_module, dest_ty, |this, dest| {
+        self.compile_expr_helper(instantiated_module_or_global, dest_ty, |this, dest| {
             let mut insns = Vec::new();
             let mut offset = TypeIndex::ZERO;
             for input in inputs {
-                let input = this.compile_expr(instantiated_module, input);
+                let input = this.compile_expr(instantiated_module_or_global, input);
                 let input = this
                     .compiled_expr_to_value(
                         input,
-                        instantiated_module.leaf_module().source_location(),
+                        instantiated_module_or_global.leaf_module_source_location(),
                     )
                     .range;
                 insns.extend(
@@ -3057,9 +3131,10 @@ impl Compiler {
     }
     fn compile_expr(
         &mut self,
-        instantiated_module: InstantiatedModule,
+        instantiated_module_or_global: impl Into<InstantiatedModuleOrGlobal>,
         expr: Expr<CanonicalType>,
     ) -> CompiledExpr<CanonicalType> {
+        let instantiated_module_or_global = instantiated_module_or_global.into();
         if let Some(&retval) = self.compiled_exprs.get(&expr) {
             return retval;
         }
@@ -3094,30 +3169,32 @@ impl Compiler {
                 CanonicalType::DynSimOnly(_) => unreachable!(),
                 CanonicalType::TraceAsString(_) => unreachable!(),
             };
-            self.simple_nary_big_expr(instantiated_module, expr.ty(), [arg], |dest, [src]| match (
-                src_signed,
-                dest_signed,
-            ) {
-                (false, false) | (true, true) => {
-                    vec![Insn::Copy { dest, src }]
-                }
-                (false, true) => vec![Insn::CastToSInt {
-                    dest,
-                    src,
-                    dest_width: 1,
-                }],
-                (true, false) => vec![Insn::CastToUInt {
-                    dest,
-                    src,
-                    dest_width: 1,
-                }],
-            })
+            self.simple_nary_big_expr(
+                instantiated_module_or_global,
+                expr.ty(),
+                [arg],
+                |dest, [src]| match (src_signed, dest_signed) {
+                    (false, false) | (true, true) => {
+                        vec![Insn::Copy { dest, src }]
+                    }
+                    (false, true) => vec![Insn::CastToSInt {
+                        dest,
+                        src,
+                        dest_width: 1,
+                    }],
+                    (true, false) => vec![Insn::CastToUInt {
+                        dest,
+                        src,
+                        dest_width: 1,
+                    }],
+                },
+            )
             .into()
         };
         let retval: CompiledExpr<_> = match *Expr::expr_enum(expr) {
             ExprEnum::UIntLiteral(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [],
                     |dest, []| {
@@ -3130,7 +3207,7 @@ impl Compiler {
                 .into(),
             ExprEnum::SIntLiteral(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [],
                     |dest, []| {
@@ -3142,21 +3219,38 @@ impl Compiler {
                 )
                 .into(),
             ExprEnum::BoolLiteral(expr) => self
-                .simple_nary_big_expr(instantiated_module, Bool.canonical(), [], |dest, []| {
-                    vec![Insn::Const {
-                        dest,
-                        value: BigInt::from(expr).intern_sized(),
-                    }]
-                })
+                .simple_nary_big_expr(
+                    instantiated_module_or_global,
+                    Bool.canonical(),
+                    [],
+                    |dest, []| {
+                        vec![Insn::Const {
+                            dest,
+                            value: BigInt::from(expr).intern_sized(),
+                        }]
+                    },
+                )
                 .into(),
             ExprEnum::PhantomConst(_) => self
-                .compile_aggregate_literal(instantiated_module, expr.ty(), Interned::default())
+                .compile_aggregate_literal(
+                    instantiated_module_or_global,
+                    expr.ty(),
+                    Interned::default(),
+                )
                 .into(),
             ExprEnum::BundleLiteral(literal) => self
-                .compile_aggregate_literal(instantiated_module, expr.ty(), literal.field_values())
+                .compile_aggregate_literal(
+                    instantiated_module_or_global,
+                    expr.ty(),
+                    literal.field_values(),
+                )
                 .into(),
             ExprEnum::ArrayLiteral(literal) => self
-                .compile_aggregate_literal(instantiated_module, expr.ty(), literal.element_values())
+                .compile_aggregate_literal(
+                    instantiated_module_or_global,
+                    expr.ty(),
+                    literal.element_values(),
+                )
                 .into(),
             ExprEnum::EnumLiteral(expr) => {
                 let enum_bits_ty = UInt[expr.ty().type_properties().bit_width];
@@ -3174,16 +3268,16 @@ impl Compiler {
                         .to_expr()
                 };
                 self.compile_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     enum_bits.cast_bits_to(expr.ty().canonical()),
                 )
             }
             ExprEnum::Uninit(expr) => self
-                .compile_cast_bits_to_or_uninit(instantiated_module, None, expr.ty())
+                .compile_cast_bits_to_or_uninit(instantiated_module_or_global, None, expr.ty())
                 .into(),
             ExprEnum::NotU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.arg().ty().canonical(),
                     [Expr::canonical(expr.arg())],
                     |dest, [src]| {
@@ -3197,7 +3291,7 @@ impl Compiler {
                 .into(),
             ExprEnum::NotS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.arg().ty().canonical(),
                     [Expr::canonical(expr.arg())],
                     |dest, [src]| vec![Insn::NotS { dest, src }],
@@ -3205,7 +3299,7 @@ impl Compiler {
                 .into(),
             ExprEnum::NotB(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.arg().ty().canonical(),
                     [Expr::canonical(expr.arg())],
                     |dest, [src]| {
@@ -3219,7 +3313,7 @@ impl Compiler {
                 .into(),
             ExprEnum::Neg(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.arg())],
                     |dest, [src]| vec![Insn::Neg { dest, src }],
@@ -3227,7 +3321,7 @@ impl Compiler {
                 .into(),
             ExprEnum::BitAndU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::And { dest, lhs, rhs }],
@@ -3235,7 +3329,7 @@ impl Compiler {
                 .into(),
             ExprEnum::BitAndS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::And { dest, lhs, rhs }],
@@ -3243,7 +3337,7 @@ impl Compiler {
                 .into(),
             ExprEnum::BitAndB(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::And { dest, lhs, rhs }],
@@ -3251,7 +3345,7 @@ impl Compiler {
                 .into(),
             ExprEnum::BitOrU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::Or { dest, lhs, rhs }],
@@ -3259,7 +3353,7 @@ impl Compiler {
                 .into(),
             ExprEnum::BitOrS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::Or { dest, lhs, rhs }],
@@ -3267,7 +3361,7 @@ impl Compiler {
                 .into(),
             ExprEnum::BitOrB(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::Or { dest, lhs, rhs }],
@@ -3275,7 +3369,7 @@ impl Compiler {
                 .into(),
             ExprEnum::BitXorU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::Xor { dest, lhs, rhs }],
@@ -3283,7 +3377,7 @@ impl Compiler {
                 .into(),
             ExprEnum::BitXorS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::Xor { dest, lhs, rhs }],
@@ -3291,7 +3385,7 @@ impl Compiler {
                 .into(),
             ExprEnum::BitXorB(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::Xor { dest, lhs, rhs }],
@@ -3299,7 +3393,7 @@ impl Compiler {
                 .into(),
             ExprEnum::AddU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::Add { dest, lhs, rhs }],
@@ -3307,7 +3401,7 @@ impl Compiler {
                 .into(),
             ExprEnum::AddS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::Add { dest, lhs, rhs }],
@@ -3315,7 +3409,7 @@ impl Compiler {
                 .into(),
             ExprEnum::SubU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| {
@@ -3330,7 +3424,7 @@ impl Compiler {
                 .into(),
             ExprEnum::SubS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::SubS { dest, lhs, rhs }],
@@ -3338,7 +3432,7 @@ impl Compiler {
                 .into(),
             ExprEnum::MulU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::Mul { dest, lhs, rhs }],
@@ -3346,7 +3440,7 @@ impl Compiler {
                 .into(),
             ExprEnum::MulS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::Mul { dest, lhs, rhs }],
@@ -3354,7 +3448,7 @@ impl Compiler {
                 .into(),
             ExprEnum::DivU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::Div { dest, lhs, rhs }],
@@ -3362,7 +3456,7 @@ impl Compiler {
                 .into(),
             ExprEnum::DivS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::Div { dest, lhs, rhs }],
@@ -3370,7 +3464,7 @@ impl Compiler {
                 .into(),
             ExprEnum::RemU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::Rem { dest, lhs, rhs }],
@@ -3378,7 +3472,7 @@ impl Compiler {
                 .into(),
             ExprEnum::RemS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::Rem { dest, lhs, rhs }],
@@ -3386,7 +3480,7 @@ impl Compiler {
                 .into(),
             ExprEnum::DynShlU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::DynShl { dest, lhs, rhs }],
@@ -3394,7 +3488,7 @@ impl Compiler {
                 .into(),
             ExprEnum::DynShlS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::DynShl { dest, lhs, rhs }],
@@ -3402,7 +3496,7 @@ impl Compiler {
                 .into(),
             ExprEnum::DynShrU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::DynShr { dest, lhs, rhs }],
@@ -3410,7 +3504,7 @@ impl Compiler {
                 .into(),
             ExprEnum::DynShrS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::DynShr { dest, lhs, rhs }],
@@ -3418,7 +3512,7 @@ impl Compiler {
                 .into(),
             ExprEnum::FixedShlU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs())],
                     |dest, [lhs]| {
@@ -3432,7 +3526,7 @@ impl Compiler {
                 .into(),
             ExprEnum::FixedShlS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs())],
                     |dest, [lhs]| {
@@ -3446,7 +3540,7 @@ impl Compiler {
                 .into(),
             ExprEnum::FixedShrU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs())],
                     |dest, [lhs]| {
@@ -3460,7 +3554,7 @@ impl Compiler {
                 .into(),
             ExprEnum::FixedShrS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.lhs())],
                     |dest, [lhs]| {
@@ -3474,7 +3568,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpLtB(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::CmpLt { dest, lhs, rhs }],
@@ -3482,7 +3576,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpLeB(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::CmpLe { dest, lhs, rhs }],
@@ -3490,7 +3584,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpGtB(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     // swap both comparison direction and lhs/rhs
                     [Expr::canonical(expr.rhs()), Expr::canonical(expr.lhs())],
@@ -3499,7 +3593,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpGeB(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     // swap both comparison direction and lhs/rhs
                     [Expr::canonical(expr.rhs()), Expr::canonical(expr.lhs())],
@@ -3508,7 +3602,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpEqB(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::CmpEq { dest, lhs, rhs }],
@@ -3516,7 +3610,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpNeB(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::CmpNe { dest, lhs, rhs }],
@@ -3524,7 +3618,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpLtU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::CmpLt { dest, lhs, rhs }],
@@ -3532,7 +3626,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpLeU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::CmpLe { dest, lhs, rhs }],
@@ -3540,7 +3634,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpGtU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     // swap both comparison direction and lhs/rhs
                     [Expr::canonical(expr.rhs()), Expr::canonical(expr.lhs())],
@@ -3549,7 +3643,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpGeU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     // swap both comparison direction and lhs/rhs
                     [Expr::canonical(expr.rhs()), Expr::canonical(expr.lhs())],
@@ -3558,7 +3652,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpEqU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::CmpEq { dest, lhs, rhs }],
@@ -3566,7 +3660,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpNeU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::CmpNe { dest, lhs, rhs }],
@@ -3574,7 +3668,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpLtS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::CmpLt { dest, lhs, rhs }],
@@ -3582,7 +3676,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpLeS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::CmpLe { dest, lhs, rhs }],
@@ -3590,7 +3684,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpGtS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     // swap both comparison direction and lhs/rhs
                     [Expr::canonical(expr.rhs()), Expr::canonical(expr.lhs())],
@@ -3599,7 +3693,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpGeS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     // swap both comparison direction and lhs/rhs
                     [Expr::canonical(expr.rhs()), Expr::canonical(expr.lhs())],
@@ -3608,7 +3702,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpEqS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::CmpEq { dest, lhs, rhs }],
@@ -3616,7 +3710,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CmpNeS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Bool.canonical(),
                     [Expr::canonical(expr.lhs()), Expr::canonical(expr.rhs())],
                     |dest, [lhs, rhs]| vec![Insn::CmpNe { dest, lhs, rhs }],
@@ -3624,7 +3718,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CastUIntToUInt(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.arg())],
                     |dest, [src]| {
@@ -3638,7 +3732,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CastUIntToSInt(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.arg())],
                     |dest, [src]| {
@@ -3652,7 +3746,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CastSIntToUInt(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.arg())],
                     |dest, [src]| {
@@ -3666,7 +3760,7 @@ impl Compiler {
                 .into(),
             ExprEnum::CastSIntToSInt(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     expr.ty().canonical(),
                     [Expr::canonical(expr.arg())],
                     |dest, [src]| {
@@ -3706,76 +3800,90 @@ impl Compiler {
             ExprEnum::CastClockToUInt(expr) => cast_bit(Expr::canonical(expr.arg())),
             ExprEnum::CastClockToSInt(expr) => cast_bit(Expr::canonical(expr.arg())),
             ExprEnum::FieldAccess(expr) => self
-                .compile_expr(instantiated_module, Expr::canonical(expr.base()))
+                .compile_expr(instantiated_module_or_global, Expr::canonical(expr.base()))
                 .map_ty(Bundle::from_canonical)
                 .field_by_index(expr.field_index()),
             ExprEnum::VariantAccess(variant_access) => {
                 let start = variant_access.base().ty().discriminant_bit_width();
                 let len = expr.ty().bit_width();
                 self.compile_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     variant_access.base().cast_to_bits()[start..start + len]
                         .cast_bits_to(expr.ty()),
                 )
             }
             ExprEnum::ArrayIndex(expr) => self
-                .compile_expr(instantiated_module, Expr::canonical(expr.base()))
+                .compile_expr(instantiated_module_or_global, Expr::canonical(expr.base()))
                 .map_ty(Array::from_canonical)
                 .element(expr.element_index()),
             ExprEnum::DynArrayIndex(expr) => {
-                let element_index =
-                    self.compile_expr(instantiated_module, Expr::canonical(expr.element_index()));
+                let element_index = self.compile_expr(
+                    instantiated_module_or_global,
+                    Expr::canonical(expr.element_index()),
+                );
                 let element_index = self.compiled_expr_to_value(
                     element_index,
-                    instantiated_module.leaf_module().source_location(),
+                    instantiated_module_or_global.leaf_module_source_location(),
                 );
                 let index_slot = self.compiled_value_to_dyn_array_index(
                     element_index.map_ty(UInt::from_canonical),
-                    instantiated_module.leaf_module().source_location(),
+                    instantiated_module_or_global.leaf_module_source_location(),
                 );
-                self.compile_expr(instantiated_module, Expr::canonical(expr.base()))
+                self.compile_expr(instantiated_module_or_global, Expr::canonical(expr.base()))
                     .map_ty(Array::from_canonical)
                     .element_dyn(index_slot)
             }
             ExprEnum::ReduceBitAndU(expr) => if expr.arg().ty().width() == 0 {
-                self.compile_expr(instantiated_module, Expr::canonical(true.to_expr()))
+                self.compile_expr(
+                    instantiated_module_or_global,
+                    Expr::canonical(true.to_expr()),
+                )
             } else {
                 self.compile_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Expr::canonical(expr.arg().cmp_eq(expr.arg().ty().from_int_wrapping(-1))),
                 )
             }
             .into(),
             ExprEnum::ReduceBitAndS(expr) => if expr.arg().ty().width() == 0 {
-                self.compile_expr(instantiated_module, Expr::canonical(true.to_expr()))
+                self.compile_expr(
+                    instantiated_module_or_global,
+                    Expr::canonical(true.to_expr()),
+                )
             } else {
                 self.compile_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Expr::canonical(expr.arg().cmp_eq(expr.arg().ty().from_int_wrapping(-1))),
                 )
             }
             .into(),
             ExprEnum::ReduceBitOrU(expr) => if expr.arg().ty().width() == 0 {
-                self.compile_expr(instantiated_module, Expr::canonical(false.to_expr()))
+                self.compile_expr(
+                    instantiated_module_or_global,
+                    Expr::canonical(false.to_expr()),
+                )
             } else {
                 self.compile_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Expr::canonical(expr.arg().cmp_ne(expr.arg().ty().from_int_wrapping(0))),
                 )
             }
             .into(),
             ExprEnum::ReduceBitOrS(expr) => if expr.arg().ty().width() == 0 {
-                self.compile_expr(instantiated_module, Expr::canonical(false.to_expr()))
+                self.compile_expr(
+                    instantiated_module_or_global,
+                    Expr::canonical(false.to_expr()),
+                )
             } else {
                 self.compile_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     Expr::canonical(expr.arg().cmp_ne(expr.arg().ty().from_int_wrapping(0))),
                 )
             }
             .into(),
             ExprEnum::ReduceBitXorU(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     UInt::<1>::TYPE.canonical(),
                     [Expr::canonical(expr.arg())],
                     |dest, [src]| {
@@ -3789,7 +3897,7 @@ impl Compiler {
                 .into(),
             ExprEnum::ReduceBitXorS(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     UInt::<1>::TYPE.canonical(),
                     [Expr::canonical(expr.arg())],
                     |dest, [src]| {
@@ -3803,7 +3911,7 @@ impl Compiler {
                 .into(),
             ExprEnum::SliceUInt(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     UInt::new_dyn(expr.range().len()).canonical(),
                     [Expr::canonical(expr.base())],
                     |dest, [src]| {
@@ -3818,7 +3926,7 @@ impl Compiler {
                 .into(),
             ExprEnum::SliceSInt(expr) => self
                 .simple_nary_big_expr(
-                    instantiated_module,
+                    instantiated_module_or_global,
                     UInt::new_dyn(expr.range().len()).canonical(),
                     [Expr::canonical(expr.base())],
                     |dest, [src]| {
@@ -3832,62 +3940,75 @@ impl Compiler {
                 )
                 .into(),
             ExprEnum::CastToBits(expr) => self
-                .compile_cast_to_bits(instantiated_module, expr)
+                .compile_cast_to_bits(instantiated_module_or_global, expr)
                 .map_ty(CanonicalType::UInt)
                 .into(),
             ExprEnum::CastBitsTo(expr) => self
-                .compile_cast_bits_to_or_uninit(instantiated_module, Some(expr.arg()), expr.ty())
+                .compile_cast_bits_to_or_uninit(
+                    instantiated_module_or_global,
+                    Some(expr.arg()),
+                    expr.ty(),
+                )
                 .into(),
             ExprEnum::ToTraceAsString(expr) => self
-                .compile_expr(instantiated_module, expr.inner())
+                .compile_expr(instantiated_module_or_global, expr.inner())
                 .wrap_in_trace_as_string(expr.ty())
                 .map_ty(|ty| ty.canonical()),
             ExprEnum::TraceAsStringAsInner(expr) => self
-                .compile_expr(instantiated_module, Expr::canonical(expr.arg()))
+                .compile_expr(instantiated_module_or_global, Expr::canonical(expr.arg()))
                 .map_ty(TraceAsString::from_canonical)
                 .inner(),
             ExprEnum::ModuleIO(expr) => self
-                .compile_value(TargetInInstantiatedModule {
-                    instantiated_module,
-                    target: expr.into(),
-                })
+                .compile_value(TargetInInstantiatedModuleOrGlobal::from_target(
+                    instantiated_module_or_global,
+                    expr.into(),
+                ))
                 .into(),
             ExprEnum::Instance(expr) => self
-                .compile_value(TargetInInstantiatedModule {
-                    instantiated_module,
-                    target: expr.into(),
-                })
+                .compile_value(TargetInInstantiatedModuleOrGlobal::from_target(
+                    instantiated_module_or_global,
+                    expr.into(),
+                ))
                 .into(),
             ExprEnum::Wire(expr) => self
-                .compile_value(TargetInInstantiatedModule {
-                    instantiated_module,
-                    target: expr.into(),
-                })
+                .compile_value(TargetInInstantiatedModuleOrGlobal::from_target(
+                    instantiated_module_or_global,
+                    expr.into(),
+                ))
                 .into(),
             ExprEnum::Reg(expr) => self
-                .compile_value(TargetInInstantiatedModule {
-                    instantiated_module,
-                    target: expr.into(),
-                })
+                .compile_value(TargetInInstantiatedModuleOrGlobal::from_target(
+                    instantiated_module_or_global,
+                    expr.into(),
+                ))
                 .into(),
             ExprEnum::RegSync(expr) => self
-                .compile_value(TargetInInstantiatedModule {
-                    instantiated_module,
-                    target: expr.into(),
-                })
+                .compile_value(TargetInInstantiatedModuleOrGlobal::from_target(
+                    instantiated_module_or_global,
+                    expr.into(),
+                ))
                 .into(),
             ExprEnum::RegAsync(expr) => self
-                .compile_value(TargetInInstantiatedModule {
-                    instantiated_module,
-                    target: expr.into(),
-                })
+                .compile_value(TargetInInstantiatedModuleOrGlobal::from_target(
+                    instantiated_module_or_global,
+                    expr.into(),
+                ))
                 .into(),
             ExprEnum::MemPort(expr) => self
-                .compile_value(TargetInInstantiatedModule {
-                    instantiated_module,
-                    target: expr.into(),
-                })
+                .compile_value(TargetInInstantiatedModuleOrGlobal::from_target(
+                    instantiated_module_or_global,
+                    expr.into(),
+                ))
                 .into(),
+            ExprEnum::FormalInput(expr) => self
+                .compile_value(TargetInInstantiatedModuleOrGlobal::from_target(
+                    instantiated_module_or_global,
+                    expr.into(),
+                ))
+                .into(),
+            ExprEnum::SimIoForGlobal(_) => {
+                unreachable!("Module is known to not contain SimIoForGlobal from validation");
+            }
         };
         self.compiled_exprs.insert(expr, retval);
         retval
@@ -4013,10 +4134,11 @@ impl Compiler {
         let Some(target) = lhs.target() else {
             unreachable!("connect lhs must have target");
         };
-        let lhs_decl_conditions = self.decl_conditions[&TargetInInstantiatedModule {
-            instantiated_module: lhs_instantiated_module,
-            target: target.base().into(),
-        }];
+        let lhs_decl_conditions = self.decl_conditions
+            [&TargetInInstantiatedModuleOrGlobal::from_target(
+                lhs_instantiated_module,
+                target.base().into(),
+            )];
         let lhs = self.compile_expr(lhs_instantiated_module, lhs);
         let rhs = self.compile_expr(rhs_instantiated_module, rhs);
         let rhs = self.compiled_expr_to_value(rhs, source_location);
@@ -4257,10 +4379,8 @@ impl Compiler {
             StmtDeclaration::RegAsync(v) => v.reg.into(),
             StmtDeclaration::Instance(v) => v.instance.into(),
         };
-        let target = TargetInInstantiatedModule {
-            instantiated_module: *parent_module,
-            target: target_base.into(),
-        };
+        let target =
+            TargetInInstantiatedModuleOrGlobal::from_target(*parent_module, target_base.into());
         self.decl_conditions.insert(target, conditions);
         let compiled_value = self.compile_value(target);
         match declaration {
@@ -4825,10 +4945,10 @@ impl Compiler {
             .iter()
             .map(|&port| {
                 let target_base = TargetBase::MemPort(port);
-                let target = TargetInInstantiatedModule {
+                let target = TargetInInstantiatedModuleOrGlobal::from_target(
                     instantiated_module,
-                    target: target_base.into(),
-                };
+                    target_base.into(),
+                );
                 self.decl_conditions.insert(target, conditions);
                 let TraceDecl::Scope(TraceScope::MemPort(trace_port)) =
                     self.make_trace_decl(instantiated_module, target_base)
@@ -5144,10 +5264,8 @@ impl Compiler {
         instantiated_module: InstantiatedModule,
         clock_for_past: Target,
     ) -> ExternModuleClockForPast {
-        let clock_for_past = TargetInInstantiatedModule {
-            instantiated_module,
-            target: clock_for_past,
-        };
+        let clock_for_past =
+            TargetInInstantiatedModuleOrGlobal::from_target(instantiated_module, clock_for_past);
         let clock_for_past = self
             .compile_value(clock_for_past)
             .map_ty(Clock::from_canonical);
@@ -5191,10 +5309,11 @@ impl Compiler {
                      module_io,
                  }| {
                     let target_base = TargetBase::from(module_io);
-                    let current = self.compile_value(TargetInInstantiatedModule {
-                        instantiated_module,
-                        target: target_base.into(),
-                    });
+                    let current =
+                        self.compile_value(TargetInInstantiatedModuleOrGlobal::from_target(
+                            instantiated_module,
+                            target_base.into(),
+                        ));
                     let unprefixed_layout = CompiledTypeLayout::get(module_io.ty());
                     let past_layout = unprefixed_layout.with_prefixed_debug_names(&format!(
                         "{module_prefix}{:?}$past({trimmed_clock_for_past_debug_name})",
@@ -5232,10 +5351,10 @@ impl Compiler {
                      annotations: _,
                      module_io,
                  }| {
-                    let target = TargetInInstantiatedModule {
-                        instantiated_module: *module,
-                        target: Target::from(module_io),
-                    };
+                    let target = TargetInInstantiatedModuleOrGlobal::from_target(
+                        *module,
+                        Target::from(module_io),
+                    );
                     self.decl_conditions.insert(target, Interned::default());
                     trace_decls.push(self.make_trace_decl(*module, module_io.into()));
                     self.compile_value(target)
@@ -5433,7 +5552,7 @@ impl Compiler {
         }
     }
     pub fn compile(mut self) -> Compiled<Bundle> {
-        let base_module =
+        let mut base_module =
             *self.compile_module(InstantiatedModule::Base(self.base_module).intern_sized());
         self.process_assignments();
         self.process_registers();
@@ -5441,18 +5560,24 @@ impl Compiler {
         let clocks_triggered = self.process_clocks();
         self.insns
             .push(Insn::Return, self.base_module.source_location());
+        base_module.trace_decls.children = self
+            .global_trace_decls
+            .into_iter()
+            .chain(base_module.trace_decls.children)
+            .collect();
         Compiled {
             insns: Insns::from(self.insns).intern_sized(),
             base_module,
             extern_modules: Intern::intern_owned(self.extern_modules),
             io: Instance::new_unchecked(
                 ScopedNameId(
-                    NameId("<simulator>".intern(), Id::new()),
+                    NameId("<simulator>".intern(), Id::new()).into(),
                     self.original_base_module.name_id(),
                 ),
                 self.original_base_module,
                 self.original_base_module.source_location(),
             ),
+            global_io: Interned::from_iter(self.global_io),
             traces: SimTraces(Intern::intern_owned(self.traces.0)),
             trace_memories: Interned::from_iter(self.memories.iter().map(
                 |&Memory {
@@ -5479,6 +5604,7 @@ pub struct Compiled<T: BundleType> {
     pub(crate) base_module: CompiledModule,
     pub(crate) extern_modules: Interned<[CompiledExternModule]>,
     pub(crate) io: Instance<T>,
+    pub(crate) global_io: Interned<[(SimIoForGlobal, CompiledValue<CanonicalType>)]>,
     pub(crate) traces: SimTraces<Interned<[SimTrace<SimTraceKind, ()>]>>,
     pub(crate) trace_memories: Interned<[(StatePartIndex<StatePartKindMemories>, TraceMem)]>,
     pub(crate) clocks_triggered: Interned<[StatePartIndex<StatePartKindSmallSlots>]>,
@@ -5494,6 +5620,7 @@ impl<T: BundleType> Compiled<T> {
             base_module,
             extern_modules,
             io,
+            global_io,
             traces,
             trace_memories,
             clocks_triggered,
@@ -5503,6 +5630,7 @@ impl<T: BundleType> Compiled<T> {
             base_module,
             extern_modules,
             io: Instance::from_canonical(io.canonical()),
+            global_io,
             traces,
             trace_memories,
             clocks_triggered,
@@ -5514,6 +5642,7 @@ impl<T: BundleType> Compiled<T> {
             base_module,
             extern_modules,
             io,
+            global_io,
             traces,
             trace_memories,
             clocks_triggered,
@@ -5523,6 +5652,7 @@ impl<T: BundleType> Compiled<T> {
             base_module,
             extern_modules,
             io: Instance::from_canonical(io.canonical()),
+            global_io,
             traces,
             trace_memories,
             clocks_triggered,
diff --git a/crates/fayalite/src/sim/vcd.rs b/crates/fayalite/src/sim/vcd.rs
index 09e7d66..17ad206 100644
--- a/crates/fayalite/src/sim/vcd.rs
+++ b/crates/fayalite/src/sim/vcd.rs
@@ -9,11 +9,11 @@ use crate::{
     prelude::PhantomConst,
     sim::{
         TraceArray, TraceAsyncReset, TraceBool, TraceBundle, TraceClock, TraceDecl,
-        TraceEnumDiscriminant, TraceEnumWithFields, TraceFieldlessEnum, TraceInstance,
-        TraceLocation, TraceMem, TraceMemPort, TraceMemoryId, TraceMemoryLocation, TraceModule,
-        TraceModuleIO, TracePhantomConst, TraceReg, TraceSInt, TraceScalar, TraceScalarId,
-        TraceScope, TraceSimOnly, TraceSyncReset, TraceTraceAsString, TraceUInt, TraceWire,
-        TraceWriter, TraceWriterDecls,
+        TraceEnumDiscriminant, TraceEnumWithFields, TraceFieldlessEnum, TraceFormalInput,
+        TraceInstance, TraceLocation, TraceMem, TraceMemPort, TraceMemoryId, TraceMemoryLocation,
+        TraceModule, TraceModuleIO, TracePhantomConst, TraceReg, TraceSInt, TraceScalar,
+        TraceScalarId, TraceScope, TraceSimOnly, TraceSyncReset, TraceTraceAsString, TraceUInt,
+        TraceWire, TraceWriter, TraceWriterDecls,
         time::{SimDuration, SimInstant},
         value::DynSimOnlyValue,
     },
@@ -766,6 +766,7 @@ impl WriteTrace for TraceScope {
             Self::Wire(v) => v.write_trace(writer, arg),
             Self::Reg(v) => v.write_trace(writer, arg),
             Self::ModuleIO(v) => v.write_trace(writer, arg),
+            Self::FormalInput(v) => v.write_trace(writer, arg),
             Self::Bundle(v) => v.write_trace(writer, arg),
             Self::Array(v) => v.write_trace(writer, arg),
             Self::EnumWithFields(v) => v.write_trace(writer, arg),
@@ -963,6 +964,27 @@ impl WriteTrace for TraceModuleIO {
     }
 }
 
+impl WriteTrace for TraceFormalInput {
+    fn write_trace<W: io::Write, A: Arg>(self, writer: &mut W, mut arg: A) -> io::Result<()> {
+        let ArgModuleBody { properties, scope } = arg.module_body();
+        let Self {
+            name: _,
+            child,
+            formal_input: _,
+        } = self;
+        child.write_trace(
+            writer,
+            ArgInType {
+                source_var_type: "wire",
+                sink_var_type: "wire",
+                duplex_var_type: "wire",
+                properties,
+                scope: Some(scope),
+            },
+        )
+    }
+}
+
 impl WriteTrace for TraceBundle {
     fn write_trace<W: io::Write, A: Arg>(self, writer: &mut W, mut arg: A) -> io::Result<()> {
         let ArgInType {
diff --git a/crates/fayalite/src/testing.rs b/crates/fayalite/src/testing.rs
index bc7a0b1..cb9db9c 100644
--- a/crates/fayalite/src/testing.rs
+++ b/crates/fayalite/src/testing.rs
@@ -12,11 +12,13 @@ use crate::{
     bundle::BundleType,
     firrtl::ExportOptions,
     module::Module,
-    util::HashMap,
+    sim::{Simulation, vcd::VcdWriterDecls},
+    util::{HashMap, RcWriter},
 };
 use serde::{Deserialize, Serialize};
 use std::{
     fmt::{self, Write},
+    panic::Location,
     path::{Path, PathBuf},
     process::Command,
     sync::{Mutex, OnceLock},
@@ -222,3 +224,190 @@ pub fn assert_formal<M: AsRef<Module<T>>, T: BundleType>(
     )
     .expect("testing::assert_formal() failed");
 }
+
+pub struct CheckedVcdOutput {
+    writer: Option<RcWriter>,
+    expected_path: PathBuf,
+    expected_contents: Result<String, (Option<PathBuf>, std::io::Error)>,
+    location: &'static Location<'static>,
+}
+
+impl CheckedVcdOutput {
+    #[must_use]
+    #[track_caller]
+    pub fn new<T: BundleType>(sim: &mut Simulation<T>, expected_path: PathBuf) -> Self {
+        let writer = RcWriter::default();
+        sim.add_trace_writer(VcdWriterDecls::new(writer.clone()));
+        Self {
+            writer: Some(writer),
+            expected_contents: std::fs::read_to_string(&expected_path).map_err(|e| {
+                eprintln!(
+                    "error: failed to read expected VCD from: {}",
+                    expected_path.display(),
+                );
+                (std::env::current_dir().ok(), e)
+            }),
+            expected_path,
+            location: Location::caller(),
+        }
+    }
+    #[must_use]
+    #[track_caller]
+    #[doc(hidden)]
+    pub fn __checked_vcd_output_macro_helper<T: BundleType>(
+        sim: &mut Simulation<T>,
+        cargo_manifest_dir: &'static str,
+        path: &'static str,
+    ) -> Self {
+        Self::new(sim, Path::new(cargo_manifest_dir).join(path))
+    }
+    pub fn with_vcd_output<R>(&self, f: impl FnOnce(&str) -> R) -> R {
+        let Some(writer) = &self.writer else {
+            unreachable!();
+        };
+        writer.clone().borrow(|output| {
+            let Ok(output) = str::from_utf8(output) else {
+                unreachable!("VcdWriter writes valid UTF-8");
+            };
+            f(output)
+        })
+    }
+    #[track_caller]
+    pub fn finish(mut self) {
+        let Ok(()) = self.finish_impl(|msg| panic!("{msg}"));
+    }
+    fn finish_impl<E>(
+        &mut self,
+        error: impl FnOnce(std::fmt::Arguments<'_>) -> E,
+    ) -> Result<(), E> {
+        let Self {
+            writer: Some(writer),
+            expected_path,
+            expected_contents,
+            location,
+        } = self
+        else {
+            // already finished
+            return Ok(());
+        };
+        let Ok(vcd) = String::from_utf8(writer.take()) else {
+            unreachable!("VcdWriter writes valid UTF-8");
+        };
+        let expected_path_d = expected_path.display();
+        if expected_contents
+            .as_ref()
+            .is_ok_and(|expected_contents| *expected_contents == vcd)
+        {
+            // avoid written output from being split from threads interleaving writes to stdout
+            let _stdout = std::io::stderr().lock();
+            // use println to get output captured by tests
+            println!("\n{location}: generated VCD matches the expected VCD in {expected_path_d}");
+            return Ok(());
+        }
+        // avoid written output from being split from threads interleaving writes to stderr
+        let _stderr = std::io::stderr().lock();
+        let error = |msg: std::fmt::Arguments<'_>| {
+            // print msg at both beginning and end so it's easier to find when the vcd is huge
+            Err(error(format_args!(
+                "\n{msg}####### VCD:\n{vcd}\n#######\n{msg}"
+            )))
+        };
+        let error = |msg: std::fmt::Arguments<'_>| match &*expected_contents {
+            Ok(_) => error(format_args!(
+                "{location}: generated VCD doesn't match the expected VCD in {expected_path_d}\n\
+                {msg}",
+            )),
+            Err((Some(current_dir), e)) => error(format_args!(
+                "{location}: generated VCD doesn't match the expected VCD in {expected_path_d}\n\
+                error: failed to read: {e}\n\
+                current dir: {current_dir}\n\
+                {msg}",
+                current_dir = current_dir.display(),
+            )),
+            Err((None, e)) => error(format_args!(
+                "{location}: generated VCD doesn't match the expected VCD in {expected_path_d}\n\
+                error: failed to read: {e}\n\
+                {msg}",
+            )),
+        };
+        const OVERWRITE_VAR_NAME: &str = "OVERWRITE_EXPECTED_VCD";
+        const OVERWRITE_VAR_VALUE: &str = "overwrite";
+        match std::env::var_os(OVERWRITE_VAR_NAME) {
+            Some(v) if v == OVERWRITE_VAR_VALUE => match std::fs::write(&expected_path, &vcd) {
+                Ok(()) => error(format_args!(
+                    "warning: since `{OVERWRITE_VAR_NAME}={OVERWRITE_VAR_VALUE}` is set -- writing the generated VCD to {expected_path_d}\n"
+                )),
+                Err(e) => error(format_args!(
+                    "error: since `{OVERWRITE_VAR_NAME}={OVERWRITE_VAR_VALUE}` is set -- tried to write the generated VCD to {expected_path_d}\n\
+                    error: failed to write: {e}"
+                )),
+            },
+            _ => error(format_args!(
+                "note: rerun the test with the environment variable `{OVERWRITE_VAR_NAME}={OVERWRITE_VAR_VALUE}`\n\
+                to update the expected output to match the generated output.\n"
+            )),
+        }
+    }
+}
+
+impl Drop for CheckedVcdOutput {
+    #[track_caller]
+    fn drop(&mut self) {
+        let _ = self.finish_impl(|msg| {
+            if std::thread::panicking() {
+                eprintln!("{msg}"); // use eprintln to get output captured by tests
+            } else {
+                panic!("{msg}");
+            }
+        });
+    }
+}
+
+#[macro_export]
+/// Use in tests to check that [`Simulation`] generates the expected VCD traces, by comparing to a `.vcd` file containing the expected traces.
+///
+/// Use like so:
+/// ```
+/// # use fayalite::prelude::*;
+/// #
+/// # #[hdl_module]
+/// # fn my_module() {
+/// #     #[hdl]
+/// #     let a: UInt<8> = m.input();
+/// #     #[hdl]
+/// #     let b: UInt<8> = m.output();
+/// #     connect(b, 0u8);
+/// #     #[hdl]
+/// #     if a.cmp_eq(100u8) {
+/// #         connect(b, 42u8);
+/// #     }
+/// # }
+/// // inside your #[test] fn my_test():
+///
+/// // get the module to simulate:
+/// let m = my_module();
+/// // create a simulation of the module:
+/// let mut sim = Simulation::new(m);
+/// // set up the expected VCD traces, the given .vcd path is relative to env!("CARGO_MANIFEST_DIR")
+/// let _checked_vcd_output = checked_vcd_output!(
+///     &mut sim,
+///     "tests/expected/my_test.vcd",
+/// );
+/// // now run the simulation like normal:
+/// sim.write(sim.io().a, 0u8);
+/// assert_eq!(sim.read(sim.io().b).as_int(), 0);
+/// sim.advance_time(SimDuration::from_micros(1));
+/// sim.write(sim.io().a, 100u8);
+/// assert_eq!(sim.read(sim.io().b).as_int(), 42);
+/// ```
+macro_rules! checked_vcd_output {
+    ($sim:expr, $path_relative_to_manifest_dir:expr $(,)?) => {
+        $crate::testing::CheckedVcdOutput::__checked_vcd_output_macro_helper(
+            $sim,
+            $crate::__std::env!("CARGO_MANIFEST_DIR"),
+            $crate::__std::concat!($path_relative_to_manifest_dir),
+        )
+    };
+}
+
+pub use checked_vcd_output;
diff --git a/crates/fayalite/src/vendor/xilinx/yosys_nextpnr_prjxray.rs b/crates/fayalite/src/vendor/xilinx/yosys_nextpnr_prjxray.rs
index 2d498e7..620e78c 100644
--- a/crates/fayalite/src/vendor/xilinx/yosys_nextpnr_prjxray.rs
+++ b/crates/fayalite/src/vendor/xilinx/yosys_nextpnr_prjxray.rs
@@ -595,6 +595,9 @@ impl<W: fmt::Write> Visitor for XdcFileWriter<W> {
                         v,
                         instance.source_location(),
                     )? {},
+                    TargetBase::FormalInput(_) | TargetBase::SimIoForGlobal(_) => {
+                        unreachable!("base.is_valid_annotation_target() is known to be false")
+                    }
                 }
             }
         }
diff --git a/crates/fayalite/src/wire.rs b/crates/fayalite/src/wire.rs
index a350d9a..d167c5f 100644
--- a/crates/fayalite/src/wire.rs
+++ b/crates/fayalite/src/wire.rs
@@ -58,11 +58,13 @@ impl<T: Type> Wire<T> {
             ty: T::from_canonical(ty),
         }
     }
+    #[track_caller]
     pub fn new_unchecked(
         scoped_name: ScopedNameId,
         source_location: SourceLocation,
         ty: T,
     ) -> Self {
+        scoped_name.0.assert_is_name_id();
         Self {
             name: scoped_name,
             source_location,
@@ -76,7 +78,7 @@ impl<T: Type> Wire<T> {
         self.containing_module_name_id().0
     }
     pub fn containing_module_name_id(&self) -> NameId {
-        self.name.0
+        self.name.0.unwrap_name_id()
     }
     pub fn name(&self) -> Interned<str> {
         self.name_id().0
diff --git a/crates/fayalite/tests/expected/my_test.md b/crates/fayalite/tests/expected/my_test.md
new file mode 100644
index 0000000..a44a873
--- /dev/null
+++ b/crates/fayalite/tests/expected/my_test.md
@@ -0,0 +1,4 @@
+<!-- SPDX-License-Identifier: LGPL-3.0-or-later -->
+<!-- See Notices.txt for copyright information -->
+
+`my_test.vcd` is used in the doctest of `fayalite::testing::checked_vcd_output`
\ No newline at end of file
diff --git a/crates/fayalite/tests/expected/my_test.vcd b/crates/fayalite/tests/expected/my_test.vcd
new file mode 100644
index 0000000..3df1caf
--- /dev/null
+++ b/crates/fayalite/tests/expected/my_test.vcd
@@ -0,0 +1,13 @@
+$timescale 1 ps $end
+$scope module my_module $end
+$var wire 8 gAF7X a $end
+$var wire 8 QS=a/ b $end
+$upscope $end
+$enddefinitions $end
+$dumpvars
+b0 gAF7X
+b0 QS=a/
+$end
+#1000000
+b1100100 gAF7X
+b101010 QS=a/
diff --git a/crates/fayalite/tests/module.rs b/crates/fayalite/tests/module.rs
index 5c62933..aa028f4 100644
--- a/crates/fayalite/tests/module.rs
+++ b/crates/fayalite/tests/module.rs
@@ -3683,20 +3683,176 @@ circuit check_formal: %[[
         input pred1: UInt<1> @[module-XXXXXXXXXX.rs 6:1]
         input pred2: UInt<1> @[module-XXXXXXXXXX.rs 7:1]
         input pred3: UInt<1> @[module-XXXXXXXXXX.rs 8:1]
-        inst formal_reset of formal_reset @[formal.rs 185:24]
+        inst formal_reset of formal_reset @[builtin 1:1]
         assert(clk, pred1, and(en1, not(formal_reset.rst)), "en check 1") @[module-XXXXXXXXXX.rs 9:1]
-        inst formal_reset_1 of formal_reset @[formal.rs 185:24]
-        assume(clk, pred2, and(en2, not(formal_reset_1.rst)), "en check 2") @[module-XXXXXXXXXX.rs 10:1]
-        inst formal_reset_2 of formal_reset @[formal.rs 185:24]
-        cover(clk, pred3, and(en3, not(formal_reset_2.rst)), "en check 3") @[module-XXXXXXXXXX.rs 11:1]
-        inst formal_reset_3 of formal_reset @[formal.rs 185:24]
-        assert(clk, pred1, and(UInt<1>(0h1), not(formal_reset_3.rst)), "check 1") @[module-XXXXXXXXXX.rs 12:1]
-        inst formal_reset_4 of formal_reset @[formal.rs 185:24]
-        assume(clk, pred2, and(UInt<1>(0h1), not(formal_reset_4.rst)), "check 2") @[module-XXXXXXXXXX.rs 13:1]
-        inst formal_reset_5 of formal_reset @[formal.rs 185:24]
-        cover(clk, pred3, and(UInt<1>(0h1), not(formal_reset_5.rst)), "check 3") @[module-XXXXXXXXXX.rs 14:1]
-    extmodule formal_reset: @[formal.rs 169:5]
-        output rst: UInt<1> @[formal.rs 172:32]
+        assume(clk, pred2, and(en2, not(formal_reset.rst)), "en check 2") @[module-XXXXXXXXXX.rs 10:1]
+        cover(clk, pred3, and(en3, not(formal_reset.rst)), "en check 3") @[module-XXXXXXXXXX.rs 11:1]
+        assert(clk, pred1, and(UInt<1>(0h1), not(formal_reset.rst)), "check 1") @[module-XXXXXXXXXX.rs 12:1]
+        assume(clk, pred2, and(UInt<1>(0h1), not(formal_reset.rst)), "check 2") @[module-XXXXXXXXXX.rs 13:1]
+        cover(clk, pred3, and(UInt<1>(0h1), not(formal_reset.rst)), "check 3") @[module-XXXXXXXXXX.rs 14:1]
+    extmodule formal_reset: @[builtin 1:1]
+        output rst: UInt<1> @[builtin 1:1]
+        defname = __fayalite_formal_reset
+"#,
+    };
+}
+
+#[hdl_module(outline_generated)]
+pub fn check_formal_input() {
+    #[hdl]
+    let bool_in: Bool = m.input();
+    #[hdl]
+    let bool_out: Bool = m.output();
+    #[hdl]
+    let any_const_out1: Bool = m.output();
+    #[hdl]
+    let any_const_out2: UInt<16> = m.output();
+    #[hdl]
+    let any_const_out3: SInt<12> = m.output();
+    #[hdl]
+    let any_seq_out: UInt<10> = m.output();
+    #[hdl]
+    let all_const_out: UInt<10> = m.output();
+    #[hdl]
+    let all_seq_out: UInt<10> = m.output();
+
+    #[hdl]
+    let bool_reg = reg_builder()
+        .clock_domain(
+            #[hdl]
+            ClockDomain {
+                clk: formal_global_clock(),
+                rst: formal_reset(),
+            },
+        )
+        .reset(false);
+
+    connect(bool_reg, bool_in);
+    connect(bool_out, bool_reg);
+    connect(any_const_out1, any_const(StaticType::TYPE));
+    connect(any_const_out2, any_const(StaticType::TYPE));
+    connect(any_const_out3, any_const(StaticType::TYPE));
+    connect(any_seq_out, any_seq(StaticType::TYPE));
+    connect(all_const_out, all_const(StaticType::TYPE));
+    connect(all_seq_out, all_seq(StaticType::TYPE));
+}
+
+#[test]
+fn test_formal_input() {
+    let _n = SourceLocation::normalize_files_for_tests();
+    let m = check_formal_input();
+    dbg!(m);
+    #[rustfmt::skip] // work around https://github.com/rust-lang/rustfmt/issues/6161
+    assert_export_firrtl! {
+        m =>
+        "/test/check_formal_input.fir": r#"FIRRTL version 3.2.0
+circuit check_formal_input: %[[
+  {
+    "class": "firrtl.AttributeAnnotation",
+    "description": "gclk",
+    "target": "~check_formal_input|check_formal_input>formal_global_clock"
+  },
+  {
+    "class": "firrtl.transforms.DontTouchAnnotation",
+    "target": "~check_formal_input|check_formal_input>formal_global_clock"
+  },
+  {
+    "class": "firrtl.AttributeAnnotation",
+    "description": "anyconst",
+    "target": "~check_formal_input|check_formal_input>any_const"
+  },
+  {
+    "class": "firrtl.transforms.DontTouchAnnotation",
+    "target": "~check_formal_input|check_formal_input>any_const"
+  },
+  {
+    "class": "firrtl.AttributeAnnotation",
+    "description": "anyconst",
+    "target": "~check_formal_input|check_formal_input>any_const_1"
+  },
+  {
+    "class": "firrtl.transforms.DontTouchAnnotation",
+    "target": "~check_formal_input|check_formal_input>any_const_1"
+  },
+  {
+    "class": "firrtl.AttributeAnnotation",
+    "description": "anyconst",
+    "target": "~check_formal_input|check_formal_input>any_const_2"
+  },
+  {
+    "class": "firrtl.transforms.DontTouchAnnotation",
+    "target": "~check_formal_input|check_formal_input>any_const_2"
+  },
+  {
+    "class": "firrtl.AttributeAnnotation",
+    "description": "anyseq",
+    "target": "~check_formal_input|check_formal_input>any_seq"
+  },
+  {
+    "class": "firrtl.transforms.DontTouchAnnotation",
+    "target": "~check_formal_input|check_formal_input>any_seq"
+  },
+  {
+    "class": "firrtl.AttributeAnnotation",
+    "description": "allconst",
+    "target": "~check_formal_input|check_formal_input>all_const"
+  },
+  {
+    "class": "firrtl.transforms.DontTouchAnnotation",
+    "target": "~check_formal_input|check_formal_input>all_const"
+  },
+  {
+    "class": "firrtl.AttributeAnnotation",
+    "description": "allseq",
+    "target": "~check_formal_input|check_formal_input>all_seq"
+  },
+  {
+    "class": "firrtl.transforms.DontTouchAnnotation",
+    "target": "~check_formal_input|check_formal_input>all_seq"
+  },
+  {
+    "class": "firrtl.transforms.BlackBoxInlineAnno",
+    "name": "fayalite_formal_reset.v",
+    "text": "module __fayalite_formal_reset(output rst);\n    assign rst = $initstate;\nendmodule\n",
+    "target": "~check_formal_input|formal_reset"
+  }
+]]
+    type Ty0 = {clk: Clock, rst: UInt<1>}
+    type Ty1 = {rst: UInt<1>}
+    module check_formal_input: @[module-XXXXXXXXXX.rs 1:1]
+        input bool_in: UInt<1> @[module-XXXXXXXXXX.rs 2:1]
+        output bool_out: UInt<1> @[module-XXXXXXXXXX.rs 3:1]
+        output any_const_out1: UInt<1> @[module-XXXXXXXXXX.rs 4:1]
+        output any_const_out2: UInt<16> @[module-XXXXXXXXXX.rs 5:1]
+        output any_const_out3: SInt<12> @[module-XXXXXXXXXX.rs 6:1]
+        output any_seq_out: UInt<10> @[module-XXXXXXXXXX.rs 7:1]
+        output all_const_out: UInt<10> @[module-XXXXXXXXXX.rs 8:1]
+        output all_seq_out: UInt<10> @[module-XXXXXXXXXX.rs 9:1]
+        wire _bundle_literal_expr_1: Ty0
+        connect _bundle_literal_expr_1.clk, asClock(UInt<1>(0h0))
+        connect _bundle_literal_expr_1.rst, UInt<1>(0h0)
+        reg formal_global_clock: UInt<1>, _bundle_literal_expr_1.clk @[builtin 1:1]
+        inst formal_reset of formal_reset @[builtin 1:1]
+        reg any_const: UInt<1>, _bundle_literal_expr_1.clk @[module-XXXXXXXXXX.rs 13:1]
+        reg any_const_1: UInt<16>, _bundle_literal_expr_1.clk @[module-XXXXXXXXXX.rs 15:1]
+        reg any_const_2: SInt<12>, _bundle_literal_expr_1.clk @[module-XXXXXXXXXX.rs 17:1]
+        reg any_seq: UInt<10>, _bundle_literal_expr_1.clk @[module-XXXXXXXXXX.rs 19:1]
+        reg all_const: UInt<10>, _bundle_literal_expr_1.clk @[module-XXXXXXXXXX.rs 21:1]
+        reg all_seq: UInt<10>, _bundle_literal_expr_1.clk @[module-XXXXXXXXXX.rs 23:1]
+        wire _bundle_literal_expr: Ty0
+        connect _bundle_literal_expr.clk, asClock(formal_global_clock)
+        connect _bundle_literal_expr.rst, formal_reset.rst
+        regreset bool_reg: UInt<1>, _bundle_literal_expr.clk, _bundle_literal_expr.rst, UInt<1>(0h0) @[module-XXXXXXXXXX.rs 10:1]
+        connect bool_reg, bool_in @[module-XXXXXXXXXX.rs 11:1]
+        connect bool_out, bool_reg @[module-XXXXXXXXXX.rs 12:1]
+        connect any_const_out1, any_const @[module-XXXXXXXXXX.rs 14:1]
+        connect any_const_out2, any_const_1 @[module-XXXXXXXXXX.rs 16:1]
+        connect any_const_out3, any_const_2 @[module-XXXXXXXXXX.rs 18:1]
+        connect any_seq_out, any_seq @[module-XXXXXXXXXX.rs 20:1]
+        connect all_const_out, all_const @[module-XXXXXXXXXX.rs 22:1]
+        connect all_seq_out, all_seq @[module-XXXXXXXXXX.rs 24:1]
+    extmodule formal_reset: @[builtin 1:1]
+        output rst: UInt<1> @[builtin 1:1]
         defname = __fayalite_formal_reset
 "#,
     };
diff --git a/crates/fayalite/tests/sim.rs b/crates/fayalite/tests/sim.rs
index 80ae4c2..c527ea1 100644
--- a/crates/fayalite/tests/sim.rs
+++ b/crates/fayalite/tests/sim.rs
@@ -5,6 +5,7 @@ use bitvec::{order::Lsb0, view::BitView};
 use fayalite::{
     assert_export_firrtl,
     firrtl::ExportOptions,
+    formal::FormalInputKind,
     memory::{ReadStruct, ReadWriteStruct, WriteStruct, splat_mask},
     module::{
         instance_with_loc, memory_with_init_and_loc, reg_builder_with_loc,
@@ -16,7 +17,12 @@ use fayalite::{
     ty::SimValueDebug,
     util::{RcWriter, ready_valid::queue},
 };
-use std::{collections::BTreeMap, num::NonZeroUsize, rc::Rc};
+use std::{
+    collections::BTreeMap,
+    num::NonZeroUsize,
+    panic::{AssertUnwindSafe, catch_unwind, resume_unwind},
+    rc::Rc,
+};
 
 #[hdl_module(outline_generated)]
 pub fn connect_const() {
@@ -3610,3 +3616,119 @@ circuit sim_trace_as_string: %[[
 ",
     };
 }
+
+#[hdl_module(outline_generated)]
+pub fn formal_counter(max_count: u8, asserted_max_count: u8) {
+    #[hdl]
+    let cd = wire();
+    connect(
+        cd,
+        #[hdl]
+        ClockDomain {
+            clk: formal_global_clock(),
+            rst: formal_reset(),
+        },
+    );
+    #[hdl]
+    let count_reg: UInt<8> = reg_builder().clock_domain(cd).reset(0u8);
+    #[hdl]
+    if count_reg.cmp_lt(max_count) {
+        connect_any(count_reg, count_reg + 1u8);
+    } else {
+        connect(count_reg, 0u8);
+    }
+    #[hdl]
+    let count: UInt<8> = m.output();
+    connect(count, count_reg);
+    hdl_assert(cd.clk, count_reg.cmp_le(asserted_max_count), "");
+    #[hdl]
+    let any_seq_out: UInt<16> = m.output();
+    connect(any_seq_out, any_seq(any_seq_out.ty()));
+}
+
+#[hdl]
+#[test]
+fn test_formal_counter() {
+    let _n = SourceLocation::normalize_files_for_tests();
+    let mut sim = Simulation::new(formal_counter(10, 10));
+    let _checked_vcd_output =
+        checked_vcd_output!(&mut sim, "tests/sim/expected/test_formal_counter.vcd");
+    let Some((_, any_seq_in)) = sim
+        .global_io()
+        .into_iter()
+        .find(|(global, _)| global.kind() == FormalInputKind::AnySeq)
+    else {
+        panic!("can't find any_seq");
+    };
+    let any_seq_in = Expr::<UInt<16>>::from_canonical(any_seq_in);
+    sim.write_clock(formal_global_clock(), false);
+    sim.write_reset(formal_reset(), true);
+    sim.write(any_seq_in, 0u16);
+    sim.advance_time(SimDuration::from_micros(1));
+    assert_eq!(sim.read(sim.io().any_seq_out).as_int(), 0u16);
+    sim.write_clock(formal_global_clock(), true);
+    sim.write(any_seq_in, 1234u16);
+    assert_eq!(sim.read(sim.io().any_seq_out).as_int(), 1234u16);
+    assert_eq!(sim.read(sim.io().count).as_int(), 0);
+    sim.write_reset(formal_reset(), false);
+    sim.advance_time(SimDuration::from_micros(1));
+    for i in 0..32u8 {
+        assert_eq!(i % 10, sim.read(sim.io().count).as_int());
+        sim.write_clock(formal_global_clock(), false);
+        sim.advance_time(SimDuration::from_micros(1));
+        sim.write_clock(formal_global_clock(), true);
+        sim.advance_time(SimDuration::from_micros(1));
+    }
+    let sim_debug = format!("{sim:#?}");
+    println!("#######\n{sim_debug}\n#######");
+    if sim_debug != include_str!("sim/expected/test_formal_counter.txt") {
+        panic!();
+    }
+}
+
+#[cfg(panic = "unwind")]
+#[hdl]
+#[test]
+fn test_formal_counter_assert() {
+    let _n = SourceLocation::normalize_files_for_tests();
+    let mut sim = Simulation::new(formal_counter(10, 9));
+    let _checked_vcd_output = checked_vcd_output!(
+        &mut sim,
+        "tests/sim/expected/test_formal_counter_assert.vcd"
+    );
+    let Some((_, any_seq_in)) = sim
+        .global_io()
+        .into_iter()
+        .find(|(global, _)| global.kind() == FormalInputKind::AnySeq)
+    else {
+        panic!("can't find any_seq");
+    };
+    let any_seq_in = Expr::<UInt<16>>::from_canonical(any_seq_in);
+    sim.write_clock(formal_global_clock(), false);
+    sim.write_reset(formal_reset(), true);
+    sim.write(any_seq_in, 0u16);
+    sim.advance_time(SimDuration::from_micros(1));
+    assert_eq!(sim.read(sim.io().any_seq_out).as_int(), 0u16);
+    sim.write_clock(formal_global_clock(), true);
+    sim.write(any_seq_in, 1234u16);
+    assert_eq!(sim.read(sim.io().any_seq_out).as_int(), 1234u16);
+    assert_eq!(sim.read(sim.io().count).as_int(), 0);
+    sim.write_reset(formal_reset(), false);
+    sim.advance_time(SimDuration::from_micros(1));
+    for i in 0..32u8 {
+        assert_eq!(i % 10, sim.read(sim.io().count).as_int());
+        sim.write_clock(formal_global_clock(), false);
+        sim.advance_time(SimDuration::from_micros(1));
+        match catch_unwind(AssertUnwindSafe(|| {
+            sim.write_clock(formal_global_clock(), true);
+            sim.advance_time(SimDuration::from_micros(1));
+        })) {
+            Ok(()) => assert!(i < 9),
+            Err(e) => match e.downcast::<String>() {
+                Ok(e) if *e == "todo panic message" && i == 9 => break,
+                Ok(e) => resume_unwind(e),
+                Err(e) => resume_unwind(e),
+            },
+        }
+    }
+}
diff --git a/crates/fayalite/tests/sim/expected/array_rw.txt b/crates/fayalite/tests/sim/expected/array_rw.txt
index 271ec3c..b73d76a 100644
--- a/crates/fayalite/tests/sim/expected/array_rw.txt
+++ b/crates/fayalite/tests/sim/expected/array_rw.txt
@@ -497,6 +497,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/conditional_assignment_last.txt b/crates/fayalite/tests/sim/expected/conditional_assignment_last.txt
index 74c03a4..9badd6f 100644
--- a/crates/fayalite/tests/sim/expected/conditional_assignment_last.txt
+++ b/crates/fayalite/tests/sim/expected/conditional_assignment_last.txt
@@ -101,6 +101,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/connect_const.txt b/crates/fayalite/tests/sim/expected/connect_const.txt
index 8193fc5..96bdf13 100644
--- a/crates/fayalite/tests/sim/expected/connect_const.txt
+++ b/crates/fayalite/tests/sim/expected/connect_const.txt
@@ -77,6 +77,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/connect_const_reset.txt b/crates/fayalite/tests/sim/expected/connect_const_reset.txt
index 5a64923..828d687 100644
--- a/crates/fayalite/tests/sim/expected/connect_const_reset.txt
+++ b/crates/fayalite/tests/sim/expected/connect_const_reset.txt
@@ -106,6 +106,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/counter_async.txt b/crates/fayalite/tests/sim/expected/counter_async.txt
index 20d27ac..a628928 100644
--- a/crates/fayalite/tests/sim/expected/counter_async.txt
+++ b/crates/fayalite/tests/sim/expected/counter_async.txt
@@ -216,6 +216,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/counter_sync.txt b/crates/fayalite/tests/sim/expected/counter_sync.txt
index baa08e7..2957ef5 100644
--- a/crates/fayalite/tests/sim/expected/counter_sync.txt
+++ b/crates/fayalite/tests/sim/expected/counter_sync.txt
@@ -197,6 +197,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/duplicate_names.txt b/crates/fayalite/tests/sim/expected/duplicate_names.txt
index 76338e8..d705861 100644
--- a/crates/fayalite/tests/sim/expected/duplicate_names.txt
+++ b/crates/fayalite/tests/sim/expected/duplicate_names.txt
@@ -97,6 +97,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [],
         uninitialized_ios: {},
diff --git a/crates/fayalite/tests/sim/expected/enum_with_simple_body.txt b/crates/fayalite/tests/sim/expected/enum_with_simple_body.txt
index 6b5af1c..bb1ee17 100644
--- a/crates/fayalite/tests/sim/expected/enum_with_simple_body.txt
+++ b/crates/fayalite/tests/sim/expected/enum_with_simple_body.txt
@@ -465,6 +465,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/enums.txt b/crates/fayalite/tests/sim/expected/enums.txt
index d2da2d9..faccec5 100644
--- a/crates/fayalite/tests/sim/expected/enums.txt
+++ b/crates/fayalite/tests/sim/expected/enums.txt
@@ -1324,6 +1324,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/extern_module.txt b/crates/fayalite/tests/sim/expected/extern_module.txt
index 48a3af5..47dde8f 100644
--- a/crates/fayalite/tests/sim/expected/extern_module.txt
+++ b/crates/fayalite/tests/sim/expected/extern_module.txt
@@ -67,6 +67,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/extern_module2.txt b/crates/fayalite/tests/sim/expected/extern_module2.txt
index d488666..60fe795 100644
--- a/crates/fayalite/tests/sim/expected/extern_module2.txt
+++ b/crates/fayalite/tests/sim/expected/extern_module2.txt
@@ -72,6 +72,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/last_connect.txt b/crates/fayalite/tests/sim/expected/last_connect.txt
index c5d1341..4afa42c 100644
--- a/crates/fayalite/tests/sim/expected/last_connect.txt
+++ b/crates/fayalite/tests/sim/expected/last_connect.txt
@@ -464,6 +464,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/many_memories.txt b/crates/fayalite/tests/sim/expected/many_memories.txt
index 0d1a6db..ab58e47 100644
--- a/crates/fayalite/tests/sim/expected/many_memories.txt
+++ b/crates/fayalite/tests/sim/expected/many_memories.txt
@@ -3183,6 +3183,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/memories.txt b/crates/fayalite/tests/sim/expected/memories.txt
index c96da4f..155ba10 100644
--- a/crates/fayalite/tests/sim/expected/memories.txt
+++ b/crates/fayalite/tests/sim/expected/memories.txt
@@ -579,6 +579,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/memories2.txt b/crates/fayalite/tests/sim/expected/memories2.txt
index 1f78fcf..9bd19f6 100644
--- a/crates/fayalite/tests/sim/expected/memories2.txt
+++ b/crates/fayalite/tests/sim/expected/memories2.txt
@@ -607,6 +607,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/memories3.txt b/crates/fayalite/tests/sim/expected/memories3.txt
index 75720a8..921a06e 100644
--- a/crates/fayalite/tests/sim/expected/memories3.txt
+++ b/crates/fayalite/tests/sim/expected/memories3.txt
@@ -1495,6 +1495,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/mod1.txt b/crates/fayalite/tests/sim/expected/mod1.txt
index a1de89a..73604ce 100644
--- a/crates/fayalite/tests/sim/expected/mod1.txt
+++ b/crates/fayalite/tests/sim/expected/mod1.txt
@@ -225,6 +225,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/phantom_const.txt b/crates/fayalite/tests/sim/expected/phantom_const.txt
index c9adae4..b13d77b 100644
--- a/crates/fayalite/tests/sim/expected/phantom_const.txt
+++ b/crates/fayalite/tests/sim/expected/phantom_const.txt
@@ -215,6 +215,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_1_false_false.txt b/crates/fayalite/tests/sim/expected/queue_1_false_false.txt
index e349bbd..61deb42 100644
--- a/crates/fayalite/tests/sim/expected/queue_1_false_false.txt
+++ b/crates/fayalite/tests/sim/expected/queue_1_false_false.txt
@@ -1201,6 +1201,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_1_false_true.txt b/crates/fayalite/tests/sim/expected/queue_1_false_true.txt
index 3a31636..ea6cfc6 100644
--- a/crates/fayalite/tests/sim/expected/queue_1_false_true.txt
+++ b/crates/fayalite/tests/sim/expected/queue_1_false_true.txt
@@ -1180,6 +1180,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_1_true_false.txt b/crates/fayalite/tests/sim/expected/queue_1_true_false.txt
index 9dd3851..16ec241 100644
--- a/crates/fayalite/tests/sim/expected/queue_1_true_false.txt
+++ b/crates/fayalite/tests/sim/expected/queue_1_true_false.txt
@@ -1211,6 +1211,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_1_true_true.txt b/crates/fayalite/tests/sim/expected/queue_1_true_true.txt
index 5762f24..7d6a029 100644
--- a/crates/fayalite/tests/sim/expected/queue_1_true_true.txt
+++ b/crates/fayalite/tests/sim/expected/queue_1_true_true.txt
@@ -1190,6 +1190,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_2_false_false.txt b/crates/fayalite/tests/sim/expected/queue_2_false_false.txt
index c2cb51a..f41afd8 100644
--- a/crates/fayalite/tests/sim/expected/queue_2_false_false.txt
+++ b/crates/fayalite/tests/sim/expected/queue_2_false_false.txt
@@ -1219,6 +1219,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_2_false_true.txt b/crates/fayalite/tests/sim/expected/queue_2_false_true.txt
index f229451..0371894 100644
--- a/crates/fayalite/tests/sim/expected/queue_2_false_true.txt
+++ b/crates/fayalite/tests/sim/expected/queue_2_false_true.txt
@@ -1198,6 +1198,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_2_true_false.txt b/crates/fayalite/tests/sim/expected/queue_2_true_false.txt
index e137316..b646158 100644
--- a/crates/fayalite/tests/sim/expected/queue_2_true_false.txt
+++ b/crates/fayalite/tests/sim/expected/queue_2_true_false.txt
@@ -1229,6 +1229,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_2_true_true.txt b/crates/fayalite/tests/sim/expected/queue_2_true_true.txt
index 5203027..c1b0349 100644
--- a/crates/fayalite/tests/sim/expected/queue_2_true_true.txt
+++ b/crates/fayalite/tests/sim/expected/queue_2_true_true.txt
@@ -1208,6 +1208,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_3_false_false.txt b/crates/fayalite/tests/sim/expected/queue_3_false_false.txt
index f5641ce..3c8b1c1 100644
--- a/crates/fayalite/tests/sim/expected/queue_3_false_false.txt
+++ b/crates/fayalite/tests/sim/expected/queue_3_false_false.txt
@@ -1248,6 +1248,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_3_false_true.txt b/crates/fayalite/tests/sim/expected/queue_3_false_true.txt
index cde5489..46b99af 100644
--- a/crates/fayalite/tests/sim/expected/queue_3_false_true.txt
+++ b/crates/fayalite/tests/sim/expected/queue_3_false_true.txt
@@ -1227,6 +1227,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_3_true_false.txt b/crates/fayalite/tests/sim/expected/queue_3_true_false.txt
index d943150..7583b68 100644
--- a/crates/fayalite/tests/sim/expected/queue_3_true_false.txt
+++ b/crates/fayalite/tests/sim/expected/queue_3_true_false.txt
@@ -1258,6 +1258,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_3_true_true.txt b/crates/fayalite/tests/sim/expected/queue_3_true_true.txt
index 4a0f664..2391673 100644
--- a/crates/fayalite/tests/sim/expected/queue_3_true_true.txt
+++ b/crates/fayalite/tests/sim/expected/queue_3_true_true.txt
@@ -1237,6 +1237,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_4_false_false.txt b/crates/fayalite/tests/sim/expected/queue_4_false_false.txt
index 4e0a067..f6c7d4c 100644
--- a/crates/fayalite/tests/sim/expected/queue_4_false_false.txt
+++ b/crates/fayalite/tests/sim/expected/queue_4_false_false.txt
@@ -1227,6 +1227,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_4_false_true.txt b/crates/fayalite/tests/sim/expected/queue_4_false_true.txt
index a374f44..eb058b2 100644
--- a/crates/fayalite/tests/sim/expected/queue_4_false_true.txt
+++ b/crates/fayalite/tests/sim/expected/queue_4_false_true.txt
@@ -1206,6 +1206,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_4_true_false.txt b/crates/fayalite/tests/sim/expected/queue_4_true_false.txt
index 7d20f26..15c5e84 100644
--- a/crates/fayalite/tests/sim/expected/queue_4_true_false.txt
+++ b/crates/fayalite/tests/sim/expected/queue_4_true_false.txt
@@ -1237,6 +1237,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/queue_4_true_true.txt b/crates/fayalite/tests/sim/expected/queue_4_true_true.txt
index a0ee509..abf172f 100644
--- a/crates/fayalite/tests/sim/expected/queue_4_true_true.txt
+++ b/crates/fayalite/tests/sim/expected/queue_4_true_true.txt
@@ -1216,6 +1216,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/ripple_counter.txt b/crates/fayalite/tests/sim/expected/ripple_counter.txt
index 6562d4d..0c31d13 100644
--- a/crates/fayalite/tests/sim/expected/ripple_counter.txt
+++ b/crates/fayalite/tests/sim/expected/ripple_counter.txt
@@ -725,6 +725,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/shift_register.txt b/crates/fayalite/tests/sim/expected/shift_register.txt
index 1eaa378..40012a7 100644
--- a/crates/fayalite/tests/sim/expected/shift_register.txt
+++ b/crates/fayalite/tests/sim/expected/shift_register.txt
@@ -293,6 +293,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/sim_fork_join.txt b/crates/fayalite/tests/sim/expected/sim_fork_join.txt
index c66e77e..08729ce 100644
--- a/crates/fayalite/tests/sim/expected/sim_fork_join.txt
+++ b/crates/fayalite/tests/sim/expected/sim_fork_join.txt
@@ -87,6 +87,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/sim_fork_join_scope.txt b/crates/fayalite/tests/sim/expected/sim_fork_join_scope.txt
index ae88960..9561bab 100644
--- a/crates/fayalite/tests/sim/expected/sim_fork_join_scope.txt
+++ b/crates/fayalite/tests/sim/expected/sim_fork_join_scope.txt
@@ -87,6 +87,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/sim_only_connects.txt b/crates/fayalite/tests/sim/expected/sim_only_connects.txt
index 2ae2fbe..8908b14 100644
--- a/crates/fayalite/tests/sim/expected/sim_only_connects.txt
+++ b/crates/fayalite/tests/sim/expected/sim_only_connects.txt
@@ -475,6 +475,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/sim_read_past.txt b/crates/fayalite/tests/sim/expected/sim_read_past.txt
index f771434..563fcf9 100644
--- a/crates/fayalite/tests/sim/expected/sim_read_past.txt
+++ b/crates/fayalite/tests/sim/expected/sim_read_past.txt
@@ -591,6 +591,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/sim_resettable_counter_async.txt b/crates/fayalite/tests/sim/expected/sim_resettable_counter_async.txt
index 5584b73..959d746 100644
--- a/crates/fayalite/tests/sim/expected/sim_resettable_counter_async.txt
+++ b/crates/fayalite/tests/sim/expected/sim_resettable_counter_async.txt
@@ -72,6 +72,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/sim_resettable_counter_async_immediate_reset.txt b/crates/fayalite/tests/sim/expected/sim_resettable_counter_async_immediate_reset.txt
index f03c25a..99dece5 100644
--- a/crates/fayalite/tests/sim/expected/sim_resettable_counter_async_immediate_reset.txt
+++ b/crates/fayalite/tests/sim/expected/sim_resettable_counter_async_immediate_reset.txt
@@ -72,6 +72,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/sim_resettable_counter_sync.txt b/crates/fayalite/tests/sim/expected/sim_resettable_counter_sync.txt
index c93d6c1..ac1e153 100644
--- a/crates/fayalite/tests/sim/expected/sim_resettable_counter_sync.txt
+++ b/crates/fayalite/tests/sim/expected/sim_resettable_counter_sync.txt
@@ -72,6 +72,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/sim_resettable_counter_sync_immediate_reset.txt b/crates/fayalite/tests/sim/expected/sim_resettable_counter_sync_immediate_reset.txt
index f13af84..99084ea 100644
--- a/crates/fayalite/tests/sim/expected/sim_resettable_counter_sync_immediate_reset.txt
+++ b/crates/fayalite/tests/sim/expected/sim_resettable_counter_sync_immediate_reset.txt
@@ -72,6 +72,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/sim_trace_as_string.txt b/crates/fayalite/tests/sim/expected/sim_trace_as_string.txt
index 0dd374c..55cb975 100644
--- a/crates/fayalite/tests/sim/expected/sim_trace_as_string.txt
+++ b/crates/fayalite/tests/sim/expected/sim_trace_as_string.txt
@@ -570,6 +570,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
diff --git a/crates/fayalite/tests/sim/expected/test_formal_counter.txt b/crates/fayalite/tests/sim/expected/test_formal_counter.txt
new file mode 100644
index 0000000..e69de29
diff --git a/crates/fayalite/visit_types.json b/crates/fayalite/visit_types.json
index f3af962..1267aa7 100644
--- a/crates/fayalite/visit_types.json
+++ b/crates/fayalite/visit_types.json
@@ -151,6 +151,11 @@
                 "$kind": "Opaque"
             }
         },
+        "NameIdOrGlobal": {
+            "data": {
+                "$kind": "ManualImpl"
+            }
+        },
         "ScopedNameId": {
             "data": {
                 "$kind": "Struct",
@@ -1043,6 +1048,13 @@
             "fold_where": "T: Fold<State>",
             "visit_where": "T: Visit<State>"
         },
+        "ops::SimIoForGlobal": {
+            "data": {
+                "$kind": "Struct",
+                "$constructor": "ops::SimIoForGlobal::new",
+                "global()": "Visible"
+            }
+        },
         "BlockId": {
             "data": {
                 "$kind": "Opaque"
@@ -1277,7 +1289,9 @@
                 "RegSync": "Visible",
                 "RegAsync": "Visible",
                 "Wire": "Visible",
-                "Instance": "Visible"
+                "Instance": "Visible",
+                "FormalInput": "Visible",
+                "SimIoForGlobal": "Visible"
             }
         },
         "TargetChild": {
@@ -1349,6 +1363,21 @@
             "generics": "<T: Type>",
             "fold_where": "T: Fold<State>",
             "visit_where": "T: Visit<State>"
+        },
+        "FormalInput": {
+            "data": {
+                "$kind": "Struct",
+                "$constructor": "FormalInput::new",
+                "kind()": "Visible",
+                "name_id()": "Visible",
+                "ty()": "Visible",
+                "source_location()": "Visible"
+            }
+        },
+        "FormalInputKind": {
+            "data": {
+                "$kind": "Opaque"
+            }
         }
     }
 }
\ No newline at end of file