WIP: reimplement fayalite::formal and add support to the simulator

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

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(),
+        }
+    }
+}

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(),
+        }
+    }
+}

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

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,
+        ScopedNameId, Stmt, StmtConnect, StmtDeclaration, StmtFormal, StmtIf, StmtInstance,
-        StmtWire,
+        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>>,
-}
+    per_module_formal_inputs: RefCell<HashMap<(FormalInput, bool), String>>,
-
-struct BlockDefinitionsState<'a> {
-    rc_definitions: RcDefinitions,
-    parent: &'a BlockDefinitions<'a>,
-    cache: BlockDefinitionsCache,
 }
 
 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(),
-                rc_definitions: RcDefinitions::default(),
+            parent: Some(parent),
-                parent,
+            cache: Default::default(),
-                cache: Default::default(),
-            }),
         }
     }
-    fn none() -> Self {
+    fn module() -> Self {
-        Self { state: None }
+        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 current = self;
-        let mut cur_state = state;
         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) {
+    fn write_out(&self, indent: Indent<'_>, out: &mut String) {
-        self.state
+        self.rc_definitions.write_and_clear(indent, out);
-            .as_ref()
-            .expect("should be some")
-            .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) {
+    fn add_definition_line(&self, v: impl fmt::Display) {
-        self.definitions
+        self.definitions.rc_definitions.add_definition_line(v);
-            .state
-            .as_ref()
-            .expect("should be some")
-            .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 {
+impl ModuleState {
-    fn default() -> Self {
+    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 =
+                    let element = self.expr(Expr::canonical(element), &definitions, const_ty)?;
-                        self.expr(Expr::canonical(element), &mut 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>,
+        reg: Reg<CanonicalType, R>,
-        module_name: Ident,
+        definitions: &BlockDefinitions<'_>,
-        definitions: &mut BlockDefinitions<'_>,
+    ) -> Result<String> {
-        body: &mut String,
-    ) -> Result<()> {
-        let StmtReg { annotations, reg } = stmt_reg;
-        let indent = self.indent;
-        self.targeted_annotations(module_name, vec![], &annotations)?;
         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!(
+            Ok(format!(
-                body,
+                "regreset {name}: {ty}, {clk}, {rst}, {init}{}",
-                "{indent}regreset {name}: {ty}, {clk}, {rst}, {init}{}",
                 FileInfo::new(reg.source_location()),
-            )
+            ))
-            .unwrap();
         } else {
-            writeln!(
+            Ok(format!(
-                body,
+                "reg {name}: {ty}, {clk}{}",
-                "{indent}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 lhs = self.expr(lhs, &definitions, false)?;
-                    let rhs = self.expr(rhs, &mut 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 clk = self.expr(Expr::canonical(clk), &definitions, false)?;
-                    let pred = self.expr(Expr::canonical(pred), &mut definitions, false)?;
+                    let pred = self.expr(Expr::canonical(pred), &definitions, false)?;
-                    let en = self.expr(Expr::canonical(en), &mut 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());
+                    writeln!(body, "{indent}{}", self.instance(instance)?).unwrap();
-                    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();
                 }
             }
             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(
+                let body_str =
-                    module,
+                    self.block(module, top_block, &module_indent, &module_definitions)?;
-                    top_block,
+                module_definitions.write_out(indent, &mut body);
-                    &module_indent,
+                body.push_str(&body_str);
-                    &BlockDefinitions::none(),
-                )?);
                 "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![],

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},
+    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 {
@@ -144,6 +322,20 @@ impl<T: Type> MakeFormalExpr for T {}
 
 #[hdl]
 pub fn formal_global_clock() -> Expr<Clock> {
+    let kind = FormalInputKind::FormalGlobalClock;
+    return 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_module(extern)]
     fn formal_global_clock() {
         #[hdl]
@@ -166,6 +358,20 @@ endmodule
 
 #[hdl]
 pub fn formal_reset() -> Expr<SyncReset> {
+    let kind = FormalInputKind::FormalReset;
+    return 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(),
+    );
     #[hdl_module(extern)]
     fn formal_reset() {
         #[hdl]
@@ -187,9 +393,28 @@ endmodule
 }
 
 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> {
+            $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;
+            return Expr::from_canonical(
+                FormalInput::new(
+                    kind,
+                    NameId(kind.interned_name(), crate::module::Id::new()),
+                    ty.canonical(),
+                    source_location,
+                )
+                .to_expr(),
+            );
             #[hdl_module(extern)]
             pub(super) fn $ident<T: BoolOrIntType>(ty: T) {
                 #[hdl]
@@ -241,7 +466,7 @@ endmodule
     };
 }
 
-make_any_const_fn!(any_const, "anyconst");
+make_any_const_fn!(any_const, any_const_with_loc, "anyconst", AnyConst);
-make_any_const_fn!(any_seq, "anyseq");
+make_any_const_fn!(any_seq, any_seq_with_loc, "anyseq", AnySeq);
-make_any_const_fn!(all_const, "allconst");
+make_any_const_fn!(all_const, all_const_with_loc, "allconst", AllConst);
-make_any_const_fn!(all_seq, "allseq");
+make_any_const_fn!(all_seq, all_seq_with_loc, "allseq", AllSeq);

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, ()> {
+    fn get_base_state(
-        self.target_states.get(&target_base).ok_or(())
+        &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() {
+        match result {
-            if is_lhs {
+            Ok(()) => {}
-                panic!("at {source_location}: tried to connect to not-yet-defined item: {target}");
+            Err(GetTargetStatesError::NotFound) => {
-            } else {
+                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 struct TargetInInstantiatedModuleOrGlobal {
-    pub instantiated_module: InstantiatedModule,
+    instantiated_module_or_global: InstantiatedModuleOrGlobal,
-    pub target: Target,
+    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)]

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),

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()

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"));

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

crates/fayalite/src/sim.rs

@@ -12,6 +12,7 @@ use crate::{
             TargetPathTraceAsStringInner,
         },
     },
+    formal::FormalInput,
     int::BoolOrIntType,
     intern::{
         Intern, InternSlice, Interned, InternedCompare, PtrEqWithTypeId, SupportsPtrEqWithTypeId,
@@ -315,6 +316,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
@@ -2162,20 +2171,26 @@ impl SimulationImpl {
             io: compiled.io.to_expr(),
             main_module: SimulationModuleState::new(
                 compiled
-                    .io
+                    .global_io
-                    .ty()
+                    .iter()
-                    .fields()
+                    .map(|&(global_io, value)| (global_io.into(), value))
-                    .into_iter()
+                    .chain(
-                    .zip(compiled.base_module.module_io)
+                        compiled
-                    .map(|(BundleField { name, .. }, value)| {
+                            .io
-                        (
+                            .ty()
-                            io_target.join(
+                            .fields()
-                                TargetPathElement::from(TargetPathBundleField { name })
+                            .into_iter()
-                                    .intern_sized(),
+                            .zip(compiled.base_module.module_io)
-                            ),
+                            .map(|(BundleField { name, .. }, value)| {
-                            value,
+                                (
-                        )
+                                    io_target.join(
-                    }),
+                                        TargetPathElement::from(TargetPathBundleField { name })
+                                            .intern_sized(),
+                                    ),
+                                    value,
+                                )
+                            }),
+                    ),
                 &[],
             ),
             extern_modules,

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,
+        TraceEnumDiscriminant, TraceEnumWithFields, TraceFieldlessEnum, TraceFormalInput,
-        TraceLocation, TraceMem, TraceMemPort, TraceMemoryId, TraceMemoryLocation, TraceModule,
+        TraceInstance, TraceLocation, TraceMem, TraceMemPort, TraceMemoryId, TraceMemoryLocation,
-        TraceModuleIO, TracePhantomConst, TraceReg, TraceSInt, TraceScalar, TraceScalarId,
+        TraceModule, TraceModuleIO, TracePhantomConst, TraceReg, TraceSInt, TraceScalar,
-        TraceScope, TraceSimOnly, TraceSyncReset, TraceTraceAsString, TraceUInt, TraceWire,
+        TraceScalarId, TraceScope, TraceSimOnly, TraceSyncReset, TraceTraceAsString, TraceUInt,
-        TraceWriter, TraceWriterDecls,
+        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 {

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")
+                    }
                 }
             }
         }

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

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.rst)), "en check 2") @[module-XXXXXXXXXX.rs 10:1]
-        assume(clk, pred2, and(en2, not(formal_reset_1.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]
-        inst formal_reset_2 of formal_reset @[formal.rs 185:24]
+        assert(clk, pred1, and(UInt<1>(0h1), not(formal_reset.rst)), "check 1") @[module-XXXXXXXXXX.rs 12:1]
-        cover(clk, pred3, and(en3, not(formal_reset_2.rst)), "en check 3") @[module-XXXXXXXXXX.rs 11:1]
+        assume(clk, pred2, and(UInt<1>(0h1), not(formal_reset.rst)), "check 2") @[module-XXXXXXXXXX.rs 13:1]
-        inst formal_reset_3 of formal_reset @[formal.rs 185:24]
+        cover(clk, pred3, and(UInt<1>(0h1), not(formal_reset.rst)), "check 3") @[module-XXXXXXXXXX.rs 14:1]
-        assert(clk, pred1, and(UInt<1>(0h1), not(formal_reset_3.rst)), "check 1") @[module-XXXXXXXXXX.rs 12:1]
+    extmodule formal_reset: @[builtin 1:1]
-        inst formal_reset_4 of formal_reset @[formal.rs 185:24]
+        output rst: UInt<1> @[builtin 1:1]
-        assume(clk, pred2, and(UInt<1>(0h1), not(formal_reset_4.rst)), "check 2") @[module-XXXXXXXXXX.rs 13:1]
+        defname = __fayalite_formal_reset
-        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]
+
+#[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
 "#,
     };

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"
+            }
         }
     }
 }