switch ready_valid::queue formal proofs to use formal_global_clock

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

crates/fayalite/src/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,69 @@ 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()`].
+///
+/// [`Simulation::io()`]: crate::sim::Simulation::io
+/// [`Simulation::write()`]: crate::sim::Simulation::write
+/// [`formal_global_clock()`]: crate::formal::formal_global_clock
+pub struct SimIoForGlobal {
+    global: FormalInput,
+}
+
+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,
-        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![],

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

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

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

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

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

@@ -6,26 +6,29 @@
 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,
+        ModuleIO, StmtFormal,
         transform::visit::{Fold, Folder, Visit, Visitor},
     },
     prelude::*,
     reset::ResetType,
     sim::{
         compiler::{
-            Compiled, CompiledBundleField, CompiledExternModule, CompiledTypeLayoutBody,
-            CompiledValue, ExternModuleClockForPast,
+            Compiled, CompiledAssert, CompiledBundleField, CompiledExternModule,
+            CompiledTypeLayoutBody, CompiledValue, ExternModuleClockForPast,
         },
         interpreter::{
             BreakAction, BreakpointsSet, RunResult, SmallUInt, State,
@@ -50,7 +53,7 @@ use std::{
     any::Any,
     cell::{Cell, RefCell},
     collections::{BTreeMap, BTreeSet},
-    fmt,
+    fmt::{self, Write},
     future::{Future, IntoFuture},
     hash::Hash,
     mem,
@@ -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,
@@ -2005,6 +2024,7 @@ struct SimulationImpl {
     >,
     waiting_sensitivity_sets_by_address: HashMap<*const SensitivitySet, Rc<SensitivitySet>>,
     trace_as_string_buf: String,
+    asserts: Interned<[CompiledAssert]>,
 }
 
 impl fmt::Debug for SimulationImpl {
@@ -2082,6 +2102,7 @@ impl SimulationImpl {
         let Self {
             state,
             io: self_io,
+            global_io,
             main_module,
             extern_modules,
             trace_decls,
@@ -2095,10 +2116,15 @@ impl SimulationImpl {
             waiting_sensitivity_sets_by_compiled_value,
             waiting_sensitivity_sets_by_address,
             trace_as_string_buf: _,
+            asserts,
         } = self;
         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)
@@ -2118,6 +2144,7 @@ impl SimulationImpl {
                 "waiting_sensitivity_sets_by_compiled_value",
                 &DebugSensitivitySetsByCompiledValue(waiting_sensitivity_sets_by_compiled_value),
             )
+            .field("asserts", asserts)
             .finish_non_exhaustive()
     }
     fn new(compiled: Compiled<Bundle>) -> Self {
@@ -2160,22 +2187,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,
@@ -2202,6 +2236,7 @@ impl SimulationImpl {
             waiting_sensitivity_sets_by_compiled_value: HashMap::default(),
             waiting_sensitivity_sets_by_address: HashMap::default(),
             trace_as_string_buf: String::with_capacity(256),
+            asserts: compiled.asserts,
         }
     }
     fn write_traces<const ONLY_IF_CHANGED: bool>(
@@ -2729,6 +2764,50 @@ impl SimulationImpl {
             self.cancel_wake_after_change(&sensitivity_set);
         }
     }
+    #[track_caller]
+    #[cold]
+    fn handle_failed_asserts(&mut self, assert_failed_log: Vec<usize>) -> ! {
+        let mut message = format!(
+            "Assertions/Assumptions failed at time {:?}:\n",
+            self.event_queue.lock().instant,
+        );
+        for assert_failed_index in assert_failed_log {
+            let CompiledAssert {
+                instantiated_module,
+                stmt_formal:
+                    StmtFormal {
+                        kind,
+                        clk: _,
+                        pred: _,
+                        en: _,
+                        text,
+                        source_location,
+                    },
+            } = self.asserts[assert_failed_index];
+            writeln!(
+                message,
+                "at {source_location}: in {instantiated_module:?}: {} failed: {text}",
+                kind.as_str()
+            )
+            .unwrap();
+        }
+        panic!("{message}")
+    }
+    #[track_caller]
+    fn check_for_failed_asserts(&mut self) {
+        if self.state.assert_failed_log.is_empty() {
+            return;
+        }
+        if let Some(Event {
+            instant: _,
+            kind: EventKind::State,
+        }) = self.event_queue.peek_first_event_for_now()
+        {
+            return;
+        }
+        let assert_failed_log = mem::take(&mut self.state.assert_failed_log);
+        self.handle_failed_asserts(assert_failed_log);
+    }
     fn write_traces_after_event(&mut self) {
         if let Some(Event {
             instant: _,
@@ -2831,6 +2910,7 @@ impl SimulationImpl {
                     }
                 }
                 this.write_traces_after_event();
+                this.check_for_failed_asserts();
                 this.check_waiting_sensitivity_sets();
             } else {
                 event_queue = first_entry.into_event_queue_lock();
@@ -2852,18 +2932,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 +2956,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 +2990,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 +3003,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 +3238,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 +3252,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 +3285,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 +3465,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 +3851,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 +3872,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 +3947,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 +3986,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 +4014,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 +4083,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 +4355,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 +4371,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 +4387,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 +4407,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 +4430,7 @@ impl ExternModuleSimulationState {
             .read(
                 Expr::canonical(io),
                 ReadTime::Past { clock_for_past },
-                WhichModule::Extern {
+                |_| WhichModule::Extern {
                     module_index: self.module_index,
                 },
             )
@@ -4019,7 +4440,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 },
     );
 }
 

crates/fayalite/src/sim/interpreter.rs

@@ -980,6 +980,7 @@ macro_rules! make_state {
             pub(crate) insns: Interned<Insns<InsnsBuildingDone>>,
             pub(crate) pc: usize,
             pub(crate) memory_write_log: Vec<(StatePartIndex<StatePartKindMemories>, usize)>,
+            pub(crate) assert_failed_log: Vec<usize>,
             $(pub(crate) $state_plural_field: StatePart<$state_kind>,)*
             $(pub(crate) $type_plural_field: StatePart<$type_kind>,)*
         }
@@ -990,6 +991,7 @@ macro_rules! make_state {
                     insns: _,
                     pc,
                     memory_write_log,
+                    assert_failed_log,
                     $($state_plural_field,)*
                     $($type_plural_field,)*
                 } = self;
@@ -997,6 +999,7 @@ macro_rules! make_state {
                     .field("insns", &InsnsOfState(self))
                     .field("pc", pc)
                     .field("memory_write_log", memory_write_log)
+                    .field("assert_failed_log", assert_failed_log)
                     $(.field(stringify!($state_plural_field), $state_plural_field))*
                     $(.field(stringify!($type_plural_field), $type_plural_field))*
                     .finish()
@@ -1009,6 +1012,7 @@ macro_rules! make_state {
                     insns,
                     pc: 0,
                     memory_write_log: Vec::with_capacity(32),
+                    assert_failed_log: Vec::new(),
                     $($state_plural_field: StatePart::new(&insns.state_layout.$state_plural_field.layout_data),)*
                     $($type_plural_field: StatePart::new(&insns.state_layout.ty.$type_plural_field.layout_data),)*
                 }
@@ -1020,6 +1024,7 @@ macro_rules! make_state {
                     pc: self.pc,
                     orig_pc: &mut self.pc,
                     memory_write_log: &mut self.memory_write_log,
+                    assert_failed_log: &mut self.assert_failed_log,
                     $($state_plural_field: self.$state_plural_field.borrow(),)*
                     $($type_plural_field: self.$type_plural_field.borrow(),)*
                 }
@@ -1042,6 +1047,7 @@ macro_rules! make_state {
             pub(crate) orig_pc: &'a mut usize,
             pub(crate) pc: usize,
             pub(crate) memory_write_log: &'a mut Vec<(StatePartIndex<StatePartKindMemories>, usize)>,
+            pub(crate) assert_failed_log: &'a mut Vec<usize>,
             $(pub(crate) $state_plural_field: BorrowedStatePart<'a, $state_kind>,)*
             $(pub(crate) $type_plural_field: BorrowedStatePart<'a, $type_kind>,)*
         }
@@ -1299,6 +1305,7 @@ impl State {
             insns: _,
             pc,
             memory_write_log: _,
+            assert_failed_log: _,
             memories: _,
             small_slots: _,
             big_slots: _,
@@ -1338,6 +1345,10 @@ impl BorrowedState<'_> {
             self.memory_write_log.push(log_entry);
         }
     }
+    #[cold]
+    fn assert_failed(&mut self, assert_index: usize) {
+        self.assert_failed_log.push(assert_index);
+    }
 }
 
 fn bigint_pow2(width: usize) -> Interned<BigInt> {
@@ -2105,6 +2116,19 @@ impl_insns! {
         state.log_memory_write(memory, addr);
         next!();
     }
+    Assert {
+        #[kind = Input]
+        clk_triggered: StatePartIndex<StatePartKindSmallSlots>,
+        #[kind = Input]
+        pred: StatePartIndex<StatePartKindSmallSlots>,
+        #[kind = Immediate]
+        assert_index: usize,
+    } => {
+        if state.small_slots[clk_triggered] != 0 && state.small_slots[pred] == 0 {
+            state.assert_failed(assert_index);
+        }
+        next!();
+    }
     Return => {
         break RunResult::Return(());
     }

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 {

crates/fayalite/src/util/ready_valid.rs

@@ -241,15 +241,13 @@ mod tests {
         /// happens to be in phase with the offending input or output).
         #[hdl_module]
         fn queue_test(capacity: NonZeroUsize, inp_ready_is_comb: bool, out_valid_is_comb: bool) {
-            #[hdl]
-            let clk: Clock = m.input();
             #[hdl]
             let cd = wire();
             connect(
                 cd,
                 #[hdl]
                 ClockDomain {
-                    clk,
+                    clk: formal_global_clock(),
                     rst: formal_reset().to_reset(),
                 },
             );
@@ -280,7 +278,7 @@ mod tests {
             #[hdl]
             let index_to_check = wire(index_ty);
             connect(index_to_check, any_const(index_ty));
-            hdl_assume(clk, index_to_check.cmp_lt(capacity.get()), "");
+            hdl_assume(cd.clk, index_to_check.cmp_lt(capacity.get()), "");
 
             // instantiate and connect the queue
             #[hdl]
@@ -300,13 +298,13 @@ mod tests {
             let expected_count_reg = reg_builder().clock_domain(cd).reset(count_ty.zero());
             #[hdl]
             if ReadyValid::firing(dut.inp) & !ReadyValid::firing(dut.out) {
-                hdl_assert(clk, expected_count_reg.cmp_ne(capacity.get()), "");
+                hdl_assert(cd.clk, expected_count_reg.cmp_ne(capacity.get()), "");
                 connect_any(expected_count_reg, expected_count_reg + 1u8);
             } else if !ReadyValid::firing(dut.inp) & ReadyValid::firing(dut.out) {
-                hdl_assert(clk, expected_count_reg.cmp_ne(count_ty.zero()), "");
+                hdl_assert(cd.clk, expected_count_reg.cmp_ne(count_ty.zero()), "");
                 connect_any(expected_count_reg, expected_count_reg - 1u8);
             }
-            hdl_assert(clk, expected_count_reg.cmp_eq(dut.count), "");
+            hdl_assert(cd.clk, expected_count_reg.cmp_eq(dut.count), "");
 
             // keep an independent write index into the FIFO's circular buffer
             #[hdl]
@@ -374,7 +372,7 @@ mod tests {
                     match inp_firing_data {
                         // ... and we are not receiving data, then we must not
                         // transmit any data.
-                        HdlNone => hdl_assert(clk, HdlOption::is_none(out_firing_data), ""),
+                        HdlNone => hdl_assert(cd.clk, HdlOption::is_none(out_firing_data), ""),
                         // If we are indeed receiving some data...
                         HdlSome(data_in) => {
                             #[hdl]
@@ -382,7 +380,9 @@ mod tests {
                                 // ... and transmitting at the same time, we
                                 // must be transmitting the input data itself,
                                 // since the holding register is empty.
-                                HdlSome(data_out) => hdl_assert(clk, data_out.cmp_eq(data_in), ""),
+                                HdlSome(data_out) => {
+                                    hdl_assert(cd.clk, data_out.cmp_eq(data_in), "")
+                                }
                                 // If we are receiving, but not transmitting,
                                 // store the received data in the holding
                                 // register.
@@ -397,11 +397,11 @@ mod tests {
                     match out_firing_data {
                         // ... and we are not transmitting it, we cannot
                         // receive any more data.
-                        HdlNone => hdl_assert(clk, HdlOption::is_none(inp_firing_data), ""),
+                        HdlNone => hdl_assert(cd.clk, HdlOption::is_none(inp_firing_data), ""),
                         // If we are transmitting a previously stored value...
                         HdlSome(data_out) => {
                             // ... it must be the same data we stored earlier.
-                            hdl_assert(clk, data_out.cmp_eq(stored), "");
+                            hdl_assert(cd.clk, data_out.cmp_eq(stored), "");
                             // Also, accept new data, if any. Otherwise,
                             // let the holding register become empty.
                             connect(stored_reg, inp_firing_data);
@@ -417,17 +417,17 @@ mod tests {
             connect(dut.dbg.index_to_check, index_to_check);
             #[hdl]
             if let HdlSome(stored) = stored_reg {
-                hdl_assert(clk, stored.cmp_eq(dut.dbg.stored), "");
+                hdl_assert(cd.clk, stored.cmp_eq(dut.dbg.stored), "");
             }
 
             // sync the read and write indices
-            hdl_assert(clk, inp_index_reg.cmp_eq(dut.dbg.inp_index), "");
-            hdl_assert(clk, out_index_reg.cmp_eq(dut.dbg.out_index), "");
+            hdl_assert(cd.clk, inp_index_reg.cmp_eq(dut.dbg.inp_index), "");
+            hdl_assert(cd.clk, out_index_reg.cmp_eq(dut.dbg.out_index), "");
 
             // the indices should never go past the capacity, but induction
             // doesn't know that...
-            hdl_assert(clk, inp_index_reg.cmp_lt(capacity.get()), "");
-            hdl_assert(clk, out_index_reg.cmp_lt(capacity.get()), "");
+            hdl_assert(cd.clk, inp_index_reg.cmp_lt(capacity.get()), "");
+            hdl_assert(cd.clk, out_index_reg.cmp_lt(capacity.get()), "");
 
             // strongly constrain the state of the holding register
             //
@@ -455,7 +455,7 @@ mod tests {
             connect(expected_stored, pending_reads.cmp_lt(dut.count));
             // sync with the state of the holding register
             hdl_assert(
-                clk,
+                cd.clk,
                 expected_stored.cmp_eq(HdlOption::is_some(stored_reg)),
                 "",
             );

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_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
 "#,
     };

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,136 @@ circuit sim_trace_as_string: %[[
 ",
     };
 }
+
+#[hdl_module(outline_generated)]
+pub fn formal_counter(count_modulus: 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);
+    let next_count = count_reg + 1u8;
+    #[hdl]
+    if next_count.cmp_lt(count_modulus) {
+        connect_any(count_reg, next_count);
+    } else {
+        connect(count_reg, 0u8);
+    }
+    #[hdl]
+    let count: UInt<8> = m.output();
+    connect(count, count_reg);
+    #[hdl]
+    let enable_assert: Bool = m.input();
+    #[hdl]
+    if enable_assert {
+        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.write(sim.io().enable_assert, true);
+    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, 8));
+    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);
+    let half_us = SimDuration::from_nanos(500);
+    sim.write_clock(formal_global_clock(), false);
+    sim.write_reset(formal_reset(), true);
+    sim.write(any_seq_in, 0u16);
+    sim.write(sim.io().enable_assert, false);
+    sim.advance_time(half_us);
+    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(half_us);
+    const PANIC_MSG: &str = "Assertions/Assumptions failed at time 20.500000000000 \u{3bc}s:\n\
+at module-XXXXXXXXXX.rs:12:1: in InstantiatedModule(formal_counter: formal_counter): assert failed: \n";
+    const EXPECTED_FAILURE_CYCLE: u8 = 19;
+    for i in 0.. {
+        dbg!(i);
+        assert_eq!(i % 10, sim.read(sim.io().count).as_int());
+        sim.write(sim.io().enable_assert, i > 15);
+        sim.write_clock(formal_global_clock(), false);
+        sim.advance_time(half_us);
+        match catch_unwind(AssertUnwindSafe(|| {
+            sim.write_clock(formal_global_clock(), true);
+            sim.advance_time(half_us);
+        })) {
+            Ok(()) => assert!(i < EXPECTED_FAILURE_CYCLE),
+            Err(e) => match e.downcast::<String>() {
+                Ok(e) if *e == PANIC_MSG => {
+                    assert_eq!(i, EXPECTED_FAILURE_CYCLE);
+                    break;
+                }
+                Ok(e) => resume_unwind(e),
+                Err(e) => resume_unwind(e),
+            },
+        }
+    }
+}

crates/fayalite/tests/sim/expected/array_rw.txt

@@ -419,6 +419,7 @@ Simulation {
         },
         pc: 38,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -497,6 +498,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -1759,5 +1761,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/conditional_assignment_last.txt

@@ -76,6 +76,7 @@ Simulation {
         },
         pc: 5,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -101,6 +102,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -186,5 +188,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/connect_const.txt

@@ -54,6 +54,7 @@ Simulation {
         },
         pc: 2,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -77,6 +78,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -138,5 +140,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/connect_const_reset.txt

@@ -80,6 +80,7 @@ Simulation {
         },
         pc: 5,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -106,6 +107,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -206,5 +208,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/counter_async.txt

@@ -180,6 +180,7 @@ Simulation {
         },
         pc: 19,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -216,6 +217,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -385,5 +387,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/counter_sync.txt

@@ -162,6 +162,7 @@ Simulation {
         },
         pc: 16,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -197,6 +198,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -366,5 +368,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/duplicate_names.txt

@@ -72,6 +72,7 @@ Simulation {
         },
         pc: 4,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -97,6 +98,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [],
         uninitialized_ios: {},
@@ -169,5 +171,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/enum_with_simple_body.txt

@@ -409,6 +409,7 @@ Simulation {
         },
         pc: 45,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -465,6 +466,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -745,5 +747,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/enums.txt

@@ -1184,6 +1184,7 @@ Simulation {
         },
         pc: 133,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -1324,6 +1325,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -1955,5 +1957,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/extern_module.txt

@@ -44,6 +44,7 @@ Simulation {
         },
         pc: 0,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -67,6 +68,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -261,5 +263,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/extern_module2.txt

@@ -48,6 +48,7 @@ Simulation {
         },
         pc: 0,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -72,6 +73,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -416,5 +418,6 @@ Simulation {
             },
         ),
     },
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/last_connect.txt

@@ -407,6 +407,7 @@ Simulation {
         },
         pc: 44,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -464,6 +465,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -705,5 +707,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/many_memories.txt

@@ -2728,6 +2728,7 @@ Simulation {
         },
         pc: 256,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -3183,6 +3184,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -7927,5 +7929,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/memories.txt

@@ -494,6 +494,7 @@ Simulation {
         },
         pc: 41,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -579,6 +580,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -1650,5 +1652,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/memories2.txt

@@ -526,6 +526,7 @@ Simulation {
         },
         pc: 52,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -607,6 +608,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -1285,5 +1287,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/memories3.txt

@@ -1336,6 +1336,7 @@ Simulation {
         },
         pc: 129,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1495,6 +1496,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -3345,5 +3347,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/mod1.txt

@@ -187,6 +187,7 @@ Simulation {
         },
         pc: 17,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -225,6 +226,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -577,5 +579,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/phantom_const.txt

@@ -172,6 +172,7 @@ Simulation {
         },
         pc: 16,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -215,6 +216,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -527,5 +529,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_1_false_false.txt

@@ -1083,6 +1083,7 @@ Simulation {
         },
         pc: 134,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1201,6 +1202,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2160,5 +2162,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_1_false_true.txt

@@ -1064,6 +1064,7 @@ Simulation {
         },
         pc: 132,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1180,6 +1181,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2139,5 +2141,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_1_true_false.txt

@@ -1093,6 +1093,7 @@ Simulation {
         },
         pc: 136,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1211,6 +1212,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2170,5 +2172,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_1_true_true.txt

@@ -1074,6 +1074,7 @@ Simulation {
         },
         pc: 134,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1190,6 +1191,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2149,5 +2151,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_2_false_false.txt

@@ -1098,6 +1098,7 @@ Simulation {
         },
         pc: 135,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1219,6 +1220,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2178,5 +2180,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_2_false_true.txt

@@ -1079,6 +1079,7 @@ Simulation {
         },
         pc: 133,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1198,6 +1199,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2157,5 +2159,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_2_true_false.txt

@@ -1108,6 +1108,7 @@ Simulation {
         },
         pc: 137,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1229,6 +1230,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2188,5 +2190,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_2_true_true.txt

@@ -1089,6 +1089,7 @@ Simulation {
         },
         pc: 135,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1208,6 +1209,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2167,5 +2169,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_3_false_false.txt

@@ -1125,6 +1125,7 @@ Simulation {
         },
         pc: 139,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1248,6 +1249,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2187,5 +2189,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_3_false_true.txt

@@ -1106,6 +1106,7 @@ Simulation {
         },
         pc: 137,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1227,6 +1228,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2166,5 +2168,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_3_true_false.txt

@@ -1135,6 +1135,7 @@ Simulation {
         },
         pc: 141,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1258,6 +1259,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2197,5 +2199,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_3_true_true.txt

@@ -1116,6 +1116,7 @@ Simulation {
         },
         pc: 139,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1237,6 +1238,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2176,5 +2178,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_4_false_false.txt

@@ -1104,6 +1104,7 @@ Simulation {
         },
         pc: 135,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1227,6 +1228,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2186,5 +2188,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_4_false_true.txt

@@ -1085,6 +1085,7 @@ Simulation {
         },
         pc: 133,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1206,6 +1207,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2165,5 +2167,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_4_true_false.txt

@@ -1114,6 +1114,7 @@ Simulation {
         },
         pc: 137,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1237,6 +1238,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2196,5 +2198,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/queue_4_true_true.txt

@@ -1095,6 +1095,7 @@ Simulation {
         },
         pc: 135,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -1216,6 +1217,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2175,5 +2177,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/ripple_counter.txt

@@ -636,6 +636,7 @@ Simulation {
         },
         pc: 69,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -725,6 +726,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -1790,5 +1792,6 @@ Simulation {
             },
         ),
     },
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/shift_register.txt

@@ -254,6 +254,7 @@ Simulation {
         },
         pc: 34,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -293,6 +294,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -545,5 +547,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/sim_fork_join.txt

@@ -60,6 +60,7 @@ Simulation {
         },
         pc: 0,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -87,6 +88,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -521,5 +523,6 @@ Simulation {
             },
         ),
     },
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/sim_fork_join_scope.txt

@@ -60,6 +60,7 @@ Simulation {
         },
         pc: 0,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -87,6 +88,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -521,5 +523,6 @@ Simulation {
             },
         ),
     },
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/sim_only_connects.txt

@@ -375,6 +375,7 @@ Simulation {
         },
         pc: 41,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -475,6 +476,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -1768,5 +1770,6 @@ Simulation {
             },
         ),
     },
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/sim_read_past.txt

@@ -512,6 +512,7 @@ Simulation {
         },
         pc: 57,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -591,6 +592,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -9726,5 +9728,6 @@ Simulation {
             },
         ),
     },
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/sim_resettable_counter_async.txt

@@ -48,6 +48,7 @@ Simulation {
         },
         pc: 0,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -72,6 +73,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -539,5 +541,6 @@ Simulation {
             },
         ),
     },
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/sim_resettable_counter_async_immediate_reset.txt

@@ -48,6 +48,7 @@ Simulation {
         },
         pc: 0,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -72,6 +73,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -539,5 +541,6 @@ Simulation {
             },
         ),
     },
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/sim_resettable_counter_sync.txt

@@ -48,6 +48,7 @@ Simulation {
         },
         pc: 0,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -72,6 +73,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -497,5 +499,6 @@ Simulation {
             },
         ),
     },
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/sim_resettable_counter_sync_immediate_reset.txt

@@ -48,6 +48,7 @@ Simulation {
         },
         pc: 0,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [],
         },
@@ -72,6 +73,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -497,5 +499,6 @@ Simulation {
             },
         ),
     },
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/sim_trace_as_string.txt

@@ -494,6 +494,7 @@ Simulation {
         },
         pc: 43,
         memory_write_log: [],
+        assert_failed_log: [],
         memories: StatePart {
             value: [
                 MemoryData {
@@ -570,6 +571,7 @@ Simulation {
             ..
         },
     },
+    global_io: {},
     main_module: SimulationModuleState {
         base_targets: [
             Instance {
@@ -2250,5 +2252,6 @@ Simulation {
     }),
     waiting_sensitivity_sets_by_address: {},
     waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [],
     ..
 }

crates/fayalite/tests/sim/expected/test_formal_counter.txt

@@ -0,0 +1,855 @@
+Simulation {
+    state: State {
+        insns: Insns {
+            state_layout: StateLayout {
+                ty: TypeLayout {
+                    small_slots: StatePartLayout<SmallSlots> {
+                        len: 5,
+                        debug_data: [
+                            SlotDebugData {
+                                name: "",
+                                ty: Bool,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: Bool,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: Bool,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: Bool,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: Bool,
+                            },
+                        ],
+                        ..
+                    },
+                    big_slots: StatePartLayout<BigSlots> {
+                        len: 26,
+                        debug_data: [
+                            SlotDebugData {
+                                name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::count",
+                                ty: UInt<8>,
+                            },
+                            SlotDebugData {
+                                name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::enable_assert",
+                                ty: Bool,
+                            },
+                            SlotDebugData {
+                                name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::any_seq_out",
+                                ty: UInt<16>,
+                            },
+                            SlotDebugData {
+                                name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::cd.clk",
+                                ty: Clock,
+                            },
+                            SlotDebugData {
+                                name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::cd.rst",
+                                ty: SyncReset,
+                            },
+                            SlotDebugData {
+                                name: ".clk",
+                                ty: Clock,
+                            },
+                            SlotDebugData {
+                                name: ".rst",
+                                ty: SyncReset,
+                            },
+                            SlotDebugData {
+                                name: "<<Global>>::formal_global_clock",
+                                ty: Clock,
+                            },
+                            SlotDebugData {
+                                name: "<<Global>>::formal_reset",
+                                ty: SyncReset,
+                            },
+                            SlotDebugData {
+                                name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::count_reg",
+                                ty: UInt<8>,
+                            },
+                            SlotDebugData {
+                                name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::count_reg$next",
+                                ty: UInt<8>,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: UInt<8>,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: UInt<8>,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: UInt<9>,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: UInt<8>,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: Bool,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: UInt<8>,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: Bool,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: Bool,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: Bool,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: Bool,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: Bool,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: Bool,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: Bool,
+                            },
+                            SlotDebugData {
+                                name: "",
+                                ty: Bool,
+                            },
+                            SlotDebugData {
+                                name: "<<Global>>::any_seq",
+                                ty: UInt<16>,
+                            },
+                        ],
+                        ..
+                    },
+                    sim_only_slots: StatePartLayout<SimOnlySlots> {
+                        len: 0,
+                        debug_data: [],
+                        layout_data: [],
+                        ..
+                    },
+                },
+                memories: StatePartLayout<Memories> {
+                    len: 0,
+                    debug_data: [],
+                    layout_data: [],
+                    ..
+                },
+            },
+            insns: [
+                // at: module-XXXXXXXXXX.rs:15:1
+                0: Copy {
+                    dest: StatePartIndex<BigSlots>(2), // (0x4d2) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::any_seq_out", ty: UInt<16> },
+                    src: StatePartIndex<BigSlots>(25), // (0x4d2) SlotDebugData { name: "<<Global>>::any_seq", ty: UInt<16> },
+                },
+                // at: module-XXXXXXXXXX.rs:1:1
+                1: Copy {
+                    dest: StatePartIndex<BigSlots>(19), // (0x0) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(8), // (0x0) SlotDebugData { name: "<<Global>>::formal_reset", ty: SyncReset },
+                },
+                2: NotU {
+                    dest: StatePartIndex<BigSlots>(20), // (0x1) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(19), // (0x0) SlotDebugData { name: "", ty: Bool },
+                    width: 1,
+                },
+                3: Const {
+                    dest: StatePartIndex<BigSlots>(18), // (0x1) SlotDebugData { name: "", ty: Bool },
+                    value: 0x1,
+                },
+                4: And {
+                    dest: StatePartIndex<BigSlots>(21), // (0x1) SlotDebugData { name: "", ty: Bool },
+                    lhs: StatePartIndex<BigSlots>(18), // (0x1) SlotDebugData { name: "", ty: Bool },
+                    rhs: StatePartIndex<BigSlots>(20), // (0x1) SlotDebugData { name: "", ty: Bool },
+                },
+                5: NotU {
+                    dest: StatePartIndex<BigSlots>(22), // (0x0) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(21), // (0x1) SlotDebugData { name: "", ty: Bool },
+                    width: 1,
+                },
+                // at: module-XXXXXXXXXX.rs:12:1
+                6: Copy {
+                    dest: StatePartIndex<BigSlots>(24), // (0x1) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(18), // (0x1) SlotDebugData { name: "", ty: Bool },
+                },
+                // at: module-XXXXXXXXXX.rs:9:1
+                7: Copy {
+                    dest: StatePartIndex<BigSlots>(0), // (0x2) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::count", ty: UInt<8> },
+                    src: StatePartIndex<BigSlots>(9), // (0x2) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::count_reg", ty: UInt<8> },
+                },
+                // at: module-XXXXXXXXXX.rs:1:1
+                8: Const {
+                    dest: StatePartIndex<BigSlots>(14), // (0xa) SlotDebugData { name: "", ty: UInt<8> },
+                    value: 0xa,
+                },
+                9: CmpLe {
+                    dest: StatePartIndex<BigSlots>(17), // (0x1) SlotDebugData { name: "", ty: Bool },
+                    lhs: StatePartIndex<BigSlots>(9), // (0x2) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::count_reg", ty: UInt<8> },
+                    rhs: StatePartIndex<BigSlots>(14), // (0xa) SlotDebugData { name: "", ty: UInt<8> },
+                },
+                10: Or {
+                    dest: StatePartIndex<BigSlots>(23), // (0x1) SlotDebugData { name: "", ty: Bool },
+                    lhs: StatePartIndex<BigSlots>(17), // (0x1) SlotDebugData { name: "", ty: Bool },
+                    rhs: StatePartIndex<BigSlots>(22), // (0x0) SlotDebugData { name: "", ty: Bool },
+                },
+                // at: module-XXXXXXXXXX.rs:11:1
+                11: BranchIfZero {
+                    target: 13,
+                    value: StatePartIndex<BigSlots>(1), // (0x1) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::enable_assert", ty: Bool },
+                },
+                // at: module-XXXXXXXXXX.rs:12:1
+                12: Copy {
+                    dest: StatePartIndex<BigSlots>(24), // (0x1) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(23), // (0x1) SlotDebugData { name: "", ty: Bool },
+                },
+                13: IsNonZeroDestIsSmall {
+                    dest: StatePartIndex<SmallSlots>(4), // (0x1 1) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(24), // (0x1) SlotDebugData { name: "", ty: Bool },
+                },
+                // at: module-XXXXXXXXXX.rs:1:1
+                14: Const {
+                    dest: StatePartIndex<BigSlots>(12), // (0x1) SlotDebugData { name: "", ty: UInt<8> },
+                    value: 0x1,
+                },
+                15: Add {
+                    dest: StatePartIndex<BigSlots>(13), // (0x3) SlotDebugData { name: "", ty: UInt<9> },
+                    lhs: StatePartIndex<BigSlots>(9), // (0x2) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::count_reg", ty: UInt<8> },
+                    rhs: StatePartIndex<BigSlots>(12), // (0x1) SlotDebugData { name: "", ty: UInt<8> },
+                },
+                16: CmpLt {
+                    dest: StatePartIndex<BigSlots>(15), // (0x1) SlotDebugData { name: "", ty: Bool },
+                    lhs: StatePartIndex<BigSlots>(13), // (0x3) SlotDebugData { name: "", ty: UInt<9> },
+                    rhs: StatePartIndex<BigSlots>(14), // (0xa) SlotDebugData { name: "", ty: UInt<8> },
+                },
+                17: CastToUInt {
+                    dest: StatePartIndex<BigSlots>(16), // (0x3) SlotDebugData { name: "", ty: UInt<8> },
+                    src: StatePartIndex<BigSlots>(13), // (0x3) SlotDebugData { name: "", ty: UInt<9> },
+                    dest_width: 8,
+                },
+                // at: module-XXXXXXXXXX.rs:4:1
+                18: Copy {
+                    dest: StatePartIndex<BigSlots>(10), // (0x3) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::count_reg$next", ty: UInt<8> },
+                    src: StatePartIndex<BigSlots>(9), // (0x2) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::count_reg", ty: UInt<8> },
+                },
+                // at: module-XXXXXXXXXX.rs:5:1
+                19: BranchIfZero {
+                    target: 21,
+                    value: StatePartIndex<BigSlots>(15), // (0x1) SlotDebugData { name: "", ty: Bool },
+                },
+                // at: module-XXXXXXXXXX.rs:6:1
+                20: Copy {
+                    dest: StatePartIndex<BigSlots>(10), // (0x3) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::count_reg$next", ty: UInt<8> },
+                    src: StatePartIndex<BigSlots>(16), // (0x3) SlotDebugData { name: "", ty: UInt<8> },
+                },
+                // at: module-XXXXXXXXXX.rs:1:1
+                21: Const {
+                    dest: StatePartIndex<BigSlots>(11), // (0x0) SlotDebugData { name: "", ty: UInt<8> },
+                    value: 0x0,
+                },
+                // at: module-XXXXXXXXXX.rs:5:1
+                22: BranchIfNonZero {
+                    target: 24,
+                    value: StatePartIndex<BigSlots>(15), // (0x1) SlotDebugData { name: "", ty: Bool },
+                },
+                // at: module-XXXXXXXXXX.rs:7:1
+                23: Copy {
+                    dest: StatePartIndex<BigSlots>(10), // (0x3) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::count_reg$next", ty: UInt<8> },
+                    src: StatePartIndex<BigSlots>(11), // (0x0) SlotDebugData { name: "", ty: UInt<8> },
+                },
+                // at: module-XXXXXXXXXX.rs:1:1
+                24: Copy {
+                    dest: StatePartIndex<BigSlots>(5), // (0x1) SlotDebugData { name: ".clk", ty: Clock },
+                    src: StatePartIndex<BigSlots>(7), // (0x1) SlotDebugData { name: "<<Global>>::formal_global_clock", ty: Clock },
+                },
+                25: Copy {
+                    dest: StatePartIndex<BigSlots>(6), // (0x0) SlotDebugData { name: ".rst", ty: SyncReset },
+                    src: StatePartIndex<BigSlots>(8), // (0x0) SlotDebugData { name: "<<Global>>::formal_reset", ty: SyncReset },
+                },
+                // at: module-XXXXXXXXXX.rs:3:1
+                26: Copy {
+                    dest: StatePartIndex<BigSlots>(3), // (0x1) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::cd.clk", ty: Clock },
+                    src: StatePartIndex<BigSlots>(5), // (0x1) SlotDebugData { name: ".clk", ty: Clock },
+                },
+                27: Copy {
+                    dest: StatePartIndex<BigSlots>(4), // (0x0) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::cd.rst", ty: SyncReset },
+                    src: StatePartIndex<BigSlots>(6), // (0x0) SlotDebugData { name: ".rst", ty: SyncReset },
+                },
+                // at: module-XXXXXXXXXX.rs:4:1
+                28: IsNonZeroDestIsSmall {
+                    dest: StatePartIndex<SmallSlots>(2), // (0x1 1) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(3), // (0x1) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::cd.clk", ty: Clock },
+                },
+                29: AndSmall {
+                    dest: StatePartIndex<SmallSlots>(1), // (0x0 0) SlotDebugData { name: "", ty: Bool },
+                    lhs: StatePartIndex<SmallSlots>(2), // (0x1 1) SlotDebugData { name: "", ty: Bool },
+                    rhs: StatePartIndex<SmallSlots>(0), // (0x0 0) SlotDebugData { name: "", ty: Bool },
+                },
+                30: IsNonZeroDestIsSmall {
+                    dest: StatePartIndex<SmallSlots>(3), // (0x0 0) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(4), // (0x0) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::cd.rst", ty: SyncReset },
+                },
+                31: BranchIfSmallZero {
+                    target: 36,
+                    value: StatePartIndex<SmallSlots>(1), // (0x0 0) SlotDebugData { name: "", ty: Bool },
+                },
+                32: BranchIfSmallNonZero {
+                    target: 35,
+                    value: StatePartIndex<SmallSlots>(3), // (0x0 0) SlotDebugData { name: "", ty: Bool },
+                },
+                33: Copy {
+                    dest: StatePartIndex<BigSlots>(9), // (0x2) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::count_reg", ty: UInt<8> },
+                    src: StatePartIndex<BigSlots>(10), // (0x3) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::count_reg$next", ty: UInt<8> },
+                },
+                34: Branch {
+                    target: 36,
+                },
+                35: Copy {
+                    dest: StatePartIndex<BigSlots>(9), // (0x2) SlotDebugData { name: "InstantiatedModule(formal_counter: formal_counter).formal_counter::count_reg", ty: UInt<8> },
+                    src: StatePartIndex<BigSlots>(11), // (0x0) SlotDebugData { name: "", ty: UInt<8> },
+                },
+                // at: module-XXXXXXXXXX.rs:12:1
+                36: Assert {
+                    clk_triggered: StatePartIndex<SmallSlots>(1), // (0x0 0) SlotDebugData { name: "", ty: Bool },
+                    pred: StatePartIndex<SmallSlots>(4), // (0x1 1) SlotDebugData { name: "", ty: Bool },
+                    assert_index: 0,
+                },
+                // at: module-XXXXXXXXXX.rs:4:1
+                37: XorSmallImmediate {
+                    dest: StatePartIndex<SmallSlots>(0), // (0x0 0) SlotDebugData { name: "", ty: Bool },
+                    lhs: StatePartIndex<SmallSlots>(2), // (0x1 1) SlotDebugData { name: "", ty: Bool },
+                    rhs: 0x1,
+                },
+                // at: module-XXXXXXXXXX.rs:1:1
+                38: Return,
+            ],
+            ..
+        },
+        pc: 38,
+        memory_write_log: [],
+        assert_failed_log: [],
+        memories: StatePart {
+            value: [],
+        },
+        small_slots: StatePart {
+            value: [
+                0,
+                0,
+                1,
+                0,
+                1,
+            ],
+        },
+        big_slots: StatePart {
+            value: [
+                2,
+                1,
+                1234,
+                1,
+                0,
+                1,
+                0,
+                1,
+                0,
+                2,
+                3,
+                0,
+                1,
+                3,
+                10,
+                1,
+                3,
+                1,
+                1,
+                0,
+                1,
+                1,
+                0,
+                1,
+                1,
+                1234,
+            ],
+        },
+        sim_only_slots: StatePart {
+            value: [],
+        },
+    },
+    io: Instance {
+        name: <simulator>::formal_counter,
+        instantiated: Module {
+            name: formal_counter,
+            ..
+        },
+    },
+    global_io: {
+        SimIoForGlobal(
+            formal_global_clock,
+        ): CompiledValue {
+            layout: CompiledTypeLayout {
+                ty: Clock,
+                layout: TypeLayout {
+                    small_slots: StatePartLayout<SmallSlots> {
+                        len: 0,
+                        debug_data: [],
+                        ..
+                    },
+                    big_slots: StatePartLayout<BigSlots> {
+                        len: 1,
+                        debug_data: [
+                            SlotDebugData {
+                                name: "<<Global>>::formal_global_clock",
+                                ty: Clock,
+                            },
+                        ],
+                        ..
+                    },
+                    sim_only_slots: StatePartLayout<SimOnlySlots> {
+                        len: 0,
+                        debug_data: [],
+                        layout_data: [],
+                        ..
+                    },
+                },
+                body: Scalar,
+            },
+            range: TypeIndexRange {
+                small_slots: StatePartIndexRange<SmallSlots> { start: 0, len: 0 },
+                big_slots: StatePartIndexRange<BigSlots> { start: 7, len: 1 },
+                sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
+            },
+            write: None,
+        },
+        SimIoForGlobal(
+            formal_reset,
+        ): CompiledValue {
+            layout: CompiledTypeLayout {
+                ty: SyncReset,
+                layout: TypeLayout {
+                    small_slots: StatePartLayout<SmallSlots> {
+                        len: 0,
+                        debug_data: [],
+                        ..
+                    },
+                    big_slots: StatePartLayout<BigSlots> {
+                        len: 1,
+                        debug_data: [
+                            SlotDebugData {
+                                name: "<<Global>>::formal_reset",
+                                ty: SyncReset,
+                            },
+                        ],
+                        ..
+                    },
+                    sim_only_slots: StatePartLayout<SimOnlySlots> {
+                        len: 0,
+                        debug_data: [],
+                        layout_data: [],
+                        ..
+                    },
+                },
+                body: Scalar,
+            },
+            range: TypeIndexRange {
+                small_slots: StatePartIndexRange<SmallSlots> { start: 0, len: 0 },
+                big_slots: StatePartIndexRange<BigSlots> { start: 8, len: 1 },
+                sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
+            },
+            write: None,
+        },
+        SimIoForGlobal(
+            any_seq(
+                UInt<16>,
+            ),
+        ): CompiledValue {
+            layout: CompiledTypeLayout {
+                ty: UInt<16>,
+                layout: TypeLayout {
+                    small_slots: StatePartLayout<SmallSlots> {
+                        len: 0,
+                        debug_data: [],
+                        ..
+                    },
+                    big_slots: StatePartLayout<BigSlots> {
+                        len: 1,
+                        debug_data: [
+                            SlotDebugData {
+                                name: "<<Global>>::any_seq",
+                                ty: UInt<16>,
+                            },
+                        ],
+                        ..
+                    },
+                    sim_only_slots: StatePartLayout<SimOnlySlots> {
+                        len: 0,
+                        debug_data: [],
+                        layout_data: [],
+                        ..
+                    },
+                },
+                body: Scalar,
+            },
+            range: TypeIndexRange {
+                small_slots: StatePartIndexRange<SmallSlots> { start: 5, len: 0 },
+                big_slots: StatePartIndexRange<BigSlots> { start: 25, len: 1 },
+                sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
+            },
+            write: None,
+        },
+    },
+    main_module: SimulationModuleState {
+        base_targets: [
+            SimIoForGlobal(
+                formal_global_clock,
+            ),
+            SimIoForGlobal(
+                formal_reset,
+            ),
+            SimIoForGlobal(
+                any_seq(
+                    UInt<16>,
+                ),
+            ),
+            Instance {
+                name: <simulator>::formal_counter,
+                instantiated: Module {
+                    name: formal_counter,
+                    ..
+                },
+            }.count,
+            Instance {
+                name: <simulator>::formal_counter,
+                instantiated: Module {
+                    name: formal_counter,
+                    ..
+                },
+            }.enable_assert,
+            Instance {
+                name: <simulator>::formal_counter,
+                instantiated: Module {
+                    name: formal_counter,
+                    ..
+                },
+            }.any_seq_out,
+        ],
+        uninitialized_ios: {},
+        io_targets: {
+            Instance {
+                name: <simulator>::formal_counter,
+                instantiated: Module {
+                    name: formal_counter,
+                    ..
+                },
+            }.any_seq_out,
+            Instance {
+                name: <simulator>::formal_counter,
+                instantiated: Module {
+                    name: formal_counter,
+                    ..
+                },
+            }.count,
+            Instance {
+                name: <simulator>::formal_counter,
+                instantiated: Module {
+                    name: formal_counter,
+                    ..
+                },
+            }.enable_assert,
+            SimIoForGlobal(
+                any_seq(
+                    UInt<16>,
+                ),
+            ),
+            SimIoForGlobal(
+                formal_global_clock,
+            ),
+            SimIoForGlobal(
+                formal_reset,
+            ),
+        },
+        did_initial_settle: true,
+        clocks_for_past: {},
+    },
+    extern_modules: [],
+    trace_decls: TraceModule {
+        name: "formal_counter",
+        children: [
+            TraceFormalInput {
+                name: "formal_global_clock",
+                child: TraceClock {
+                    location: TraceScalarId(5),
+                    name: "formal_global_clock",
+                    flow: Source,
+                },
+                formal_input: formal_global_clock,
+            },
+            TraceFormalInput {
+                name: "formal_reset",
+                child: TraceSyncReset {
+                    location: TraceScalarId(6),
+                    name: "formal_reset",
+                    flow: Source,
+                },
+                formal_input: formal_reset,
+            },
+            TraceFormalInput {
+                name: "any_seq",
+                child: TraceUInt {
+                    location: TraceScalarId(8),
+                    name: "any_seq",
+                    ty: UInt<16>,
+                    flow: Source,
+                },
+                formal_input: any_seq(
+                    UInt<16>,
+                ),
+            },
+            TraceModuleIO {
+                name: "count",
+                child: TraceUInt {
+                    location: TraceScalarId(0),
+                    name: "count",
+                    ty: UInt<8>,
+                    flow: Sink,
+                },
+                ty: UInt<8>,
+                flow: Sink,
+            },
+            TraceModuleIO {
+                name: "enable_assert",
+                child: TraceBool {
+                    location: TraceScalarId(1),
+                    name: "enable_assert",
+                    flow: Source,
+                },
+                ty: Bool,
+                flow: Source,
+            },
+            TraceModuleIO {
+                name: "any_seq_out",
+                child: TraceUInt {
+                    location: TraceScalarId(2),
+                    name: "any_seq_out",
+                    ty: UInt<16>,
+                    flow: Sink,
+                },
+                ty: UInt<16>,
+                flow: Sink,
+            },
+            TraceWire {
+                name: "cd",
+                child: TraceBundle {
+                    name: "cd",
+                    fields: [
+                        TraceClock {
+                            location: TraceScalarId(3),
+                            name: "clk",
+                            flow: Duplex,
+                        },
+                        TraceSyncReset {
+                            location: TraceScalarId(4),
+                            name: "rst",
+                            flow: Duplex,
+                        },
+                    ],
+                    ty: Bundle {
+                        /* offset = 0 */
+                        clk: Clock,
+                        /* offset = 1 */
+                        rst: SyncReset,
+                    },
+                    flow: Duplex,
+                },
+                ty: Bundle {
+                    /* offset = 0 */
+                    clk: Clock,
+                    /* offset = 1 */
+                    rst: SyncReset,
+                },
+            },
+            TraceReg {
+                name: "count_reg",
+                child: TraceUInt {
+                    location: TraceScalarId(7),
+                    name: "count_reg",
+                    ty: UInt<8>,
+                    flow: Duplex,
+                },
+                ty: UInt<8>,
+            },
+        ],
+    },
+    traces: [
+        SimTrace {
+            id: TraceScalarId(0),
+            kind: BigUInt {
+                index: StatePartIndex<BigSlots>(0),
+                ty: UInt<8>,
+            },
+            maybe_changed: true,
+            state: 0x02,
+            last_state: 0x01,
+        },
+        SimTrace {
+            id: TraceScalarId(1),
+            kind: BigBool {
+                index: StatePartIndex<BigSlots>(1),
+            },
+            maybe_changed: false,
+            state: 0x1,
+            last_state: 0x1,
+        },
+        SimTrace {
+            id: TraceScalarId(2),
+            kind: BigUInt {
+                index: StatePartIndex<BigSlots>(2),
+                ty: UInt<16>,
+            },
+            maybe_changed: true,
+            state: 0x04d2,
+            last_state: 0x04d2,
+        },
+        SimTrace {
+            id: TraceScalarId(3),
+            kind: BigClock {
+                index: StatePartIndex<BigSlots>(3),
+            },
+            maybe_changed: true,
+            state: 0x1,
+            last_state: 0x0,
+        },
+        SimTrace {
+            id: TraceScalarId(4),
+            kind: BigSyncReset {
+                index: StatePartIndex<BigSlots>(4),
+            },
+            maybe_changed: true,
+            state: 0x0,
+            last_state: 0x0,
+        },
+        SimTrace {
+            id: TraceScalarId(5),
+            kind: BigClock {
+                index: StatePartIndex<BigSlots>(7),
+            },
+            maybe_changed: true,
+            state: 0x1,
+            last_state: 0x0,
+        },
+        SimTrace {
+            id: TraceScalarId(6),
+            kind: BigSyncReset {
+                index: StatePartIndex<BigSlots>(8),
+            },
+            maybe_changed: true,
+            state: 0x0,
+            last_state: 0x0,
+        },
+        SimTrace {
+            id: TraceScalarId(7),
+            kind: BigUInt {
+                index: StatePartIndex<BigSlots>(9),
+                ty: UInt<8>,
+            },
+            maybe_changed: true,
+            state: 0x02,
+            last_state: 0x01,
+        },
+        SimTrace {
+            id: TraceScalarId(8),
+            kind: BigUInt {
+                index: StatePartIndex<BigSlots>(25),
+                ty: UInt<16>,
+            },
+            maybe_changed: true,
+            state: 0x04d2,
+            last_state: 0x04d2,
+        },
+    ],
+    trace_memories: {},
+    trace_writers: [
+        Running(
+            VcdWriter {
+                finished_init: true,
+                timescale: 1 ps,
+                ..
+            },
+        ),
+    ],
+    clocks_triggered: [
+        StatePartIndex<SmallSlots>(1),
+    ],
+    event_queue: EventQueue(EventQueueData {
+        instant: 66 μs,
+        events: {},
+    }),
+    waiting_sensitivity_sets_by_address: {},
+    waiting_sensitivity_sets_by_compiled_value: {},
+    asserts: [
+        CompiledAssert {
+            instantiated_module: InstantiatedModule(formal_counter: formal_counter),
+            stmt_formal: assert {
+                clk: Wire(formal_counter::cd: Bundle {
+                    /* offset = 0 */
+                    clk: Clock,
+                    /* offset = 1 */
+                    rst: SyncReset,
+                }).clk,
+                pred: CmpLeU {
+                    lhs: Reg {
+                        name: formal_counter::count_reg,
+                        ty: UInt<8>,
+                        clock_domain: Wire(formal_counter::cd: Bundle {
+                            /* offset = 0 */
+                            clk: Clock,
+                            /* offset = 1 */
+                            rst: SyncReset,
+                        }),
+                        init: Some(
+                            0x0_u8,
+                        ),
+                        ..
+                    },
+                    rhs: 0xA_u8,
+                    literal_bits: Err(
+                        NotALiteralExpr,
+                    ),
+                },
+                en: BitAndB {
+                    lhs: true,
+                    rhs: NotB {
+                        arg: CastSyncResetToBool {
+                            arg: formal_reset,
+                            literal_bits: Err(
+                                NotALiteralExpr,
+                            ),
+                        },
+                        literal_bits: Err(
+                            NotALiteralExpr,
+                        ),
+                    },
+                    literal_bits: Err(
+                        NotALiteralExpr,
+                    ),
+                },
+                text: "",
+                ..
+            },
+        },
+    ],
+    ..
+}

crates/fayalite/tests/sim/expected/test_formal_counter.vcd

@@ -0,0 +1,290 @@
+$timescale 1 ps $end
+$scope module formal_counter $end
+$var wire 1 ekAK2 formal_global_clock $end
+$var wire 1 qTY9h formal_reset $end
+$var wire 16 /roOY any_seq $end
+$var wire 8 }eN0d count $end
+$var wire 1 2f=;S enable_assert $end
+$var wire 16 L-uG? any_seq_out $end
+$scope struct cd $end
+$var wire 1 -e"5` clk $end
+$var wire 1 IC0;$ rst $end
+$upscope $end
+$var reg 8 ^:T_4 count_reg $end
+$upscope $end
+$enddefinitions $end
+$dumpvars
+b0 }eN0d
+12f=;S
+b0 L-uG?
+0-e"5`
+1IC0;$
+0ekAK2
+1qTY9h
+b0 ^:T_4
+b0 /roOY
+$end
+#1000000
+b10011010010 L-uG?
+1-e"5`
+1ekAK2
+b10011010010 /roOY
+0IC0;$
+0qTY9h
+#2000000
+0-e"5`
+0ekAK2
+#3000000
+b1 }eN0d
+1-e"5`
+1ekAK2
+b1 ^:T_4
+#4000000
+0-e"5`
+0ekAK2
+#5000000
+b10 }eN0d
+1-e"5`
+1ekAK2
+b10 ^:T_4
+#6000000
+0-e"5`
+0ekAK2
+#7000000
+b11 }eN0d
+1-e"5`
+1ekAK2
+b11 ^:T_4
+#8000000
+0-e"5`
+0ekAK2
+#9000000
+b100 }eN0d
+1-e"5`
+1ekAK2
+b100 ^:T_4
+#10000000
+0-e"5`
+0ekAK2
+#11000000
+b101 }eN0d
+1-e"5`
+1ekAK2
+b101 ^:T_4
+#12000000
+0-e"5`
+0ekAK2
+#13000000
+b110 }eN0d
+1-e"5`
+1ekAK2
+b110 ^:T_4
+#14000000
+0-e"5`
+0ekAK2
+#15000000
+b111 }eN0d
+1-e"5`
+1ekAK2
+b111 ^:T_4
+#16000000
+0-e"5`
+0ekAK2
+#17000000
+b1000 }eN0d
+1-e"5`
+1ekAK2
+b1000 ^:T_4
+#18000000
+0-e"5`
+0ekAK2
+#19000000
+b1001 }eN0d
+1-e"5`
+1ekAK2
+b1001 ^:T_4
+#20000000
+0-e"5`
+0ekAK2
+#21000000
+b0 }eN0d
+1-e"5`
+1ekAK2
+b0 ^:T_4
+#22000000
+0-e"5`
+0ekAK2
+#23000000
+b1 }eN0d
+1-e"5`
+1ekAK2
+b1 ^:T_4
+#24000000
+0-e"5`
+0ekAK2
+#25000000
+b10 }eN0d
+1-e"5`
+1ekAK2
+b10 ^:T_4
+#26000000
+0-e"5`
+0ekAK2
+#27000000
+b11 }eN0d
+1-e"5`
+1ekAK2
+b11 ^:T_4
+#28000000
+0-e"5`
+0ekAK2
+#29000000
+b100 }eN0d
+1-e"5`
+1ekAK2
+b100 ^:T_4
+#30000000
+0-e"5`
+0ekAK2
+#31000000
+b101 }eN0d
+1-e"5`
+1ekAK2
+b101 ^:T_4
+#32000000
+0-e"5`
+0ekAK2
+#33000000
+b110 }eN0d
+1-e"5`
+1ekAK2
+b110 ^:T_4
+#34000000
+0-e"5`
+0ekAK2
+#35000000
+b111 }eN0d
+1-e"5`
+1ekAK2
+b111 ^:T_4
+#36000000
+0-e"5`
+0ekAK2
+#37000000
+b1000 }eN0d
+1-e"5`
+1ekAK2
+b1000 ^:T_4
+#38000000
+0-e"5`
+0ekAK2
+#39000000
+b1001 }eN0d
+1-e"5`
+1ekAK2
+b1001 ^:T_4
+#40000000
+0-e"5`
+0ekAK2
+#41000000
+b0 }eN0d
+1-e"5`
+1ekAK2
+b0 ^:T_4
+#42000000
+0-e"5`
+0ekAK2
+#43000000
+b1 }eN0d
+1-e"5`
+1ekAK2
+b1 ^:T_4
+#44000000
+0-e"5`
+0ekAK2
+#45000000
+b10 }eN0d
+1-e"5`
+1ekAK2
+b10 ^:T_4
+#46000000
+0-e"5`
+0ekAK2
+#47000000
+b11 }eN0d
+1-e"5`
+1ekAK2
+b11 ^:T_4
+#48000000
+0-e"5`
+0ekAK2
+#49000000
+b100 }eN0d
+1-e"5`
+1ekAK2
+b100 ^:T_4
+#50000000
+0-e"5`
+0ekAK2
+#51000000
+b101 }eN0d
+1-e"5`
+1ekAK2
+b101 ^:T_4
+#52000000
+0-e"5`
+0ekAK2
+#53000000
+b110 }eN0d
+1-e"5`
+1ekAK2
+b110 ^:T_4
+#54000000
+0-e"5`
+0ekAK2
+#55000000
+b111 }eN0d
+1-e"5`
+1ekAK2
+b111 ^:T_4
+#56000000
+0-e"5`
+0ekAK2
+#57000000
+b1000 }eN0d
+1-e"5`
+1ekAK2
+b1000 ^:T_4
+#58000000
+0-e"5`
+0ekAK2
+#59000000
+b1001 }eN0d
+1-e"5`
+1ekAK2
+b1001 ^:T_4
+#60000000
+0-e"5`
+0ekAK2
+#61000000
+b0 }eN0d
+1-e"5`
+1ekAK2
+b0 ^:T_4
+#62000000
+0-e"5`
+0ekAK2
+#63000000
+b1 }eN0d
+1-e"5`
+1ekAK2
+b1 ^:T_4
+#64000000
+0-e"5`
+0ekAK2
+#65000000
+b10 }eN0d
+1-e"5`
+1ekAK2
+b10 ^:T_4
+#66000000

crates/fayalite/tests/sim/expected/test_formal_counter_assert.vcd

@@ -0,0 +1,194 @@
+$timescale 1 ps $end
+$scope module formal_counter $end
+$var wire 1 ekAK2 formal_global_clock $end
+$var wire 1 qTY9h formal_reset $end
+$var wire 16 /roOY any_seq $end
+$var wire 8 }eN0d count $end
+$var wire 1 2f=;S enable_assert $end
+$var wire 16 L-uG? any_seq_out $end
+$scope struct cd $end
+$var wire 1 -e"5` clk $end
+$var wire 1 IC0;$ rst $end
+$upscope $end
+$var reg 8 ^:T_4 count_reg $end
+$upscope $end
+$enddefinitions $end
+$dumpvars
+b0 }eN0d
+02f=;S
+b0 L-uG?
+0-e"5`
+1IC0;$
+0ekAK2
+1qTY9h
+b0 ^:T_4
+b0 /roOY
+$end
+#500000
+b10011010010 L-uG?
+1-e"5`
+1ekAK2
+b10011010010 /roOY
+0IC0;$
+0qTY9h
+#1000000
+0-e"5`
+0ekAK2
+#1500000
+b1 }eN0d
+1-e"5`
+1ekAK2
+b1 ^:T_4
+#2000000
+0-e"5`
+0ekAK2
+#2500000
+b10 }eN0d
+1-e"5`
+1ekAK2
+b10 ^:T_4
+#3000000
+0-e"5`
+0ekAK2
+#3500000
+b11 }eN0d
+1-e"5`
+1ekAK2
+b11 ^:T_4
+#4000000
+0-e"5`
+0ekAK2
+#4500000
+b100 }eN0d
+1-e"5`
+1ekAK2
+b100 ^:T_4
+#5000000
+0-e"5`
+0ekAK2
+#5500000
+b101 }eN0d
+1-e"5`
+1ekAK2
+b101 ^:T_4
+#6000000
+0-e"5`
+0ekAK2
+#6500000
+b110 }eN0d
+1-e"5`
+1ekAK2
+b110 ^:T_4
+#7000000
+0-e"5`
+0ekAK2
+#7500000
+b111 }eN0d
+1-e"5`
+1ekAK2
+b111 ^:T_4
+#8000000
+0-e"5`
+0ekAK2
+#8500000
+b1000 }eN0d
+1-e"5`
+1ekAK2
+b1000 ^:T_4
+#9000000
+0-e"5`
+0ekAK2
+#9500000
+b1001 }eN0d
+1-e"5`
+1ekAK2
+b1001 ^:T_4
+#10000000
+0-e"5`
+0ekAK2
+#10500000
+b0 }eN0d
+1-e"5`
+1ekAK2
+b0 ^:T_4
+#11000000
+0-e"5`
+0ekAK2
+#11500000
+b1 }eN0d
+1-e"5`
+1ekAK2
+b1 ^:T_4
+#12000000
+0-e"5`
+0ekAK2
+#12500000
+b10 }eN0d
+1-e"5`
+1ekAK2
+b10 ^:T_4
+#13000000
+0-e"5`
+0ekAK2
+#13500000
+b11 }eN0d
+1-e"5`
+1ekAK2
+b11 ^:T_4
+#14000000
+0-e"5`
+0ekAK2
+#14500000
+b100 }eN0d
+1-e"5`
+1ekAK2
+b100 ^:T_4
+#15000000
+0-e"5`
+0ekAK2
+#15500000
+b101 }eN0d
+1-e"5`
+1ekAK2
+b101 ^:T_4
+#16000000
+0-e"5`
+0ekAK2
+#16500000
+b110 }eN0d
+1-e"5`
+1ekAK2
+b110 ^:T_4
+#17000000
+12f=;S
+0-e"5`
+0ekAK2
+#17500000
+b111 }eN0d
+1-e"5`
+1ekAK2
+b111 ^:T_4
+#18000000
+0-e"5`
+0ekAK2
+#18500000
+b1000 }eN0d
+1-e"5`
+1ekAK2
+b1000 ^:T_4
+#19000000
+0-e"5`
+0ekAK2
+#19500000
+b1001 }eN0d
+1-e"5`
+1ekAK2
+b1001 ^:T_4
+#20000000
+0-e"5`
+0ekAK2
+#20500000
+b0 }eN0d
+1-e"5`
+1ekAK2
+b0 ^:T_4

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