Initial queue formal proof based on one-entry FIFO equivalence

For now, only check that the basic properties work in bounded model check
mode, leave the induction proof for later.

Partially replace the previously existing proof.

Remove earlier assumptions and bounds that don't apply for this proof.

Use parameterized types instead of hard-coded types.

crates/fayalite/src/bundle.rs

@@ -4,12 +4,14 @@
 use crate::{
     expr::{ops::BundleLiteral, Expr, ToExpr},
     intern::{Intern, Interned},
+    sim::{SimValue, ToSimValue},
     source_location::SourceLocation,
     ty::{
         impl_match_variant_as_self, CanonicalType, MatchVariantWithoutScope, StaticType, Type,
         TypeProperties, TypeWithDeref,
     },
 };
+use bitvec::vec::BitVec;
 use hashbrown::HashMap;
 use std::{fmt, marker::PhantomData};
 
@@ -323,7 +325,7 @@ macro_rules! impl_tuple_builder_fields {
 }
 
 macro_rules! impl_tuples {
-    ([$({#[num = $num:literal, field = $field:ident] $var:ident: $T:ident})*] []) => {
+    ([$({#[num = $num:literal, field = $field:ident, ty = $ty_var:ident: $Ty:ident] $var:ident: $T:ident})*] []) => {
         impl_tuple_builder_fields! {
             {}
             [$({
@@ -423,6 +425,79 @@ macro_rules! impl_tuples {
                 BundleLiteral::new(ty, field_values[..].intern()).to_expr()
             }
         }
+        impl<$($T: ToSimValue<CanonicalType>,)*> ToSimValue<CanonicalType> for ($($T,)*) {
+            #[track_caller]
+            fn to_sim_value(&self, ty: CanonicalType) -> SimValue<CanonicalType> {
+                ToSimValue::<Bundle>::to_sim_value(self, Bundle::from_canonical(ty)).into_canonical()
+            }
+            #[track_caller]
+            fn into_sim_value(self, ty: CanonicalType) -> SimValue<CanonicalType>
+            {
+                ToSimValue::<Bundle>::into_sim_value(self, Bundle::from_canonical(ty)).into_canonical()
+            }
+            #[track_caller]
+            fn box_into_sim_value(self: Box<Self>, ty: CanonicalType) -> SimValue<CanonicalType> {
+                ToSimValue::<Bundle>::box_into_sim_value(self, Bundle::from_canonical(ty)).into_canonical()
+            }
+        }
+        impl<$($T: ToSimValue<CanonicalType>,)*> ToSimValue<Bundle> for ($($T,)*) {
+            #[track_caller]
+            fn to_sim_value(&self, ty: Bundle) -> SimValue<Bundle> {
+                let ($($var,)*) = self;
+                let [$($ty_var,)*] = *ty.fields() else {
+                    panic!("bundle has wrong number of fields");
+                };
+                $(let $var = $var.to_sim_value($ty_var.ty);)*
+                ToSimValue::into_sim_value(($($var,)*), ty)
+            }
+            #[track_caller]
+            fn into_sim_value(self, ty: Bundle) -> SimValue<Bundle> {
+                #![allow(unused_mut)]
+                #![allow(clippy::unused_unit)]
+                let ($($var,)*) = self;
+                let [$($ty_var,)*] = *ty.fields() else {
+                    panic!("bundle has wrong number of fields");
+                };
+                let mut bits: Option<BitVec> = None;
+                $(let $var = $var.into_sim_value($ty_var.ty);
+                assert_eq!($var.ty(), $ty_var.ty);
+                if !$var.bits().is_empty() {
+                    if let Some(bits) = &mut bits {
+                        bits.extend_from_bitslice($var.bits());
+                    } else {
+                        let mut $var = $var.into_bits();
+                        $var.reserve(ty.type_properties().bit_width - $var.len());
+                        bits = Some($var);
+                    }
+                }
+                )*
+                bits.unwrap_or_else(BitVec::new).into_sim_value(ty)
+            }
+            #[track_caller]
+            fn box_into_sim_value(self: Box<Self>, ty: Bundle) -> SimValue<Bundle> {
+                Self::into_sim_value(*self, ty)
+            }
+        }
+        impl<$($T: ToSimValue<$Ty>, $Ty: Type,)*> ToSimValue<($($Ty,)*)> for ($($T,)*) {
+            #[track_caller]
+            fn to_sim_value(&self, ty: ($($Ty,)*)) -> SimValue<($($Ty,)*)> {
+                let ($($var,)*) = self;
+                let ($($ty_var,)*) = ty;
+                $(let $var = $var.to_sim_value($ty_var).into_canonical();)*
+                SimValue::from_canonical(ToSimValue::into_sim_value(($($var,)*), ty.canonical()))
+            }
+            #[track_caller]
+            fn into_sim_value(self, ty: ($($Ty,)*)) -> SimValue<($($Ty,)*)> {
+                let ($($var,)*) = self;
+                let ($($ty_var,)*) = ty;
+                $(let $var = $var.into_sim_value($ty_var).into_canonical();)*
+                SimValue::from_canonical(ToSimValue::into_sim_value(($($var,)*), ty.canonical()))
+            }
+            #[track_caller]
+            fn box_into_sim_value(self: Box<Self>, ty: ($($Ty,)*)) -> SimValue<($($Ty,)*)> {
+                Self::into_sim_value(*self, ty)
+            }
+        }
     };
     ([$($lhs:tt)*] [$rhs_first:tt $($rhs:tt)*]) => {
         impl_tuples!([$($lhs)*] []);
@@ -432,18 +507,18 @@ macro_rules! impl_tuples {
 
 impl_tuples! {
     [] [
-        {#[num = 0, field = field_0] v0: T0}
-        {#[num = 1, field = field_1] v1: T1}
-        {#[num = 2, field = field_2] v2: T2}
-        {#[num = 3, field = field_3] v3: T3}
-        {#[num = 4, field = field_4] v4: T4}
-        {#[num = 5, field = field_5] v5: T5}
-        {#[num = 6, field = field_6] v6: T6}
-        {#[num = 7, field = field_7] v7: T7}
-        {#[num = 8, field = field_8] v8: T8}
-        {#[num = 9, field = field_9] v9: T9}
-        {#[num = 10, field = field_10] v10: T10}
-        {#[num = 11, field = field_11] v11: T11}
+        {#[num = 0, field = field_0, ty = ty0: Ty0] v0: T0}
+        {#[num = 1, field = field_1, ty = ty1: Ty1] v1: T1}
+        {#[num = 2, field = field_2, ty = ty2: Ty2] v2: T2}
+        {#[num = 3, field = field_3, ty = ty3: Ty3] v3: T3}
+        {#[num = 4, field = field_4, ty = ty4: Ty4] v4: T4}
+        {#[num = 5, field = field_5, ty = ty5: Ty5] v5: T5}
+        {#[num = 6, field = field_6, ty = ty6: Ty6] v6: T6}
+        {#[num = 7, field = field_7, ty = ty7: Ty7] v7: T7}
+        {#[num = 8, field = field_8, ty = ty8: Ty8] v8: T8}
+        {#[num = 9, field = field_9, ty = ty9: Ty9] v9: T9}
+        {#[num = 10, field = field_10, ty = ty10: Ty10] v10: T10}
+        {#[num = 11, field = field_11, ty = ty11: Ty11] v11: T11}
     ]
 }
 
@@ -528,3 +603,27 @@ impl<T: ?Sized + Send + Sync + 'static> ToExpr for PhantomData<T> {
         BundleLiteral::new(PhantomData, Interned::default()).to_expr()
     }
 }
+
+impl<T: ?Sized + Send + Sync + 'static> ToSimValue<Self> for PhantomData<T> {
+    #[track_caller]
+    fn to_sim_value(&self, ty: Self) -> SimValue<Self> {
+        ToSimValue::into_sim_value(BitVec::new(), ty)
+    }
+}
+
+impl<T: ?Sized> ToSimValue<Bundle> for PhantomData<T> {
+    #[track_caller]
+    fn to_sim_value(&self, ty: Bundle) -> SimValue<Bundle> {
+        assert!(ty.fields().is_empty());
+        ToSimValue::into_sim_value(BitVec::new(), ty)
+    }
+}
+
+impl<T: ?Sized> ToSimValue<CanonicalType> for PhantomData<T> {
+    #[track_caller]
+    fn to_sim_value(&self, ty: CanonicalType) -> SimValue<CanonicalType> {
+        let ty = Bundle::from_canonical(ty);
+        assert!(ty.fields().is_empty());
+        ToSimValue::into_sim_value(BitVec::new(), ty).into_canonical()
+    }
+}

crates/fayalite/src/memory.rs

@@ -519,7 +519,12 @@ impl<Element: Type, Len: Size> fmt::Debug for Mem<Element, Len> {
         f.debug_struct("Mem")
             .field("name", scoped_name)
             .field("array_type", array_type)
-            .field("initial_value", initial_value)
+            .field(
+                "initial_value",
+                &initial_value.as_ref().map(|initial_value| {
+                    DebugMemoryData::from_bit_slice(*array_type, initial_value)
+                }),
+            )
             .field("read_latency", read_latency)
             .field("write_latency", write_latency)
             .field("read_under_write", read_under_write)
@@ -1079,3 +1084,61 @@ pub fn splat_mask<T: Type>(ty: T, value: Expr<Bool>) -> Expr<AsMask<T>> {
         )),
     }
 }
+
+pub trait DebugMemoryDataGetElement {
+    fn get_element(&self, element_index: usize, array_type: Array) -> &BitSlice;
+}
+
+impl<'a, F: ?Sized + Fn(usize, Array) -> &'a BitSlice> DebugMemoryDataGetElement for &'a F {
+    fn get_element(&self, element_index: usize, array_type: Array) -> &BitSlice {
+        self(element_index, array_type)
+    }
+}
+
+#[derive(Clone)]
+pub struct DebugMemoryData<GetElement: DebugMemoryDataGetElement> {
+    pub array_type: Array,
+    pub get_element: GetElement,
+}
+
+impl DebugMemoryDataGetElement for &'_ BitSlice {
+    fn get_element(&self, element_index: usize, array_type: Array) -> &BitSlice {
+        assert!(element_index < array_type.len());
+        let stride = array_type.element().bit_width();
+        let start = element_index
+            .checked_mul(stride)
+            .expect("memory is too big");
+        let end = start.checked_add(stride).expect("memory is too big");
+        &self[start..end]
+    }
+}
+
+impl<'a> DebugMemoryData<&'a BitSlice> {
+    pub fn from_bit_slice<T: Type, Depth: Size>(
+        array_type: ArrayType<T, Depth>,
+        bit_slice: &'a BitSlice,
+    ) -> Self {
+        let array_type = array_type.as_dyn_array();
+        assert_eq!(bit_slice.len(), array_type.type_properties().bit_width);
+        Self {
+            array_type,
+            get_element: bit_slice,
+        }
+    }
+}
+
+impl<GetElement: DebugMemoryDataGetElement> fmt::Debug for DebugMemoryData<GetElement> {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        if self.array_type.len() == 0 {
+            return f.write_str("[]");
+        }
+        writeln!(f, "[\n    // len = {:#x}", self.array_type.len())?;
+        for element_index in 0..self.array_type.len() {
+            let element = crate::util::BitSliceWriteWithBase(
+                self.get_element.get_element(element_index, self.array_type),
+            );
+            writeln!(f, "    [{element_index:#x}]: {element:#x},")?;
+        }
+        f.write_str("]")
+    }
+}

crates/fayalite/src/sim/interpreter.rs

@@ -2,6 +2,7 @@
 // See Notices.txt for copyright information
 
 use crate::{
+    array::Array,
     int::{BoolOrIntType, SInt, UInt},
     intern::{Intern, Interned, Memoize},
     source_location::SourceLocation,
@@ -9,17 +10,17 @@ use crate::{
     util::get_many_mut,
 };
 use bitvec::{boxed::BitBox, slice::BitSlice};
-use hashbrown::HashMap;
+use hashbrown::{HashMap, HashSet};
 use num_bigint::BigInt;
 use num_traits::{One, Signed, ToPrimitive, Zero};
 use std::{
     any::TypeId,
     borrow::BorrowMut,
     convert::Infallible,
-    fmt,
+    fmt::{self, Write},
     hash::{Hash, Hasher},
     marker::PhantomData,
-    ops::{Deref, DerefMut, Index, IndexMut},
+    ops::{ControlFlow, Deref, DerefMut, Index, IndexMut},
 };
 use vec_map::VecMap;
 
@@ -174,7 +175,37 @@ fn make_array_into_iter<T, const I: usize, const N: usize>(
 
 impl fmt::Debug for Insn {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        self.debug_fmt::<InsnsBuildingDone>(f, None, None)
+        self.debug_fmt::<InsnsBuildingDone>(f, None, None, None)
+    }
+}
+
+struct PrefixLinesWrapper<'a, W> {
+    writer: W,
+    at_beginning_of_line: bool,
+    blank_line_prefix: &'a str,
+    line_prefix: &'a str,
+}
+
+impl<T: fmt::Write> fmt::Write for PrefixLinesWrapper<'_, T> {
+    fn write_str(&mut self, input: &str) -> fmt::Result {
+        for part in input.split_inclusive('\n') {
+            if part.is_empty() {
+                continue;
+            }
+            if self.at_beginning_of_line {
+                let prefix = match part {
+                    "\n" => self.blank_line_prefix,
+                    _ => self.line_prefix,
+                };
+                if !prefix.is_empty() {
+                    self.writer.write_str(prefix)?;
+                }
+                self.at_beginning_of_line = false;
+            }
+            self.writer.write_str(part)?;
+            self.at_beginning_of_line = part.ends_with('\n');
+        }
+        Ok(())
     }
 }
 
@@ -184,15 +215,22 @@ impl Insn {
         f: &mut fmt::Formatter<'_>,
         labels: Option<&Labels>,
         state_layout: Option<&StateLayout<BK>>,
+        state: Option<&State>,
     ) -> fmt::Result {
         let (insn_name, fields) = self.fields_with_names();
         write!(f, "{insn_name}")?;
         if fields.len() == 0 {
             return Ok(());
         }
+        let mut f = PrefixLinesWrapper {
+            writer: f,
+            at_beginning_of_line: false,
+            blank_line_prefix: "",
+            line_prefix: "    ",
+        };
         writeln!(f, " {{")?;
         for (field_name, field) in fields {
-            write!(f, "    {field_name}: ")?;
+            write!(f, "{field_name}: ")?;
             match field.kind {
                 InsnFieldKind::BranchTarget => match field.ty {
                     InsnFieldType::USize(&label_index) => {
@@ -227,35 +265,100 @@ impl Insn {
                 | InsnFieldKind::Output
                 | InsnFieldKind::Immediate => {}
             }
+            macro_rules! debug_fmt_state_part {
+                ($v:expr) => {
+                    $v.debug_fmt(&mut f, ",", " // ", "        // ", "", state_layout, state)
+                };
+            }
             match field.ty {
                 InsnFieldType::Memory(v) => {
-                    v.debug_fmt(f, ",", " // ", "", state_layout)?;
+                    debug_fmt_state_part!(v)?;
                 }
                 InsnFieldType::SmallSlot(v) => {
-                    v.debug_fmt(f, ",", " // ", "", state_layout)?;
+                    debug_fmt_state_part!(v)?;
                 }
                 InsnFieldType::BigSlot(v) => {
-                    v.debug_fmt(f, ",", " // ", "", state_layout)?;
+                    debug_fmt_state_part!(v)?;
                 }
                 InsnFieldType::SmallSlotArrayIndexed(v) => {
-                    v.debug_fmt(f, ",", " // ", "", state_layout)?;
+                    debug_fmt_state_part!(v)?;
                 }
                 InsnFieldType::BigSlotArrayIndexed(v) => {
-                    v.debug_fmt(f, ",", " // ", "", state_layout)?;
+                    debug_fmt_state_part!(v)?;
                 }
-                InsnFieldType::SmallUInt(v) => fmt::Debug::fmt(v, f)?,
-                InsnFieldType::SmallSInt(v) => fmt::Debug::fmt(v, f)?,
-                InsnFieldType::InternedBigInt(v) => fmt::Debug::fmt(v, f)?,
-                InsnFieldType::U8(v) => fmt::Debug::fmt(v, f)?,
-                InsnFieldType::USize(v) => fmt::Debug::fmt(v, f)?,
-                InsnFieldType::Empty(v) => fmt::Debug::fmt(v, f)?,
+                InsnFieldType::SmallUInt(v) => write!(f, "{v:#x}")?,
+                InsnFieldType::SmallSInt(v) => write!(f, "{v:#x}")?,
+                InsnFieldType::InternedBigInt(v) => write!(f, "{v:#x}")?,
+                InsnFieldType::U8(v) => write!(f, "{v:#x}")?,
+                InsnFieldType::USize(v) => write!(f, "{v}")?,
+                InsnFieldType::Empty(v) => write!(f, "{v:?}")?,
             }
             writeln!(f, ",")?;
         }
-        write!(f, "}}")
+        write!(f.writer, "}}")
     }
 }
 
+pub(crate) trait Breakpoints {
+    type Break;
+    fn check_for_breakpoint(&mut self, pc: usize) -> ControlFlow<Self::Break>;
+}
+
+impl<T: ?Sized + Breakpoints> Breakpoints for &'_ mut T {
+    type Break = T::Break;
+    fn check_for_breakpoint(&mut self, pc: usize) -> ControlFlow<Self::Break> {
+        T::check_for_breakpoint(self, pc)
+    }
+}
+
+impl<T: ?Sized + Breakpoints> Breakpoints for Box<T> {
+    type Break = T::Break;
+    fn check_for_breakpoint(&mut self, pc: usize) -> ControlFlow<Self::Break> {
+        T::check_for_breakpoint(self, pc)
+    }
+}
+
+impl Breakpoints for () {
+    type Break = Infallible;
+    fn check_for_breakpoint(&mut self, _pc: usize) -> ControlFlow<Self::Break> {
+        ControlFlow::Continue(())
+    }
+}
+
+pub(crate) struct BreakpointsSet {
+    pub(crate) last_was_break: bool,
+    pub(crate) set: HashSet<usize>,
+    pub(crate) trace: bool,
+}
+
+#[derive(Copy, Clone, Eq, PartialEq, Hash, Debug)]
+pub(crate) enum BreakAction {
+    DumpStateAndContinue,
+    Continue,
+}
+
+impl Breakpoints for BreakpointsSet {
+    type Break = BreakAction;
+    fn check_for_breakpoint(&mut self, pc: usize) -> ControlFlow<Self::Break> {
+        let retval = if self.last_was_break {
+            ControlFlow::Continue(())
+        } else if self.set.contains(&pc) {
+            ControlFlow::Break(BreakAction::DumpStateAndContinue)
+        } else if self.trace {
+            ControlFlow::Break(BreakAction::Continue)
+        } else {
+            ControlFlow::Continue(())
+        };
+        self.last_was_break = retval.is_break();
+        retval
+    }
+}
+
+pub(crate) enum RunResult<Break, Return> {
+    Break(Break),
+    Return(Return),
+}
+
 macro_rules! impl_insns {
     (
         #[insn = $Insn:ident, next_macro = $next_macro:ident, branch_macro = $branch_macro:ident]
@@ -402,11 +505,14 @@ macro_rules! impl_insns {
         }
 
         impl $State {
-            $vis fn $run(&mut $self) -> $run_ret_ty {
+            $vis fn $run<B: Breakpoints>(&mut $self, mut breakpoints: B) -> RunResult<B::Break, $run_ret_ty> {
                 let mut $state = $state_init;
                 $($setup)*
                 let mut insn = $state.insns[$state.pc];
                 let retval = 'main_loop: loop {
+                    if let ControlFlow::Break(b) = breakpoints.check_for_breakpoint($state.pc) {
+                        break RunResult::Break(b);
+                    }
                     macro_rules! $next_macro {
                         () => {
                             $state.pc += 1;
@@ -542,6 +648,7 @@ struct InsnsDebug<'a, BK: InsnsBuildingKind> {
     insn_source_locations: &'a [SourceLocation],
     labels: &'a BK::Labels,
     state_layout: &'a StateLayout<BK>,
+    state: Option<&'a State>,
 }
 
 struct InsnDebug<'a, BK: InsnsBuildingKind> {
@@ -550,6 +657,7 @@ struct InsnDebug<'a, BK: InsnsBuildingKind> {
     insn: &'a Insn,
     labels: Option<&'a Labels>,
     state_layout: &'a StateLayout<BK>,
+    state: Option<&'a State>,
 }
 
 impl<BK: InsnsBuildingKind> fmt::Debug for InsnDebug<'_, BK> {
@@ -565,7 +673,9 @@ impl<BK: InsnsBuildingKind> fmt::Debug for InsnDebug<'_, BK> {
         if let Some(source_location) = self.source_location {
             writeln!(f, "// at: {source_location}")?;
         }
-        self.insn.debug_fmt(f, self.labels, Some(self.state_layout))
+        write!(f, "{}: ", self.address)?;
+        self.insn
+            .debug_fmt(f, self.labels, Some(self.state_layout), self.state)
     }
 }
 
@@ -590,6 +700,7 @@ impl<'a, BK: InsnsBuildingKind> fmt::Debug for InsnsDebug<'a, BK> {
                 insn,
                 labels,
                 state_layout: self.state_layout,
+                state: self.state,
             });
             last_source_location = Some(source_location);
         }
@@ -597,8 +708,45 @@ impl<'a, BK: InsnsBuildingKind> fmt::Debug for InsnsDebug<'a, BK> {
     }
 }
 
-impl<BK: InsnsBuildingKind> fmt::Debug for Insns<BK> {
+impl<BK: InsnsBuildingKind> Insns<BK> {
+    pub(crate) fn debug_insn_at<'a>(
+        &'a self,
+        address: usize,
+        state: Option<&'a State>,
+    ) -> impl fmt::Debug + 'a {
+        let Self {
+            insns,
+            insn_source_locations,
+            labels,
+            state_layout,
+        } = self;
+        InsnDebug {
+            address,
+            source_location: Some(insn_source_locations[address]),
+            insn: &insns[address],
+            labels: BK::labels(labels),
+            state_layout,
+            state,
+        }
+    }
+}
+
+impl State {
+    pub(crate) fn debug_insn_at(&self, address: usize) -> impl fmt::Debug + '_ {
+        self.insns.debug_insn_at(address, Some(self))
+    }
+}
+
+struct InsnsOfState<'a>(&'a State);
+
+impl fmt::Debug for InsnsOfState<'_> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        self.0.insns.debug_fmt(Some(self.0), f)
+    }
+}
+
+impl<BK: InsnsBuildingKind> Insns<BK> {
+    fn debug_fmt(&self, state: Option<&State>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         let Self {
             insns,
             insn_source_locations,
@@ -614,12 +762,19 @@ impl<BK: InsnsBuildingKind> fmt::Debug for Insns<BK> {
                     insn_source_locations,
                     labels,
                     state_layout,
+                    state,
                 },
             )
             .finish_non_exhaustive()
     }
 }
 
+impl<BK: InsnsBuildingKind> fmt::Debug for Insns<BK> {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        self.debug_fmt(None, f)
+    }
+}
+
 pub(crate) trait StatePartKind:
     Send + Sync + Ord + Hash + fmt::Debug + 'static + Copy + Default
 {
@@ -634,6 +789,11 @@ pub(crate) trait StatePartKind:
         state_layout: &StateLayout<BK>,
         part_index: StatePartIndex<Self>,
     ) -> Option<&Self::DebugData>;
+    fn debug_fmt_state_value(
+        state: &State,
+        index: StatePartIndex<Self>,
+        f: &mut impl fmt::Write,
+    ) -> fmt::Result;
 }
 
 pub(crate) trait StatePartsValue {
@@ -986,7 +1146,6 @@ macro_rules! make_state_part_kinds {
             }
         }
 
-        #[derive(Debug)]
         pub(crate) struct State {
             pub(crate) insns: Interned<Insns<InsnsBuildingDone>>,
             pub(crate) pc: usize,
@@ -995,6 +1154,25 @@ macro_rules! make_state_part_kinds {
             $(pub(crate) $type_field: StatePart<$TypeKind>,)*
         }
 
+        impl fmt::Debug for State {
+            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+                let Self {
+                    insns: _,
+                    pc,
+                    memory_write_log,
+                    $($state_field,)*
+                    $($type_field,)*
+                } = self;
+                f.debug_struct("State")
+                    .field("insns", &InsnsOfState(self))
+                    .field("pc", pc)
+                    .field("memory_write_log", memory_write_log)
+                    $(.field(stringify!($state_field), $state_field))*
+                    $(.field(stringify!($type_field), $type_field))*
+                    .finish()
+            }
+        }
+
         impl State {
             pub(crate) fn new(insns: Interned<Insns<InsnsBuildingDone>>) -> Self {
                 Self {
@@ -1198,6 +1376,25 @@ macro_rules! make_state_part_kinds {
     };
 }
 
+#[derive(Copy, Clone, Hash, PartialEq, Eq)]
+pub(crate) struct MemoryData<T: Deref<Target = BitSlice>> {
+    pub(crate) array_type: Array,
+    pub(crate) data: T,
+}
+
+impl<T: Deref<Target = BitSlice>> fmt::Debug for MemoryData<T> {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        let Self { array_type, data } = self;
+        f.debug_struct("MemoryData")
+            .field("array_type", array_type)
+            .field(
+                "data",
+                &crate::memory::DebugMemoryData::from_bit_slice(*array_type, data),
+            )
+            .finish()
+    }
+}
+
 make_state_part_kinds! {
     /*#[state, field = small_stack]
     impl StatePartKind for StatePartKindSmallStack {
@@ -1243,11 +1440,14 @@ make_state_part_kinds! {
     impl StatePartKind for StatePartKindMemories {
         const NAME: &'static str = "Memories";
         type DebugData = ();
-        type LayoutData = Interned<BitSlice>;
-        type State = Box<[BitBox]>;
-        type BorrowedState<'a> = &'a mut [BitBox];
+        type LayoutData = MemoryData<Interned<BitSlice>>;
+        type State = Box<[MemoryData<BitBox>]>;
+        type BorrowedState<'a> = &'a mut [MemoryData<BitBox>];
         fn new_state(layout_data: &[Self::LayoutData]) -> Self::State {
-            layout_data.iter().map(|initial_data| BitBox::from_bitslice(initial_data)).collect()
+            layout_data.iter().map(|MemoryData { array_type, data }| MemoryData {
+                array_type: *array_type,
+                data: BitBox::from_bitslice(data),
+            }).collect()
         }
         fn borrow_state<'a>(state: &'a mut Self::State) -> Self::BorrowedState<'a> {
             state
@@ -1258,6 +1458,13 @@ make_state_part_kinds! {
         ) -> Option<&Self::DebugData> {
             state_layout.memories.debug_data.get(part_index.as_usize())
         }
+        fn debug_fmt_state_value(
+            state: &State,
+            index: StatePartIndex<Self>,
+            f: &mut impl fmt::Write,
+        ) -> fmt::Result {
+            write!(f, "{:#?}", &state.memories[index])
+        }
     }
     #[type, field = small_slots]
     impl StatePartKind for StatePartKindSmallSlots {
@@ -1278,6 +1485,15 @@ make_state_part_kinds! {
         ) -> Option<&Self::DebugData> {
             state_layout.ty.small_slots.debug_data.get(part_index.as_usize())
         }
+        fn debug_fmt_state_value(
+            state: &State,
+            index: StatePartIndex<Self>,
+            f: &mut impl fmt::Write,
+        ) -> fmt::Result {
+            let value = state.small_slots[index];
+            write!(f, "{value:#x} {}", value as SmallSInt)?;
+            Ok(())
+        }
     }
     #[type, field = big_slots]
     impl StatePartKind for StatePartKindBigSlots {
@@ -1298,6 +1514,13 @@ make_state_part_kinds! {
         ) -> Option<&Self::DebugData> {
             state_layout.ty.big_slots.debug_data.get(part_index.as_usize())
         }
+        fn debug_fmt_state_value(
+            state: &State,
+            index: StatePartIndex<Self>,
+            f: &mut impl fmt::Write,
+        ) -> fmt::Result {
+            write!(f, "{:#x}", state.big_slots[index])
+        }
     }
 }
 
@@ -1473,37 +1696,32 @@ pub(crate) struct StatePartArrayIndexed<K: StatePartKind> {
 impl<K: StatePartKind> StatePartArrayIndexed<K> {
     pub(crate) fn debug_fmt<BK: InsnsBuildingKind>(
         &self,
-        f: &mut fmt::Formatter<'_>,
+        f: &mut impl fmt::Write,
         before_debug_info_text: &str,
         comment_start: &str,
+        comment_line_start: &str,
         comment_end: &str,
         state_layout: Option<&StateLayout<BK>>,
+        state: Option<&State>,
     ) -> fmt::Result {
-        if let Some(state_layout) = state_layout {
-            let Self { base, indexes } = *self;
-            if indexes.is_empty() {
-                base.debug_fmt(
-                    f,
-                    before_debug_info_text,
-                    comment_start,
-                    comment_end,
-                    Some(state_layout),
-                )
-            } else {
-                base.debug_fmt(f, "", " /* ", " */ ", Some(state_layout))?;
-                for StatePartArrayIndex { index, len, stride } in indexes {
-                    f.write_str("[")?;
-                    index.debug_fmt(f, "", " /* ", " */ ", Some(state_layout))?;
-                    write!(f, ", len={len}, stride={}]", stride.value)?;
-                }
-                f.write_str(before_debug_info_text)
-            }
+        let Self { base, indexes } = *self;
+        if indexes.is_empty() {
+            base.debug_fmt(
+                f,
+                before_debug_info_text,
+                comment_start,
+                comment_line_start,
+                comment_end,
+                state_layout,
+                state,
+            )
         } else {
-            let Self { base, indexes } = self;
-            f.debug_struct("StatePartArrayIndexed")
-                .field("base", base)
-                .field("indexes", indexes)
-                .finish()?;
+            base.debug_fmt(f, "", " /* ", "", " */ ", state_layout, state)?;
+            for StatePartArrayIndex { index, len, stride } in indexes {
+                f.write_str("[")?;
+                index.debug_fmt(f, "", " /* ", "", " */ ", state_layout, state)?;
+                write!(f, ", len={len}, stride={}]", stride.value)?;
+            }
             f.write_str(before_debug_info_text)
         }
     }
@@ -1511,7 +1729,7 @@ impl<K: StatePartKind> StatePartArrayIndexed<K> {
 
 impl<K: StatePartKind + fmt::Debug> fmt::Debug for StatePartArrayIndexed<K> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        self.debug_fmt::<InsnsBuildingDone>(f, "", "", "", None)
+        self.debug_fmt::<InsnsBuildingDone>(f, "", "", "", "", None, None)
     }
 }
 
@@ -1578,18 +1796,40 @@ impl<K: StatePartKind> StatePartIndex<K> {
     }
     pub(crate) fn debug_fmt<BK: InsnsBuildingKind>(
         &self,
-        f: &mut fmt::Formatter<'_>,
+        f: &mut impl fmt::Write,
         before_debug_info_text: &str,
         comment_start: &str,
+        comment_line_start: &str,
         comment_end: &str,
         state_layout: Option<&StateLayout<BK>>,
+        state: Option<&State>,
     ) -> fmt::Result {
         write!(f, "StatePartIndex<{}>({})", K::NAME, self.value)?;
         f.write_str(before_debug_info_text)?;
-        if let Some(state_layout) = state_layout {
-            if let Some(debug_data) = K::part_debug_data(state_layout, *self) {
-                write!(f, "{comment_start}{debug_data:?}{comment_end}")?;
-            }
+        let debug_data =
+            state_layout.and_then(|state_layout| K::part_debug_data(state_layout, *self));
+        if state.is_some() || debug_data.is_some() {
+            f.write_str(comment_start)?;
+        }
+        let mut f = PrefixLinesWrapper {
+            writer: f,
+            at_beginning_of_line: false,
+            blank_line_prefix: comment_line_start.trim_end(),
+            line_prefix: comment_line_start,
+        };
+        if let Some(state) = state {
+            f.write_str("(")?;
+            K::debug_fmt_state_value(state, *self, &mut f)?;
+            f.write_str(")")?;
+        }
+        if state.is_some() && debug_data.is_some() {
+            f.write_str(" ")?;
+        }
+        if let Some(debug_data) = debug_data {
+            write!(f, "{debug_data:?}")?;
+        }
+        if state.is_some() || debug_data.is_some() {
+            f.writer.write_str(comment_end)?;
         }
         Ok(())
     }
@@ -1597,7 +1837,7 @@ impl<K: StatePartKind> StatePartIndex<K> {
 
 impl<K: StatePartKind> fmt::Debug for StatePartIndex<K> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        self.debug_fmt::<InsnsBuildingDone>(f, "", "", "", None)
+        self.debug_fmt::<InsnsBuildingDone>(f, "", "", "", "", None, None)
     }
 }
 
@@ -1711,7 +1951,7 @@ impl<K: StatePartKind, BK: InsnsBuildingKind> fmt::Debug for StatePartLayout<K,
             layout_data,
             _phantom: _,
         } = self;
-        write!(f, "StatePartAllocationLayout<{}>", K::NAME)?;
+        write!(f, "StatePartLayout<{}>", K::NAME)?;
         let mut debug_struct = f.debug_struct("");
         debug_struct
             .field("len", &debug_data.len())
@@ -2181,7 +2421,7 @@ impl BorrowedState<'_> {
         let Ok(addr) = usize::try_from(addr) else {
             return;
         };
-        if addr < self.memories.value.len() {
+        if addr < self.memories[memory].array_type.len() {
             let log_entry = (memory, addr);
             if self.memory_write_log.last().copied() == Some(log_entry) {
                 return;
@@ -2520,6 +2760,18 @@ impl_insns! {
         state.big_slots[dest] = value;
         next!();
     }
+    XorSmallImmediate {
+        #[kind = Output]
+        dest: StatePartIndex<StatePartKindSmallSlots>,
+        #[kind = Input]
+        lhs: StatePartIndex<StatePartKindSmallSlots>,
+        #[kind = Immediate]
+        rhs: SmallUInt,
+    } => {
+        let value = state.small_slots[lhs] ^ rhs;
+        state.small_slots[dest] = value;
+        next!();
+    }
     NotS {
         #[kind = Output]
         dest: StatePartIndex<StatePartKindBigSlots>,
@@ -2542,16 +2794,6 @@ impl_insns! {
         state.big_slots[dest] = value;
         next!();
     }
-    NotSmall {
-        #[kind = Output]
-        dest: StatePartIndex<StatePartKindSmallSlots>,
-        #[kind = Input]
-        src: StatePartIndex<StatePartKindSmallSlots>,
-    } => {
-        let value = !state.small_slots[src];
-        state.small_slots[dest] = value;
-        next!();
-    }
     Neg {
         #[kind = Output]
         dest: StatePartIndex<StatePartKindBigSlots>,
@@ -2878,7 +3120,7 @@ impl_insns! {
         width: usize,
     } => {
         let addr = state.small_slots[addr];
-        state.big_slots[dest] = memory_read_big::<UInt>(&mut state.memories[memory], addr, stride, start, width).unwrap_or_default();
+        state.big_slots[dest] = memory_read_big::<UInt>(&mut state.memories[memory].data, addr, stride, start, width).unwrap_or_default();
         next!();
     }
     MemoryReadSInt {
@@ -2896,7 +3138,7 @@ impl_insns! {
         width: usize,
     } => {
         let addr = state.small_slots[addr];
-        state.big_slots[dest] = memory_read_big::<SInt>(&mut state.memories[memory], addr, stride, start, width).unwrap_or_default();
+        state.big_slots[dest] = memory_read_big::<SInt>(&mut state.memories[memory].data, addr, stride, start, width).unwrap_or_default();
         next!();
     }
     MemoryWriteUInt {
@@ -2914,7 +3156,7 @@ impl_insns! {
         width: usize,
     } => {
         let addr = state.small_slots[addr];
-        memory_write_big::<UInt>(&mut state.memories[memory], addr, stride, start, width, &mut state.big_slots[value]);
+        memory_write_big::<UInt>(&mut state.memories[memory].data, addr, stride, start, width, &mut state.big_slots[value]);
         state.log_memory_write(memory, addr);
         next!();
     }
@@ -2933,11 +3175,11 @@ impl_insns! {
         width: usize,
     } => {
         let addr = state.small_slots[addr];
-        memory_write_big::<SInt>(&mut state.memories[memory], addr, stride, start, width, &mut state.big_slots[value]);
+        memory_write_big::<SInt>(&mut state.memories[memory].data, addr, stride, start, width, &mut state.big_slots[value]);
         state.log_memory_write(memory, addr);
         next!();
     }
     Return => {
-        break;
+        break RunResult::Return(());
     }
 }

crates/fayalite/src/util/ready_valid.rs

@@ -195,7 +195,7 @@ mod tests {
         assert_formal(
             format_args!("test_queue_{capacity}_{inp_ready_is_comb}_{out_valid_is_comb}"),
             queue_test(capacity, inp_ready_is_comb, out_valid_is_comb),
-            FormalMode::Prove,
+            FormalMode::BMC,
             14,
             None,
             ExportOptions {
@@ -203,6 +203,24 @@ mod tests {
                 ..ExportOptions::default()
             },
         );
+        /// Formal verification of the FIFO queue
+        ///
+        /// The strategy derives from the observation that, if we filter its
+        /// input and output streams to consider just one in every N reads and
+        /// writes (where N is the FIFO capacity), then the FIFO effectively
+        /// behaves as an one-entry FIFO.
+        ///
+        /// In particular, any counterexample of the full FIFO behaving badly
+        /// will also be caught by one of the filtered versions (one which
+        /// happens to be in phase with the offending input or output).
+        ///
+        /// Interestingly, this strategy seems to be simpler than the one
+        /// described on the [Asynchronous FIFO] and the [FIFO tutorial]
+        /// articles of the ZipCPU blog, which considers two adjacent writes
+        /// and reads.
+        ///
+        /// [Asynchronous FIFO]: https://zipcpu.com/blog/2018/07/06/afifo.html#fifo-contract
+        /// [FIFO tutorial]: https://zipcpu.com/tutorial/lsn-10-fifo.pdf
         #[hdl_module]
         fn queue_test(capacity: NonZeroUsize, inp_ready_is_comb: bool, out_valid_is_comb: bool) {
             #[hdl]
@@ -217,6 +235,8 @@ mod tests {
                     rst: formal_reset().to_reset(),
                 },
             );
+
+            // random input data
             #[hdl]
             let inp_data: HdlOption<UInt<8>> = wire();
             #[hdl]
@@ -225,16 +245,25 @@ mod tests {
             } else {
                 connect(inp_data, HdlNone());
             }
+
+            // assert output ready at random
             #[hdl]
             let out_ready: Bool = wire();
             connect(out_ready, any_seq(Bool));
-            let index_ty: UInt<32> = UInt::TYPE;
+
+            // The current number of elements in the FIFO ranges from zero to
+            // maximum capacity, inclusive.
+            let count_ty = UInt::range_inclusive(0..=capacity.get());
+            // type for counters that wrap around at the FIFO capacity
+            let index_ty = UInt::range(0..capacity.get());
+
+            // among all entries of the FIFO internal circular memory, choose
+            // one at random to check
             #[hdl]
-            let index_to_check = wire();
+            let index_to_check = wire(index_ty);
             connect(index_to_check, any_const(index_ty));
-            let index_max = !index_ty.zero();
-            // we saturate at index_max, so only check indexes where we properly maintain position
-            hdl_assume(clk, index_to_check.cmp_ne(index_max), "");
+
+            // instantiate and connect the queue
             #[hdl]
             let dut = instance(queue(
                 UInt[ConstUsize::<8>],
@@ -245,108 +274,121 @@ mod tests {
             connect(dut.cd, cd);
             connect(dut.inp.data, inp_data);
             connect(dut.out.ready, out_ready);
-            hdl_assume(
-                clk,
-                index_to_check.cmp_ne(!Expr::ty(index_to_check).zero()),
-                "",
-            );
 
+            // Keep an independent count of words in the FIFO. Ensure that
+            // it's always correct, and never overflows.
             #[hdl]
-            let expected_count_reg = reg_builder().clock_domain(cd).reset(0u32);
-            #[hdl]
-            let next_expected_count = wire();
-            connect(next_expected_count, expected_count_reg);
-            connect(expected_count_reg, next_expected_count);
+            let expected_count_reg = reg_builder().clock_domain(cd).reset(count_ty.zero());
             #[hdl]
             if ReadyValid::firing(dut.inp) & !ReadyValid::firing(dut.out) {
-                connect_any(next_expected_count, expected_count_reg + 1u8);
+                hdl_assert(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) {
-                connect_any(next_expected_count, expected_count_reg - 1u8);
+                hdl_assert(clk, expected_count_reg.cmp_ne(count_ty.zero()), "");
+                connect_any(expected_count_reg, expected_count_reg - 1u8);
             }
-            hdl_assert(cd.clk, expected_count_reg.cmp_eq(dut.count), "");
-
-            #[hdl]
-            let prev_out_ready_reg = reg_builder().clock_domain(cd).reset(!0_hdl_u3);
-            connect_any(
-                prev_out_ready_reg,
-                (prev_out_ready_reg << 1) | out_ready.cast_to(UInt[1]),
-            );
-            #[hdl]
-            let prev_inp_valid_reg = reg_builder().clock_domain(cd).reset(!0_hdl_u3);
-            connect_any(
-                prev_inp_valid_reg,
-                (prev_inp_valid_reg << 1) | HdlOption::is_some(inp_data).cast_to(UInt[1]),
-            );
-            hdl_assume(
-                clk,
-                (prev_out_ready_reg & prev_inp_valid_reg).cmp_ne(0u8),
-                "",
-            );
+            hdl_assert(clk, expected_count_reg.cmp_eq(dut.count), "");
 
+            // keep an independent write index into the FIFO's circular buffer
             #[hdl]
             let inp_index_reg = reg_builder().clock_domain(cd).reset(index_ty.zero());
             #[hdl]
-            let stored_inp_data_reg = reg_builder().clock_domain(cd).reset(0u8);
-
-            #[hdl]
-            if let HdlSome(data) = ReadyValid::firing_data(dut.inp) {
+            if ReadyValid::firing(dut.inp) {
                 #[hdl]
-                if inp_index_reg.cmp_lt(index_max) {
+                if inp_index_reg.cmp_ne(capacity.get() - 1) {
                     connect_any(inp_index_reg, inp_index_reg + 1u8);
-                    #[hdl]
-                    if inp_index_reg.cmp_eq(index_to_check) {
-                        connect(stored_inp_data_reg, data);
-                    }
+                } else {
+                    connect_any(inp_index_reg, 0_hdl_u0);
                 }
             }
 
-            #[hdl]
-            if inp_index_reg.cmp_lt(index_to_check) {
-                hdl_assert(clk, stored_inp_data_reg.cmp_eq(0u8), "");
-            }
-
+            // keep an independent read index into the FIFO's circular buffer
             #[hdl]
             let out_index_reg = reg_builder().clock_domain(cd).reset(index_ty.zero());
             #[hdl]
-            let stored_out_data_reg = reg_builder().clock_domain(cd).reset(0u8);
-
-            #[hdl]
-            if let HdlSome(data) = ReadyValid::firing_data(dut.out) {
+            if ReadyValid::firing(dut.out) {
                 #[hdl]
-                if out_index_reg.cmp_lt(index_max) {
+                if out_index_reg.cmp_ne(capacity.get() - 1) {
                     connect_any(out_index_reg, out_index_reg + 1u8);
-                    #[hdl]
-                    if out_index_reg.cmp_eq(index_to_check) {
-                        connect(stored_out_data_reg, data);
-                    }
+                } else {
+                    connect_any(out_index_reg, 0_hdl_u0);
                 }
             }
 
+            // filter the input data stream, predicated by the read index
+            // matching the chosen position in the FIFO's circular buffer
             #[hdl]
-            if out_index_reg.cmp_lt(index_to_check) {
-                hdl_assert(clk, stored_out_data_reg.cmp_eq(0u8), "");
+            let inp_index_matches = wire();
+            connect(inp_index_matches, inp_index_reg.cmp_eq(index_to_check));
+            #[hdl]
+            let inp_firing_data = wire();
+            connect(inp_firing_data, HdlNone());
+            #[hdl]
+            if inp_index_matches {
+                connect(inp_firing_data, ReadyValid::firing_data(dut.inp));
             }
 
-            hdl_assert(clk, inp_index_reg.cmp_ge(out_index_reg), "");
-
+            // filter the output data stream, predicated by the write index
+            // matching the chosen position in the FIFO's circular buffer
             #[hdl]
-            if inp_index_reg.cmp_lt(index_max) & out_index_reg.cmp_lt(index_max) {
-                hdl_assert(
-                    clk,
-                    expected_count_reg.cmp_eq(inp_index_reg - out_index_reg),
-                    "",
-                );
-            } else {
-                hdl_assert(
-                    clk,
-                    expected_count_reg.cmp_ge(inp_index_reg - out_index_reg),
-                    "",
-                );
+            let out_index_matches = wire();
+            connect(out_index_matches, out_index_reg.cmp_eq(index_to_check));
+            #[hdl]
+            let out_firing_data = wire();
+            connect(out_firing_data, HdlNone());
+            #[hdl]
+            if out_index_matches {
+                connect(out_firing_data, ReadyValid::firing_data(dut.out));
             }
 
+            // Implement an one-entry FIFO and ensure its equivalence to the
+            // filtered FIFO.
+            //
+            // the holding register for our one-entry FIFO
             #[hdl]
-            if inp_index_reg.cmp_gt(index_to_check) & out_index_reg.cmp_gt(index_to_check) {
-                hdl_assert(clk, stored_inp_data_reg.cmp_eq(stored_out_data_reg), "");
+            let stored_reg = reg_builder().clock_domain(cd).reset(HdlNone());
+            #[hdl]
+            match stored_reg {
+                // If the holding register is empty...
+                HdlNone => {
+                    #[hdl]
+                    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), ""),
+                        // If we are indeed receiving some data...
+                        HdlSome(data_in) => {
+                            #[hdl]
+                            match out_firing_data {
+                                // ... 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), ""),
+                                // If we are receiving, but not transmitting,
+                                // store the received data in the holding
+                                // register.
+                                HdlNone => connect(stored_reg, HdlSome(data_in)),
+                            }
+                        }
+                    }
+                }
+                // If there is some value stored in the holding register...
+                HdlSome(stored) => {
+                    #[hdl]
+                    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), ""),
+                        // 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), "");
+                            // Also, accept new data, if any. Otherwise,
+                            // let the holding register become empty.
+                            connect(stored_reg, inp_firing_data);
+                        }
+                    }
+                }
             }
         }
     }

crates/fayalite/tests/formal.rs

@@ -7,12 +7,13 @@ use fayalite::{
     clock::{Clock, ClockDomain},
     expr::{CastTo, HdlPartialEq},
     firrtl::ExportOptions,
-    formal::{any_seq, formal_reset, hdl_assert, hdl_assume},
-    hdl_module,
-    int::{Bool, UInt},
-    module::{connect, connect_any, reg_builder, wire},
+    formal::{any_const, any_seq, formal_reset, hdl_assert, hdl_assume},
+    hdl, hdl_module,
+    int::{Bool, DynSize, Size, UInt, UIntType},
+    module::{connect, connect_any, instance, memory, reg_builder, wire},
     reset::ToReset,
     testing::assert_formal,
+    ty::StaticType,
 };
 
 /// Test hidden state
@@ -131,3 +132,164 @@ mod hidden_state {
         );
     }
 }
+
+/// Formal verification of designs containing memories
+///
+/// There is a trick for memories, described in the [Zipcpu blog].
+/// First, select a fixed but arbitrary memory address, monitoring all reads
+/// and writes made to it. Then, assert that anything read from that location
+/// matches the last stored value.
+///
+/// A difficulty for induction is that the memory represents [hidden_state]. A
+/// solution is to include an additional read port to the memory and assert
+/// that the memory location effectively contains the last stored value.
+/// This additional debug port is present only to assist the proof and is
+/// unused (optimized out) in actual use.
+///
+/// [Zipcpu blog]: <https://zipcpu.com/zipcpu/2018/07/13/memories.html>
+mod memory {
+    use super::*;
+
+    /// Test a simple 8-bit SRAM model
+    #[test]
+    fn test_sram() {
+        #[hdl]
+        struct WritePort<AddrWidth: Size> {
+            addr: UIntType<AddrWidth>,
+            data: UInt<8>,
+            en: Bool,
+        }
+        #[hdl]
+        struct ReadPort<AddrWidth: Size> {
+            addr: UIntType<AddrWidth>,
+            #[hdl(flip)]
+            data: UInt<8>,
+        }
+        /// This debug port is only meant to assist the proof.
+        /// For normal use in a design, a wrapper could be provided,
+        /// omitting this port.
+        /// The implementation is forbidden to use any information
+        /// provided on this port in its internal workings.
+        #[hdl]
+        struct DebugPort<AddrWidth: Size> {
+            selected: UIntType<AddrWidth>,
+            stored: UInt<8>,
+            wrote: Bool,
+        }
+        /// simple 1R1W SRAM model (one asynchronous read port and one
+        /// independent write port) with `n`-bit address width
+        #[hdl_module]
+        fn example_sram(n: usize) {
+            #[hdl]
+            let wr: WritePort<DynSize> = m.input(WritePort[n]);
+            #[hdl]
+            let rd: ReadPort<DynSize> = m.input(ReadPort[n]);
+            #[hdl]
+            let cd: ClockDomain = m.input();
+
+            // declare and connect the backing memory
+            #[hdl]
+            let mut mem = memory();
+            mem.depth(1 << n);
+            let read_port = mem.new_read_port();
+            let write_port = mem.new_write_port();
+            connect(write_port.clk, cd.clk);
+            connect(write_port.addr, wr.addr);
+            connect(write_port.en, wr.en);
+            connect(write_port.data, wr.data);
+            connect(write_port.mask, true);
+            connect(read_port.clk, cd.clk);
+            connect(read_port.addr, rd.addr);
+            connect(read_port.en, true);
+            connect(rd.data, read_port.data);
+
+            // To assist with induction, ensure that the chosen memory location
+            // really contains, always, the last value written to it.
+            #[hdl]
+            let dbg: DebugPort<DynSize> = m.input(DebugPort[n]);
+            let debug_port = mem.new_read_port();
+            connect(debug_port.en, true);
+            connect(debug_port.clk, cd.clk);
+            connect(debug_port.addr, dbg.selected);
+            #[hdl]
+            if dbg.wrote {
+                hdl_assert(cd.clk, debug_port.data.cmp_eq(dbg.stored), "");
+                // Try commenting out the assert above, induction will fail.
+                // Opening the trace, it can be seen that the memory contents
+                // and the stored value don't match, which is an unreachable
+                // state. By asserting the above, it will become invalid
+                // as well, so induction will skip this kind of situation.
+            }
+        }
+
+        /// formal verification of the SRAM module, parametrized by the
+        /// address bit-width
+        #[hdl_module]
+        fn test_module(n: usize) {
+            #[hdl]
+            let clk: Clock = m.input();
+            let cd = #[hdl]
+            ClockDomain {
+                clk,
+                rst: formal_reset().to_reset(),
+            };
+
+            // instantiate the SRAM model, connecting its inputs to
+            // a random sequence
+            #[hdl]
+            let rd: ReadPort<DynSize> = wire(ReadPort[n]);
+            connect(rd.addr, any_seq(UInt[n]));
+            #[hdl]
+            let wr: WritePort<DynSize> = wire(WritePort[n]);
+            connect(wr.addr, any_seq(UInt[n]));
+            connect(wr.data, any_seq(UInt::<8>::TYPE));
+            connect(wr.en, any_seq(Bool));
+            #[hdl]
+            let dut = instance(example_sram(n));
+            connect(dut.cd, cd);
+            connect(dut.rd, rd);
+            connect(dut.wr, wr);
+
+            // select a fixed but arbitrary test address
+            #[hdl]
+            let selected = wire(UInt[n]);
+            connect(selected, any_const(UInt[n]));
+            // store the last value written to that address
+            #[hdl]
+            let stored: UInt<8> = reg_builder().clock_domain(cd).reset(0u8);
+            // since memories are not initialized, track whether we wrote to the
+            // memory at least once
+            #[hdl]
+            let wrote: Bool = reg_builder().clock_domain(cd).reset(false);
+            // on a write, capture the last written value
+            #[hdl]
+            if wr.en & wr.addr.cmp_eq(selected) {
+                connect(stored, wr.data);
+                connect(wrote, true);
+            }
+            // on a read, assert that the read value is the same which was stored
+            #[hdl]
+            if rd.addr.cmp_eq(selected) & wrote {
+                hdl_assert(clk, rd.data.cmp_eq(stored), "");
+            }
+
+            // to assist induction, pass our state to the underlying instance
+            let dbg = #[hdl]
+            DebugPort {
+                selected,
+                stored,
+                wrote,
+            };
+            connect(dut.dbg, dbg);
+        }
+
+        assert_formal(
+            "sram",
+            test_module(8),
+            FormalMode::Prove,
+            2,
+            None,
+            ExportOptions::default(),
+        );
+    }
+}

crates/fayalite/tests/sim.rs

@@ -5,7 +5,8 @@ use fayalite::{
     int::UIntValue,
     prelude::*,
     reset::ResetType,
-    sim::{time::SimDuration, vcd::VcdWriterDecls, Simulation},
+    sim::{time::SimDuration, vcd::VcdWriterDecls, Simulation, ToSimValue},
+    ty::StaticType,
     util::RcWriter,
 };
 use std::num::NonZeroUsize;
@@ -254,8 +255,14 @@ fn test_shift_register() {
     let mut sim = Simulation::new(shift_register());
     let mut writer = RcWriter::default();
     sim.add_trace_writer(VcdWriterDecls::new(writer.clone()));
-    sim.write_clock(sim.io().cd.clk, false);
-    sim.write_reset(sim.io().cd.rst, true);
+    sim.write(
+        sim.io().cd,
+        #[hdl]
+        ClockDomain {
+            clk: false.to_clock(),
+            rst: true.to_sync_reset(),
+        },
+    );
     sim.write_bool(sim.io().d, false);
     sim.advance_time(SimDuration::from_micros(1));
     sim.write_clock(sim.io().cd.clk, true);
@@ -271,7 +278,7 @@ fn test_shift_register() {
                 assert_eq!(
                     *expected,
                     sim.read_bool(sim.io().q),
-                    "cycle: {cycle}\nvcd:\n{}",
+                    "vcd:\n{}\ncycle: {cycle}",
                     String::from_utf8(writer.take()).unwrap(),
                 );
             }
@@ -309,6 +316,8 @@ pub fn enums() {
     let which_out: UInt<2> = m.output();
     #[hdl]
     let data_out: UInt<4> = m.output();
+    #[hdl]
+    let b_out: HdlOption<(UInt<1>, Bool)> = m.output();
 
     #[hdl]
     struct MyStruct<T> {
@@ -348,6 +357,8 @@ pub fn enums() {
         }
     }
 
+    connect(b_out, HdlNone());
+
     #[hdl]
     match the_reg {
         MyEnum::A => {
@@ -357,6 +368,7 @@ pub fn enums() {
         MyEnum::B(v) => {
             connect(which_out, 1_hdl_u2);
             connect_any(data_out, v.0 | (v.1.cast_to_static::<UInt<1>>() << 1));
+            connect(b_out, HdlSome(v));
         }
         MyEnum::C(v) => {
             connect(which_out, 2_hdl_u2);
@@ -382,13 +394,33 @@ fn test_enums() {
     sim.advance_time(SimDuration::from_nanos(100));
     sim.write_reset(sim.io().cd.rst, false);
     sim.advance_time(SimDuration::from_nanos(900));
-    #[derive(Debug, PartialEq, Eq)]
+    type BOutTy = HdlOption<(UInt<1>, Bool)>;
+    #[derive(Debug)]
     struct IO {
         en: bool,
         which_in: u8,
         data_in: u8,
         which_out: u8,
         data_out: u8,
+        b_out: Expr<BOutTy>,
+    }
+    impl PartialEq for IO {
+        fn eq(&self, other: &Self) -> bool {
+            let Self {
+                en,
+                which_in,
+                data_in,
+                which_out,
+                data_out,
+                b_out,
+            } = *self;
+            en == other.en
+                && which_in == other.which_in
+                && data_in == other.data_in
+                && which_out == other.which_out
+                && data_out == other.data_out
+                && b_out.to_sim_value(BOutTy::TYPE) == other.b_out.to_sim_value(BOutTy::TYPE)
+        }
     }
     let io_cycles = [
         IO {
@@ -397,6 +429,7 @@ fn test_enums() {
             data_in: 0,
             which_out: 0,
             data_out: 0,
+            b_out: HdlNone(),
         },
         IO {
             en: true,
@@ -404,6 +437,7 @@ fn test_enums() {
             data_in: 0,
             which_out: 0,
             data_out: 0,
+            b_out: HdlNone(),
         },
         IO {
             en: false,
@@ -411,6 +445,7 @@ fn test_enums() {
             data_in: 0,
             which_out: 1,
             data_out: 0,
+            b_out: HdlSome((0_hdl_u1, false)),
         },
         IO {
             en: true,
@@ -418,6 +453,7 @@ fn test_enums() {
             data_in: 0xF,
             which_out: 1,
             data_out: 0,
+            b_out: HdlSome((0_hdl_u1, false)),
         },
         IO {
             en: true,
@@ -425,6 +461,7 @@ fn test_enums() {
             data_in: 0xF,
             which_out: 1,
             data_out: 0x3,
+            b_out: HdlSome((1_hdl_u1, true)),
         },
         IO {
             en: true,
@@ -432,6 +469,7 @@ fn test_enums() {
             data_in: 0xF,
             which_out: 1,
             data_out: 0x3,
+            b_out: HdlSome((1_hdl_u1, true)),
         },
         IO {
             en: true,
@@ -439,6 +477,7 @@ fn test_enums() {
             data_in: 0xF,
             which_out: 2,
             data_out: 0xF,
+            b_out: HdlNone(),
         },
     ];
     for (
@@ -449,6 +488,7 @@ fn test_enums() {
             data_in,
             which_out: _,
             data_out: _,
+            b_out: _,
         },
     ) in io_cycles.into_iter().enumerate()
     {
@@ -469,11 +509,12 @@ fn test_enums() {
                 .to_bigint()
                 .try_into()
                 .expect("known to be in range"),
+            b_out: sim.read(sim.io().b_out).to_expr(),
         };
         assert_eq!(
             expected,
             io,
-            "cycle: {cycle}\nvcd:\n{}",
+            "vcd:\n{}\ncycle: {cycle}",
             String::from_utf8(writer.take()).unwrap(),
         );
         sim.write_clock(sim.io().cd.clk, false);
@@ -509,7 +550,6 @@ pub fn memories() {
     connect_any(mem.new_write_port(), w);
 }
 
-#[cfg(todo)] // TODO: finish
 #[hdl]
 #[test]
 fn test_memories() {
@@ -529,15 +569,107 @@ fn test_memories() {
         w_data: (u8, i8),
         w_mask: (bool, bool),
     }
-    let io_cycles = [IO {
-        r_addr: 0,
-        r_en: false,
-        r_data: (0, 0),
-        w_addr: 0,
-        w_en: false,
-        w_data: (0, 0),
-        w_mask: (false, false),
-    }];
+    let io_cycles = [
+        IO {
+            r_addr: 0,
+            r_en: false,
+            r_data: (0, 0),
+            w_addr: 0,
+            w_en: false,
+            w_data: (0, 0),
+            w_mask: (false, false),
+        },
+        IO {
+            r_addr: 0,
+            r_en: true,
+            r_data: (0x1, 0x23),
+            w_addr: 0,
+            w_en: true,
+            w_data: (0x10, 0x20),
+            w_mask: (true, true),
+        },
+        IO {
+            r_addr: 0,
+            r_en: true,
+            r_data: (0x10, 0x20),
+            w_addr: 0,
+            w_en: true,
+            w_data: (0x30, 0x40),
+            w_mask: (false, true),
+        },
+        IO {
+            r_addr: 0,
+            r_en: true,
+            r_data: (0x10, 0x40),
+            w_addr: 0,
+            w_en: true,
+            w_data: (0x50, 0x60),
+            w_mask: (true, false),
+        },
+        IO {
+            r_addr: 0,
+            r_en: true,
+            r_data: (0x50, 0x40),
+            w_addr: 0,
+            w_en: true,
+            w_data: (0x70, -0x80),
+            w_mask: (false, false),
+        },
+        IO {
+            r_addr: 0,
+            r_en: true,
+            r_data: (0x50, 0x40),
+            w_addr: 0,
+            w_en: false,
+            w_data: (0x90, 0xA0u8 as i8),
+            w_mask: (false, false),
+        },
+        IO {
+            r_addr: 0,
+            r_en: true,
+            r_data: (0x50, 0x40),
+            w_addr: 1,
+            w_en: true,
+            w_data: (0x90, 0xA0u8 as i8),
+            w_mask: (true, true),
+        },
+        IO {
+            r_addr: 0,
+            r_en: true,
+            r_data: (0x50, 0x40),
+            w_addr: 2,
+            w_en: true,
+            w_data: (0xB0, 0xC0u8 as i8),
+            w_mask: (true, true),
+        },
+        IO {
+            r_addr: 0,
+            r_en: true,
+            r_data: (0x50, 0x40),
+            w_addr: 2,
+            w_en: false,
+            w_data: (0xD0, 0xE0u8 as i8),
+            w_mask: (true, true),
+        },
+        IO {
+            r_addr: 1,
+            r_en: true,
+            r_data: (0x90, 0xA0u8 as i8),
+            w_addr: 2,
+            w_en: false,
+            w_data: (0xD0, 0xE0u8 as i8),
+            w_mask: (true, true),
+        },
+        IO {
+            r_addr: 2,
+            r_en: true,
+            r_data: (0xB0, 0xC0u8 as i8),
+            w_addr: 2,
+            w_en: false,
+            w_data: (0xD0, 0xE0u8 as i8),
+            w_mask: (true, true),
+        },
+    ];
     for (
         cycle,
         expected @ IO {
@@ -580,7 +712,7 @@ fn test_memories() {
         assert_eq!(
             expected,
             io,
-            "cycle: {cycle}\nvcd:\n{}",
+            "vcd:\n{}\ncycle: {cycle}",
             String::from_utf8(writer.take()).unwrap(),
         );
         sim.advance_time(SimDuration::from_micros(1));
@@ -603,4 +735,514 @@ fn test_memories() {
     }
 }
 
-// TODO: add more tests for memories
+#[hdl_module(outline_generated)]
+pub fn memories2() {
+    #[hdl]
+    let rw: fayalite::memory::ReadWriteStruct<UInt<2>, ConstUsize<3>> = m.input();
+    #[hdl]
+    let mut mem = memory_with_init([HdlSome(true); 5]);
+    mem.read_latency(1);
+    mem.write_latency(NonZeroUsize::new(1).unwrap());
+    mem.read_under_write(ReadUnderWrite::New);
+    let rw_port = mem.new_rw_port();
+    connect_any(rw_port.addr, rw.addr);
+    connect(rw_port.en, rw.en);
+    connect(rw_port.clk, rw.clk);
+    connect_any(rw.rdata, rw_port.rdata.cast_to_bits());
+    connect(rw_port.wmode, rw.wmode);
+    connect(rw_port.wdata, HdlNone());
+    #[hdl]
+    if rw.wdata[0] {
+        connect(rw_port.wdata, HdlSome(rw.wdata[1]));
+    }
+    connect(rw_port.wmask, rw.wmask);
+}
+
+#[hdl]
+#[test]
+fn test_memories2() {
+    let _n = SourceLocation::normalize_files_for_tests();
+    let mut sim = Simulation::new(memories2());
+    let mut writer = RcWriter::default();
+    sim.add_trace_writer(VcdWriterDecls::new(writer.clone()));
+    sim.write_clock(sim.io().rw.clk, false);
+    #[derive(Debug, PartialEq, Eq)]
+    struct IO {
+        addr: u8,
+        en: bool,
+        rdata: u8,
+        wmode: bool,
+        wdata: u8,
+        wmask: bool,
+    }
+    let io_cycles = [
+        IO {
+            addr: 0,
+            en: false,
+            rdata: 0,
+            wmode: false,
+            wdata: 0,
+            wmask: false,
+        },
+        IO {
+            addr: 0,
+            en: true,
+            rdata: 0x3,
+            wmode: false,
+            wdata: 0,
+            wmask: false,
+        },
+        IO {
+            addr: 0,
+            en: false,
+            rdata: 0,
+            wmode: false,
+            wdata: 0,
+            wmask: false,
+        },
+        IO {
+            addr: 0,
+            en: true,
+            rdata: 0,
+            wmode: true,
+            wdata: 0,
+            wmask: true,
+        },
+        IO {
+            addr: 0,
+            en: true,
+            rdata: 0,
+            wmode: false,
+            wdata: 0,
+            wmask: false,
+        },
+        IO {
+            addr: 0,
+            en: true,
+            rdata: 0,
+            wmode: true,
+            wdata: 3,
+            wmask: false,
+        },
+        IO {
+            addr: 1,
+            en: true,
+            rdata: 0,
+            wmode: true,
+            wdata: 1,
+            wmask: true,
+        },
+        IO {
+            addr: 2,
+            en: true,
+            rdata: 0,
+            wmode: true,
+            wdata: 2,
+            wmask: true,
+        },
+        IO {
+            addr: 3,
+            en: true,
+            rdata: 0,
+            wmode: true,
+            wdata: 3,
+            wmask: true,
+        },
+        IO {
+            addr: 4,
+            en: true,
+            rdata: 0,
+            wmode: true,
+            wdata: 2,
+            wmask: true,
+        },
+        IO {
+            addr: 5,
+            en: true,
+            rdata: 0,
+            wmode: true,
+            wdata: 1,
+            wmask: true,
+        },
+        IO {
+            addr: 6,
+            en: true,
+            rdata: 0,
+            wmode: true,
+            wdata: 1,
+            wmask: true,
+        },
+        IO {
+            addr: 7,
+            en: true,
+            rdata: 0,
+            wmode: true,
+            wdata: 1,
+            wmask: true,
+        },
+        IO {
+            addr: 7,
+            en: true,
+            rdata: 0,
+            wmode: false,
+            wdata: 0,
+            wmask: false,
+        },
+        IO {
+            addr: 6,
+            en: true,
+            rdata: 0,
+            wmode: false,
+            wdata: 0,
+            wmask: false,
+        },
+        IO {
+            addr: 5,
+            en: true,
+            rdata: 0,
+            wmode: false,
+            wdata: 0,
+            wmask: false,
+        },
+        IO {
+            addr: 4,
+            en: true,
+            rdata: 0,
+            wmode: false,
+            wdata: 0,
+            wmask: false,
+        },
+        IO {
+            addr: 3,
+            en: true,
+            rdata: 3,
+            wmode: false,
+            wdata: 0,
+            wmask: false,
+        },
+        IO {
+            addr: 2,
+            en: true,
+            rdata: 0,
+            wmode: false,
+            wdata: 0,
+            wmask: false,
+        },
+        IO {
+            addr: 0,
+            en: true,
+            rdata: 0,
+            wmode: false,
+            wdata: 0,
+            wmask: false,
+        },
+        IO {
+            addr: 1,
+            en: true,
+            rdata: 1,
+            wmode: false,
+            wdata: 0,
+            wmask: false,
+        },
+        IO {
+            addr: 0,
+            en: false,
+            rdata: 0,
+            wmode: false,
+            wdata: 0,
+            wmask: false,
+        },
+    ];
+    for (
+        cycle,
+        expected @ IO {
+            addr,
+            en,
+            rdata: _,
+            wmode,
+            wdata,
+            wmask,
+        },
+    ) in io_cycles.into_iter().enumerate()
+    {
+        sim.write_bool_or_int(sim.io().rw.addr, addr.cast_to_static());
+        sim.write_bool(sim.io().rw.en, en);
+        sim.write_bool(sim.io().rw.wmode, wmode);
+        sim.write_bool_or_int(sim.io().rw.wdata, wdata.cast_to_static());
+        sim.write_bool(sim.io().rw.wmask, wmask);
+        sim.advance_time(SimDuration::from_nanos(250));
+        sim.write_clock(sim.io().rw.clk, true);
+        sim.advance_time(SimDuration::from_nanos(250));
+        let io = IO {
+            addr,
+            en,
+            rdata: sim
+                .read_bool_or_int(sim.io().rw.rdata)
+                .to_bigint()
+                .try_into()
+                .expect("known to be in range"),
+            wmode,
+            wdata,
+            wmask,
+        };
+        assert_eq!(
+            expected,
+            io,
+            "vcd:\n{}\ncycle: {cycle}",
+            String::from_utf8(writer.take()).unwrap(),
+        );
+        sim.advance_time(SimDuration::from_nanos(250));
+        sim.write_clock(sim.io().rw.clk, false);
+        sim.advance_time(SimDuration::from_nanos(250));
+    }
+    sim.flush_traces().unwrap();
+    let vcd = String::from_utf8(writer.take()).unwrap();
+    println!("####### VCD:\n{vcd}\n#######");
+    if vcd != include_str!("sim/expected/memories2.vcd") {
+        panic!();
+    }
+    let sim_debug = format!("{sim:#?}");
+    println!("#######\n{sim_debug}\n#######");
+    if sim_debug != include_str!("sim/expected/memories2.txt") {
+        panic!();
+    }
+}
+
+#[hdl_module(outline_generated)]
+pub fn memories3() {
+    #[hdl]
+    let r: fayalite::memory::ReadStruct<Array<UInt<8>, 8>, ConstUsize<3>> = m.input();
+    #[hdl]
+    let w: fayalite::memory::WriteStruct<Array<UInt<8>, 8>, ConstUsize<3>> = m.input();
+    #[hdl]
+    let mut mem: MemBuilder<Array<UInt<8>, 8>> = memory();
+    mem.depth(8);
+    mem.read_latency(2);
+    mem.write_latency(NonZeroUsize::new(2).unwrap());
+    mem.read_under_write(ReadUnderWrite::Old);
+    connect_any(mem.new_read_port(), r);
+    connect_any(mem.new_write_port(), w);
+}
+
+#[hdl]
+#[test]
+fn test_memories3() {
+    let _n = SourceLocation::normalize_files_for_tests();
+    let mut sim = Simulation::new(memories3());
+    let mut writer = RcWriter::default();
+    sim.add_trace_writer(VcdWriterDecls::new(writer.clone()));
+    sim.write_clock(sim.io().r.clk, false);
+    sim.write_clock(sim.io().w.clk, false);
+    #[derive(Debug, PartialEq, Eq, Clone, Copy)]
+    struct IO {
+        r_addr: u8,
+        r_en: bool,
+        r_data: [u8; 8],
+        w_addr: u8,
+        w_en: bool,
+        w_data: [u8; 8],
+        w_mask: [bool; 8],
+    }
+    let io_cycles = [
+        IO {
+            r_addr: 0,
+            r_en: false,
+            r_data: [0; 8],
+            w_addr: 0,
+            w_en: true,
+            w_data: [0x12, 0x34, 0x56, 0x78, 0x9A, 0xBC, 0xDE, 0xF0],
+            w_mask: [false, true, false, true, true, false, false, true],
+        },
+        IO {
+            r_addr: 0,
+            r_en: true,
+            r_data: [0; 8],
+            w_addr: 1,
+            w_en: false,
+            w_data: [0; 8],
+            w_mask: [false; 8],
+        },
+        IO {
+            r_addr: 0,
+            r_en: true,
+            r_data: [0, 0x34, 0, 0x78, 0x9A, 0, 0, 0xF0],
+            w_addr: 1,
+            w_en: false,
+            w_data: [0; 8],
+            w_mask: [false; 8],
+        },
+        IO {
+            r_addr: 0,
+            r_en: true,
+            r_data: [0, 0x34, 0, 0x78, 0x9A, 0, 0, 0xF0],
+            w_addr: 0,
+            w_en: true,
+            w_data: [0xFE, 0xDC, 0xBA, 0x98, 0x76, 0x54, 0x32, 0x10],
+            w_mask: [true; 8],
+        },
+        IO {
+            r_addr: 0,
+            r_en: true,
+            r_data: [0, 0x34, 0, 0x78, 0x9A, 0, 0, 0xF0],
+            w_addr: 0,
+            w_en: true,
+            w_data: [0xFE, 0xDC, 0xBA, 0x98, 0x76, 0x54, 0x32, 0x10],
+            w_mask: [true; 8],
+        },
+        IO {
+            r_addr: 0,
+            r_en: true,
+            r_data: [0xFE, 0xDC, 0xBA, 0x98, 0x76, 0x54, 0x32, 0x10],
+            w_addr: 0,
+            w_en: true,
+            w_data: [0xFE, 0xDC, 0xBA, 0x98, 0x76, 0x54, 0x32, 0x10],
+            w_mask: [true; 8],
+        },
+        IO {
+            r_addr: 0,
+            r_en: false,
+            r_data: [0; 8],
+            w_addr: 1,
+            w_en: true,
+            w_data: [0x13, 0x57, 0x9B, 0xDF, 0x02, 0x46, 0x8A, 0xCE],
+            w_mask: [true; 8],
+        },
+        IO {
+            r_addr: 0,
+            r_en: false,
+            r_data: [0; 8],
+            w_addr: 2,
+            w_en: true,
+            w_data: *b"testing!",
+            w_mask: [true; 8],
+        },
+        IO {
+            r_addr: 0,
+            r_en: false,
+            r_data: [0; 8],
+            w_addr: 3,
+            w_en: true,
+            w_data: *b"more tst",
+            w_mask: [true; 8],
+        },
+        IO {
+            r_addr: 0,
+            r_en: true,
+            r_data: [0xFE, 0xDC, 0xBA, 0x98, 0x76, 0x54, 0x32, 0x10],
+            w_addr: 0,
+            w_en: false,
+            w_data: [0; 8],
+            w_mask: [false; 8],
+        },
+        IO {
+            r_addr: 1,
+            r_en: true,
+            r_data: [0x13, 0x57, 0x9B, 0xDF, 0x02, 0x46, 0x8A, 0xCE],
+            w_addr: 0,
+            w_en: false,
+            w_data: [0; 8],
+            w_mask: [false; 8],
+        },
+        IO {
+            r_addr: 2,
+            r_en: true,
+            r_data: *b"testing!",
+            w_addr: 0,
+            w_en: false,
+            w_data: [0; 8],
+            w_mask: [false; 8],
+        },
+        IO {
+            r_addr: 3,
+            r_en: true,
+            r_data: *b"more tst",
+            w_addr: 0,
+            w_en: false,
+            w_data: [0; 8],
+            w_mask: [false; 8],
+        },
+    ];
+    for cycle in 0..io_cycles.len() + 2 {
+        {
+            let IO {
+                r_addr,
+                r_en,
+                r_data: _,
+                w_addr,
+                w_en,
+                w_data,
+                w_mask,
+            } = io_cycles.get(cycle).copied().unwrap_or(IO {
+                r_addr: 0,
+                r_en: false,
+                r_data: [0; 8],
+                w_addr: 0,
+                w_en: false,
+                w_data: [0; 8],
+                w_mask: [false; 8],
+            });
+            sim.write_bool_or_int(sim.io().r.addr, r_addr.cast_to_static());
+            sim.write_bool(sim.io().r.en, r_en);
+            sim.write_bool_or_int(sim.io().w.addr, w_addr.cast_to_static());
+            sim.write_bool(sim.io().w.en, w_en);
+            for (i, v) in w_data.into_iter().enumerate() {
+                sim.write_bool_or_int(sim.io().w.data[i], v);
+            }
+            for (i, v) in w_mask.into_iter().enumerate() {
+                sim.write_bool_or_int(sim.io().w.mask[i], v);
+            }
+        }
+        sim.advance_time(SimDuration::from_nanos(250));
+        sim.write_clock(sim.io().r.clk, true);
+        sim.write_clock(sim.io().w.clk, true);
+        sim.advance_time(SimDuration::from_nanos(250));
+        if let Some(
+            expected @ IO {
+                r_addr,
+                r_en,
+                r_data: _,
+                w_addr,
+                w_en,
+                w_data,
+                w_mask,
+            },
+        ) = cycle.checked_sub(1).and_then(|i| io_cycles.get(i).copied())
+        {
+            let io = IO {
+                r_addr,
+                r_en,
+                r_data: std::array::from_fn(|i| {
+                    sim.read_bool_or_int(sim.io().r.data[i])
+                        .to_bigint()
+                        .try_into()
+                        .expect("known to be in range")
+                }),
+                w_addr,
+                w_en,
+                w_data,
+                w_mask,
+            };
+            assert_eq!(
+                expected,
+                io,
+                "vcd:\n{}\ncycle: {cycle}",
+                String::from_utf8(writer.take()).unwrap(),
+            );
+        }
+        sim.advance_time(SimDuration::from_nanos(250));
+        sim.write_clock(sim.io().r.clk, false);
+        sim.write_clock(sim.io().w.clk, false);
+        sim.advance_time(SimDuration::from_nanos(250));
+    }
+    sim.flush_traces().unwrap();
+    let vcd = String::from_utf8(writer.take()).unwrap();
+    println!("####### VCD:\n{vcd}\n#######");
+    if vcd != include_str!("sim/expected/memories3.vcd") {
+        panic!();
+    }
+    let sim_debug = format!("{sim:#?}");
+    println!("#######\n{sim_debug}\n#######");
+    if sim_debug != include_str!("sim/expected/memories3.txt") {
+        panic!();
+    }
+}

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

@@ -3,12 +3,12 @@ Simulation {
         insns: Insns {
             state_layout: StateLayout {
                 ty: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 2,
                         debug_data: [
                             SlotDebugData {
@@ -23,7 +23,7 @@ Simulation {
                         ..
                     },
                 },
-                memories: StatePartAllocationLayout<Memories> {
+                memories: StatePartLayout<Memories> {
                     len: 0,
                     debug_data: [],
                     layout_data: [],
@@ -32,17 +32,17 @@ Simulation {
             },
             insns: [
                 // at: module-XXXXXXXXXX.rs:1:1
-                Const {
-                    dest: StatePartIndex<BigSlots>(1), // SlotDebugData { name: "", ty: UInt<8> },
-                    value: 5,
+                0: Const {
+                    dest: StatePartIndex<BigSlots>(1), // (0x5) SlotDebugData { name: "", ty: UInt<8> },
+                    value: 0x5,
                 },
                 // at: module-XXXXXXXXXX.rs:3:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(0), // SlotDebugData { name: "InstantiatedModule(connect_const: connect_const).connect_const::o", ty: UInt<8> },
-                    src: StatePartIndex<BigSlots>(1), // SlotDebugData { name: "", ty: UInt<8> },
+                1: Copy {
+                    dest: StatePartIndex<BigSlots>(0), // (0x5) SlotDebugData { name: "InstantiatedModule(connect_const: connect_const).connect_const::o", ty: UInt<8> },
+                    src: StatePartIndex<BigSlots>(1), // (0x5) SlotDebugData { name: "", ty: UInt<8> },
                 },
                 // at: module-XXXXXXXXXX.rs:1:1
-                Return,
+                2: Return,
             ],
             ..
         },
@@ -80,12 +80,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: UInt<8>,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -138,4 +138,5 @@ Simulation {
     trace_writers: [],
     instant: 0 s,
     clocks_triggered: [],
+    ..
 }

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

@@ -3,12 +3,12 @@ Simulation {
         insns: Insns {
             state_layout: StateLayout {
                 ty: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 5,
                         debug_data: [
                             SlotDebugData {
@@ -35,7 +35,7 @@ Simulation {
                         ..
                     },
                 },
-                memories: StatePartAllocationLayout<Memories> {
+                memories: StatePartLayout<Memories> {
                     len: 0,
                     debug_data: [],
                     layout_data: [],
@@ -44,31 +44,31 @@ Simulation {
             },
             insns: [
                 // at: module-XXXXXXXXXX.rs:1:1
-                Const {
-                    dest: StatePartIndex<BigSlots>(2), // SlotDebugData { name: "", ty: Bool },
-                    value: 1,
+                0: Const {
+                    dest: StatePartIndex<BigSlots>(2), // (0x1) SlotDebugData { name: "", ty: Bool },
+                    value: 0x1,
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(3), // SlotDebugData { name: "", ty: AsyncReset },
-                    src: StatePartIndex<BigSlots>(2), // SlotDebugData { name: "", ty: Bool },
+                1: Copy {
+                    dest: StatePartIndex<BigSlots>(3), // (0x1) SlotDebugData { name: "", ty: AsyncReset },
+                    src: StatePartIndex<BigSlots>(2), // (0x1) SlotDebugData { name: "", ty: Bool },
                 },
                 // at: module-XXXXXXXXXX.rs:4:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(0), // SlotDebugData { name: "InstantiatedModule(connect_const_reset: connect_const_reset).connect_const_reset::reset_out", ty: AsyncReset },
-                    src: StatePartIndex<BigSlots>(3), // SlotDebugData { name: "", ty: AsyncReset },
+                2: Copy {
+                    dest: StatePartIndex<BigSlots>(0), // (0x1) SlotDebugData { name: "InstantiatedModule(connect_const_reset: connect_const_reset).connect_const_reset::reset_out", ty: AsyncReset },
+                    src: StatePartIndex<BigSlots>(3), // (0x1) SlotDebugData { name: "", ty: AsyncReset },
                 },
                 // at: module-XXXXXXXXXX.rs:1:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(4), // SlotDebugData { name: "", ty: Bool },
-                    src: StatePartIndex<BigSlots>(0), // SlotDebugData { name: "InstantiatedModule(connect_const_reset: connect_const_reset).connect_const_reset::reset_out", ty: AsyncReset },
+                3: Copy {
+                    dest: StatePartIndex<BigSlots>(4), // (0x1) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(0), // (0x1) SlotDebugData { name: "InstantiatedModule(connect_const_reset: connect_const_reset).connect_const_reset::reset_out", ty: AsyncReset },
                 },
                 // at: module-XXXXXXXXXX.rs:5:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(1), // SlotDebugData { name: "InstantiatedModule(connect_const_reset: connect_const_reset).connect_const_reset::bit_out", ty: Bool },
-                    src: StatePartIndex<BigSlots>(4), // SlotDebugData { name: "", ty: Bool },
+                4: Copy {
+                    dest: StatePartIndex<BigSlots>(1), // (0x1) SlotDebugData { name: "InstantiatedModule(connect_const_reset: connect_const_reset).connect_const_reset::bit_out", ty: Bool },
+                    src: StatePartIndex<BigSlots>(4), // (0x1) SlotDebugData { name: "", ty: Bool },
                 },
                 // at: module-XXXXXXXXXX.rs:1:1
-                Return,
+                5: Return,
             ],
             ..
         },
@@ -109,12 +109,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: Bool,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -143,12 +143,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: AsyncReset,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -225,4 +225,5 @@ Simulation {
     ],
     instant: 1 μs,
     clocks_triggered: [],
+    ..
 }

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

@@ -3,7 +3,7 @@ Simulation {
         insns: Insns {
             state_layout: StateLayout {
                 ty: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 4,
                         debug_data: [
                             SlotDebugData {
@@ -25,7 +25,7 @@ Simulation {
                         ],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 10,
                         debug_data: [
                             SlotDebugData {
@@ -72,7 +72,7 @@ Simulation {
                         ..
                     },
                 },
-                memories: StatePartAllocationLayout<Memories> {
+                memories: StatePartLayout<Memories> {
                     len: 0,
                     debug_data: [],
                     layout_data: [],
@@ -81,89 +81,90 @@ Simulation {
             },
             insns: [
                 // at: module-XXXXXXXXXX.rs:1:1
-                Const {
-                    dest: StatePartIndex<BigSlots>(7), // SlotDebugData { name: "", ty: UInt<1> },
-                    value: 1,
+                0: Const {
+                    dest: StatePartIndex<BigSlots>(7), // (0x1) SlotDebugData { name: "", ty: UInt<1> },
+                    value: 0x1,
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(6), // SlotDebugData { name: "", ty: Bool },
-                    src: StatePartIndex<BigSlots>(1), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::cd.rst", ty: AsyncReset },
+                1: Copy {
+                    dest: StatePartIndex<BigSlots>(6), // (0x0) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(1), // (0x0) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::cd.rst", ty: AsyncReset },
                 },
                 // at: module-XXXXXXXXXX.rs:3:1
-                IsNonZeroDestIsSmall {
-                    dest: StatePartIndex<SmallSlots>(3), // SlotDebugData { name: "", ty: Bool },
-                    src: StatePartIndex<BigSlots>(1), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::cd.rst", ty: AsyncReset },
+                2: IsNonZeroDestIsSmall {
+                    dest: StatePartIndex<SmallSlots>(3), // (0x0 0) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(1), // (0x0) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::cd.rst", ty: AsyncReset },
                 },
                 // at: module-XXXXXXXXXX.rs:1:1
-                Const {
-                    dest: StatePartIndex<BigSlots>(5), // SlotDebugData { name: "", ty: UInt<4> },
-                    value: 3,
+                3: Const {
+                    dest: StatePartIndex<BigSlots>(5), // (0x3) SlotDebugData { name: "", ty: UInt<4> },
+                    value: 0x3,
                 },
                 // at: module-XXXXXXXXXX.rs:3:1
-                BranchIfZero {
+                4: BranchIfZero {
                     target: 6,
-                    value: StatePartIndex<BigSlots>(6), // SlotDebugData { name: "", ty: Bool },
+                    value: StatePartIndex<BigSlots>(6), // (0x0) SlotDebugData { name: "", ty: Bool },
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(3), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(5), // SlotDebugData { name: "", ty: UInt<4> },
+                5: Copy {
+                    dest: StatePartIndex<BigSlots>(3), // (0x3) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(5), // (0x3) SlotDebugData { name: "", ty: UInt<4> },
                 },
                 // at: module-XXXXXXXXXX.rs:1:1
-                Add {
-                    dest: StatePartIndex<BigSlots>(8), // SlotDebugData { name: "", ty: UInt<5> },
-                    lhs: StatePartIndex<BigSlots>(3), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
-                    rhs: StatePartIndex<BigSlots>(7), // SlotDebugData { name: "", ty: UInt<1> },
+                6: Add {
+                    dest: StatePartIndex<BigSlots>(8), // (0x4) SlotDebugData { name: "", ty: UInt<5> },
+                    lhs: StatePartIndex<BigSlots>(3), // (0x3) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
+                    rhs: StatePartIndex<BigSlots>(7), // (0x1) SlotDebugData { name: "", ty: UInt<1> },
                 },
-                CastToUInt {
-                    dest: StatePartIndex<BigSlots>(9), // SlotDebugData { name: "", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(8), // SlotDebugData { name: "", ty: UInt<5> },
+                7: CastToUInt {
+                    dest: StatePartIndex<BigSlots>(9), // (0x4) SlotDebugData { name: "", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(8), // (0x4) SlotDebugData { name: "", ty: UInt<5> },
                     dest_width: 4,
                 },
                 // at: module-XXXXXXXXXX.rs:4:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(4), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg$next", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(9), // SlotDebugData { name: "", ty: UInt<4> },
+                8: Copy {
+                    dest: StatePartIndex<BigSlots>(4), // (0x4) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg$next", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(9), // (0x4) SlotDebugData { name: "", ty: UInt<4> },
                 },
                 // at: module-XXXXXXXXXX.rs:6:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(2), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(3), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
+                9: Copy {
+                    dest: StatePartIndex<BigSlots>(2), // (0x3) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(3), // (0x3) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
                 },
                 // at: module-XXXXXXXXXX.rs:3:1
-                IsNonZeroDestIsSmall {
-                    dest: StatePartIndex<SmallSlots>(2), // SlotDebugData { name: "", ty: Bool },
-                    src: StatePartIndex<BigSlots>(0), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::cd.clk", ty: Clock },
+                10: IsNonZeroDestIsSmall {
+                    dest: StatePartIndex<SmallSlots>(2), // (0x1 1) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(0), // (0x1) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::cd.clk", ty: Clock },
                 },
-                AndSmall {
-                    dest: StatePartIndex<SmallSlots>(1), // SlotDebugData { name: "", ty: Bool },
-                    lhs: StatePartIndex<SmallSlots>(2), // SlotDebugData { name: "", ty: Bool },
-                    rhs: StatePartIndex<SmallSlots>(0), // SlotDebugData { name: "", ty: Bool },
+                11: 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 },
                 },
-                BranchIfSmallNonZero {
+                12: BranchIfSmallNonZero {
                     target: 16,
-                    value: StatePartIndex<SmallSlots>(3), // SlotDebugData { name: "", ty: Bool },
+                    value: StatePartIndex<SmallSlots>(3), // (0x0 0) SlotDebugData { name: "", ty: Bool },
                 },
-                BranchIfSmallZero {
+                13: BranchIfSmallZero {
                     target: 17,
-                    value: StatePartIndex<SmallSlots>(1), // SlotDebugData { name: "", ty: Bool },
+                    value: StatePartIndex<SmallSlots>(1), // (0x0 0) SlotDebugData { name: "", ty: Bool },
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(3), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(4), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg$next", ty: UInt<4> },
+                14: Copy {
+                    dest: StatePartIndex<BigSlots>(3), // (0x3) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(4), // (0x4) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg$next", ty: UInt<4> },
                 },
-                Branch {
+                15: Branch {
                     target: 17,
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(3), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(5), // SlotDebugData { name: "", ty: UInt<4> },
+                16: Copy {
+                    dest: StatePartIndex<BigSlots>(3), // (0x3) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(5), // (0x3) SlotDebugData { name: "", ty: UInt<4> },
                 },
-                NotSmall {
-                    dest: StatePartIndex<SmallSlots>(0), // SlotDebugData { name: "", ty: Bool },
-                    src: StatePartIndex<SmallSlots>(2), // SlotDebugData { name: "", ty: Bool },
+                17: 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
-                Return,
+                18: Return,
             ],
             ..
         },
@@ -174,7 +175,7 @@ Simulation {
         },
         small_slots: StatePart {
             value: [
-                18446744073709551614,
+                0,
                 0,
                 1,
                 0,
@@ -219,12 +220,12 @@ Simulation {
                     rst: AsyncReset,
                 },
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 2,
                         debug_data: [
                             SlotDebugData {
@@ -249,12 +250,12 @@ Simulation {
                             ty: CompiledTypeLayout {
                                 ty: Clock,
                                 layout: TypeLayout {
-                                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                                    small_slots: StatePartLayout<SmallSlots> {
                                         len: 0,
                                         debug_data: [],
                                         ..
                                     },
-                                    big_slots: StatePartAllocationLayout<BigSlots> {
+                                    big_slots: StatePartLayout<BigSlots> {
                                         len: 1,
                                         debug_data: [
                                             SlotDebugData {
@@ -276,12 +277,12 @@ Simulation {
                             ty: CompiledTypeLayout {
                                 ty: AsyncReset,
                                 layout: TypeLayout {
-                                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                                    small_slots: StatePartLayout<SmallSlots> {
                                         len: 0,
                                         debug_data: [],
                                         ..
                                     },
-                                    big_slots: StatePartAllocationLayout<BigSlots> {
+                                    big_slots: StatePartLayout<BigSlots> {
                                         len: 1,
                                         debug_data: [
                                             SlotDebugData {
@@ -314,12 +315,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: Clock,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -348,12 +349,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: AsyncReset,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -382,12 +383,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: UInt<4>,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -517,4 +518,5 @@ Simulation {
     clocks_triggered: [
         StatePartIndex<SmallSlots>(1),
     ],
+    ..
 }

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

@@ -3,7 +3,7 @@ Simulation {
         insns: Insns {
             state_layout: StateLayout {
                 ty: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 4,
                         debug_data: [
                             SlotDebugData {
@@ -25,7 +25,7 @@ Simulation {
                         ],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 9,
                         debug_data: [
                             SlotDebugData {
@@ -68,7 +68,7 @@ Simulation {
                         ..
                     },
                 },
-                memories: StatePartAllocationLayout<Memories> {
+                memories: StatePartLayout<Memories> {
                     len: 0,
                     debug_data: [],
                     layout_data: [],
@@ -77,75 +77,76 @@ Simulation {
             },
             insns: [
                 // at: module-XXXXXXXXXX.rs:6:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(2), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(3), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
+                0: Copy {
+                    dest: StatePartIndex<BigSlots>(2), // (0x3) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(3), // (0x3) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
                 },
                 // at: module-XXXXXXXXXX.rs:1:1
-                Const {
-                    dest: StatePartIndex<BigSlots>(6), // SlotDebugData { name: "", ty: UInt<1> },
-                    value: 1,
+                1: Const {
+                    dest: StatePartIndex<BigSlots>(6), // (0x1) SlotDebugData { name: "", ty: UInt<1> },
+                    value: 0x1,
                 },
-                Add {
-                    dest: StatePartIndex<BigSlots>(7), // SlotDebugData { name: "", ty: UInt<5> },
-                    lhs: StatePartIndex<BigSlots>(3), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
-                    rhs: StatePartIndex<BigSlots>(6), // SlotDebugData { name: "", ty: UInt<1> },
+                2: Add {
+                    dest: StatePartIndex<BigSlots>(7), // (0x4) SlotDebugData { name: "", ty: UInt<5> },
+                    lhs: StatePartIndex<BigSlots>(3), // (0x3) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
+                    rhs: StatePartIndex<BigSlots>(6), // (0x1) SlotDebugData { name: "", ty: UInt<1> },
                 },
-                CastToUInt {
-                    dest: StatePartIndex<BigSlots>(8), // SlotDebugData { name: "", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(7), // SlotDebugData { name: "", ty: UInt<5> },
+                3: CastToUInt {
+                    dest: StatePartIndex<BigSlots>(8), // (0x4) SlotDebugData { name: "", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(7), // (0x4) SlotDebugData { name: "", ty: UInt<5> },
                     dest_width: 4,
                 },
                 // at: module-XXXXXXXXXX.rs:4:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(4), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg$next", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(8), // SlotDebugData { name: "", ty: UInt<4> },
+                4: Copy {
+                    dest: StatePartIndex<BigSlots>(4), // (0x4) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg$next", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(8), // (0x4) SlotDebugData { name: "", ty: UInt<4> },
                 },
                 // at: module-XXXXXXXXXX.rs:3:1
-                IsNonZeroDestIsSmall {
-                    dest: StatePartIndex<SmallSlots>(3), // SlotDebugData { name: "", ty: Bool },
-                    src: StatePartIndex<BigSlots>(1), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::cd.rst", ty: SyncReset },
+                5: IsNonZeroDestIsSmall {
+                    dest: StatePartIndex<SmallSlots>(3), // (0x0 0) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(1), // (0x0) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::cd.rst", ty: SyncReset },
                 },
                 // at: module-XXXXXXXXXX.rs:1:1
-                Const {
-                    dest: StatePartIndex<BigSlots>(5), // SlotDebugData { name: "", ty: UInt<4> },
-                    value: 3,
+                6: Const {
+                    dest: StatePartIndex<BigSlots>(5), // (0x3) SlotDebugData { name: "", ty: UInt<4> },
+                    value: 0x3,
                 },
                 // at: module-XXXXXXXXXX.rs:3:1
-                IsNonZeroDestIsSmall {
-                    dest: StatePartIndex<SmallSlots>(2), // SlotDebugData { name: "", ty: Bool },
-                    src: StatePartIndex<BigSlots>(0), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::cd.clk", ty: Clock },
+                7: IsNonZeroDestIsSmall {
+                    dest: StatePartIndex<SmallSlots>(2), // (0x1 1) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(0), // (0x1) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::cd.clk", ty: Clock },
                 },
-                AndSmall {
-                    dest: StatePartIndex<SmallSlots>(1), // SlotDebugData { name: "", ty: Bool },
-                    lhs: StatePartIndex<SmallSlots>(2), // SlotDebugData { name: "", ty: Bool },
-                    rhs: StatePartIndex<SmallSlots>(0), // SlotDebugData { name: "", ty: Bool },
+                8: 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 },
                 },
-                BranchIfSmallZero {
+                9: BranchIfSmallZero {
                     target: 14,
-                    value: StatePartIndex<SmallSlots>(1), // SlotDebugData { name: "", ty: Bool },
+                    value: StatePartIndex<SmallSlots>(1), // (0x0 0) SlotDebugData { name: "", ty: Bool },
                 },
-                BranchIfSmallNonZero {
+                10: BranchIfSmallNonZero {
                     target: 13,
-                    value: StatePartIndex<SmallSlots>(3), // SlotDebugData { name: "", ty: Bool },
+                    value: StatePartIndex<SmallSlots>(3), // (0x0 0) SlotDebugData { name: "", ty: Bool },
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(3), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(4), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg$next", ty: UInt<4> },
+                11: Copy {
+                    dest: StatePartIndex<BigSlots>(3), // (0x3) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(4), // (0x4) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg$next", ty: UInt<4> },
                 },
-                Branch {
+                12: Branch {
                     target: 14,
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(3), // SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(5), // SlotDebugData { name: "", ty: UInt<4> },
+                13: Copy {
+                    dest: StatePartIndex<BigSlots>(3), // (0x3) SlotDebugData { name: "InstantiatedModule(counter: counter).counter::count_reg", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(5), // (0x3) SlotDebugData { name: "", ty: UInt<4> },
                 },
-                NotSmall {
-                    dest: StatePartIndex<SmallSlots>(0), // SlotDebugData { name: "", ty: Bool },
-                    src: StatePartIndex<SmallSlots>(2), // SlotDebugData { name: "", ty: Bool },
+                14: 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
-                Return,
+                15: Return,
             ],
             ..
         },
@@ -156,7 +157,7 @@ Simulation {
         },
         small_slots: StatePart {
             value: [
-                18446744073709551614,
+                0,
                 0,
                 1,
                 0,
@@ -200,12 +201,12 @@ Simulation {
                     rst: SyncReset,
                 },
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 2,
                         debug_data: [
                             SlotDebugData {
@@ -230,12 +231,12 @@ Simulation {
                             ty: CompiledTypeLayout {
                                 ty: Clock,
                                 layout: TypeLayout {
-                                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                                    small_slots: StatePartLayout<SmallSlots> {
                                         len: 0,
                                         debug_data: [],
                                         ..
                                     },
-                                    big_slots: StatePartAllocationLayout<BigSlots> {
+                                    big_slots: StatePartLayout<BigSlots> {
                                         len: 1,
                                         debug_data: [
                                             SlotDebugData {
@@ -257,12 +258,12 @@ Simulation {
                             ty: CompiledTypeLayout {
                                 ty: SyncReset,
                                 layout: TypeLayout {
-                                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                                    small_slots: StatePartLayout<SmallSlots> {
                                         len: 0,
                                         debug_data: [],
                                         ..
                                     },
-                                    big_slots: StatePartAllocationLayout<BigSlots> {
+                                    big_slots: StatePartLayout<BigSlots> {
                                         len: 1,
                                         debug_data: [
                                             SlotDebugData {
@@ -295,12 +296,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: Clock,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -329,12 +330,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: SyncReset,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -363,12 +364,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: UInt<4>,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -498,4 +499,5 @@ Simulation {
     clocks_triggered: [
         StatePartIndex<SmallSlots>(1),
     ],
+    ..
 }

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

@@ -9,18 +9,25 @@ $var wire 2 $ which_in $end
 $var wire 4 % data_in $end
 $var wire 2 & which_out $end
 $var wire 4 ' data_out $end
-$scope struct the_reg $end
+$scope struct b_out $end
 $var string 1 ( \$tag $end
+$scope struct HdlSome $end
+$var wire 1 ) \0 $end
+$var wire 1 * \1 $end
+$upscope $end
+$upscope $end
+$scope struct the_reg $end
+$var string 1 + \$tag $end
 $scope struct B $end
-$var reg 1 ) \0 $end
-$var reg 1 * \1 $end
+$var reg 1 , \0 $end
+$var reg 1 - \1 $end
 $upscope $end
 $scope struct C $end
 $scope struct a $end
-$var reg 1 + \[0] $end
-$var reg 1 , \[1] $end
+$var reg 1 . \[0] $end
+$var reg 1 / \[1] $end
 $upscope $end
-$var reg 2 - b $end
+$var reg 2 0 b $end
 $upscope $end
 $upscope $end
 $upscope $end
@@ -33,12 +40,15 @@ b0 $
 b0 %
 b0 &
 b0 '
-sA\x20(0) (
+sHdlNone\x20(0) (
 0)
 0*
-0+
+sA\x20(0) +
 0,
-b0 -
+0-
+0.
+0/
+b0 0
 $end
 #1000000
 1!
@@ -55,7 +65,8 @@ b1 $
 #5000000
 1!
 b1 &
-sB\x20(1) (
+sHdlSome\x20(1) (
+sB\x20(1) +
 #6000000
 0#
 b0 $
@@ -72,8 +83,10 @@ b1111 %
 b11 '
 1)
 1*
-1+
 1,
+1-
+1.
+1/
 #10000000
 0!
 #11000000
@@ -85,8 +98,11 @@ b10 $
 1!
 b10 &
 b1111 '
-sC\x20(2) (
-b11 -
+sHdlNone\x20(0) (
+0)
+0*
+sC\x20(2) +
+b11 0
 #14000000
 0!
 #15000000

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

@@ -0,0 +1,408 @@
+$timescale 1 ps $end
+$scope module memories $end
+$scope struct r $end
+$var wire 4 ! addr $end
+$var wire 1 " en $end
+$var wire 1 # clk $end
+$scope struct data $end
+$var wire 8 $ \0 $end
+$var wire 8 % \1 $end
+$upscope $end
+$upscope $end
+$scope struct w $end
+$var wire 4 & addr $end
+$var wire 1 ' en $end
+$var wire 1 ( clk $end
+$scope struct data $end
+$var wire 8 ) \0 $end
+$var wire 8 * \1 $end
+$upscope $end
+$scope struct mask $end
+$var wire 1 + \0 $end
+$var wire 1 , \1 $end
+$upscope $end
+$upscope $end
+$scope struct mem $end
+$scope struct contents $end
+$scope struct [0] $end
+$scope struct mem $end
+$var reg 8 9 \0 $end
+$var reg 8 I \1 $end
+$upscope $end
+$upscope $end
+$scope struct [1] $end
+$scope struct mem $end
+$var reg 8 : \0 $end
+$var reg 8 J \1 $end
+$upscope $end
+$upscope $end
+$scope struct [2] $end
+$scope struct mem $end
+$var reg 8 ; \0 $end
+$var reg 8 K \1 $end
+$upscope $end
+$upscope $end
+$scope struct [3] $end
+$scope struct mem $end
+$var reg 8 < \0 $end
+$var reg 8 L \1 $end
+$upscope $end
+$upscope $end
+$scope struct [4] $end
+$scope struct mem $end
+$var reg 8 = \0 $end
+$var reg 8 M \1 $end
+$upscope $end
+$upscope $end
+$scope struct [5] $end
+$scope struct mem $end
+$var reg 8 > \0 $end
+$var reg 8 N \1 $end
+$upscope $end
+$upscope $end
+$scope struct [6] $end
+$scope struct mem $end
+$var reg 8 ? \0 $end
+$var reg 8 O \1 $end
+$upscope $end
+$upscope $end
+$scope struct [7] $end
+$scope struct mem $end
+$var reg 8 @ \0 $end
+$var reg 8 P \1 $end
+$upscope $end
+$upscope $end
+$scope struct [8] $end
+$scope struct mem $end
+$var reg 8 A \0 $end
+$var reg 8 Q \1 $end
+$upscope $end
+$upscope $end
+$scope struct [9] $end
+$scope struct mem $end
+$var reg 8 B \0 $end
+$var reg 8 R \1 $end
+$upscope $end
+$upscope $end
+$scope struct [10] $end
+$scope struct mem $end
+$var reg 8 C \0 $end
+$var reg 8 S \1 $end
+$upscope $end
+$upscope $end
+$scope struct [11] $end
+$scope struct mem $end
+$var reg 8 D \0 $end
+$var reg 8 T \1 $end
+$upscope $end
+$upscope $end
+$scope struct [12] $end
+$scope struct mem $end
+$var reg 8 E \0 $end
+$var reg 8 U \1 $end
+$upscope $end
+$upscope $end
+$scope struct [13] $end
+$scope struct mem $end
+$var reg 8 F \0 $end
+$var reg 8 V \1 $end
+$upscope $end
+$upscope $end
+$scope struct [14] $end
+$scope struct mem $end
+$var reg 8 G \0 $end
+$var reg 8 W \1 $end
+$upscope $end
+$upscope $end
+$scope struct [15] $end
+$scope struct mem $end
+$var reg 8 H \0 $end
+$var reg 8 X \1 $end
+$upscope $end
+$upscope $end
+$upscope $end
+$scope struct r0 $end
+$var wire 4 - addr $end
+$var wire 1 . en $end
+$var wire 1 / clk $end
+$scope struct data $end
+$var wire 8 0 \0 $end
+$var wire 8 1 \1 $end
+$upscope $end
+$upscope $end
+$scope struct w1 $end
+$var wire 4 2 addr $end
+$var wire 1 3 en $end
+$var wire 1 4 clk $end
+$scope struct data $end
+$var wire 8 5 \0 $end
+$var wire 8 6 \1 $end
+$upscope $end
+$scope struct mask $end
+$var wire 1 7 \0 $end
+$var wire 1 8 \1 $end
+$upscope $end
+$upscope $end
+$upscope $end
+$upscope $end
+$enddefinitions $end
+$dumpvars
+b1 9
+b100011 I
+b1 :
+b100011 J
+b1 ;
+b100011 K
+b1 <
+b100011 L
+b1 =
+b100011 M
+b1 >
+b100011 N
+b1 ?
+b100011 O
+b1 @
+b100011 P
+b1 A
+b100011 Q
+b1 B
+b100011 R
+b1 C
+b100011 S
+b1 D
+b100011 T
+b1 E
+b100011 U
+b1 F
+b100011 V
+b1 G
+b100011 W
+b1 H
+b100011 X
+b0 !
+0"
+0#
+b0 $
+b0 %
+b0 &
+0'
+0(
+b0 )
+b0 *
+0+
+0,
+b0 -
+0.
+0/
+b0 0
+b0 1
+b0 2
+03
+04
+b0 5
+b0 6
+07
+08
+$end
+#1000000
+1#
+1(
+1/
+14
+#2000000
+1"
+0#
+b1 $
+b100011 %
+1'
+0(
+b10000 )
+b100000 *
+1+
+1,
+1.
+0/
+b1 0
+b100011 1
+13
+04
+b10000 5
+b100000 6
+17
+18
+#3000000
+b10000 9
+b100000 I
+1#
+1(
+1/
+14
+b10000 $
+b100000 %
+b10000 0
+b100000 1
+#4000000
+0#
+0(
+b110000 )
+b1000000 *
+0+
+0/
+04
+b110000 5
+b1000000 6
+07
+#5000000
+b10000 9
+b1000000 I
+1#
+1(
+1/
+14
+b1000000 %
+b1000000 1
+#6000000
+0#
+0(
+b1010000 )
+b1100000 *
+1+
+0,
+0/
+04
+b1010000 5
+b1100000 6
+17
+08
+#7000000
+b1010000 9
+b1000000 I
+1#
+1(
+1/
+14
+b1010000 $
+b1010000 0
+#8000000
+0#
+0(
+b1110000 )
+b10000000 *
+0+
+0/
+04
+b1110000 5
+b10000000 6
+07
+#9000000
+1#
+1(
+1/
+14
+#10000000
+0#
+0'
+0(
+b10010000 )
+b10100000 *
+0/
+03
+04
+b10010000 5
+b10100000 6
+#11000000
+1#
+1(
+1/
+14
+#12000000
+0#
+b1 &
+1'
+0(
+1+
+1,
+0/
+b1 2
+13
+04
+17
+18
+#13000000
+b10010000 :
+b10100000 J
+1#
+1(
+1/
+14
+#14000000
+0#
+b10 &
+0(
+b10110000 )
+b11000000 *
+0/
+b10 2
+04
+b10110000 5
+b11000000 6
+#15000000
+b10110000 ;
+b11000000 K
+1#
+1(
+1/
+14
+#16000000
+0#
+0'
+0(
+b11010000 )
+b11100000 *
+0/
+03
+04
+b11010000 5
+b11100000 6
+#17000000
+1#
+1(
+1/
+14
+#18000000
+b1 !
+0#
+b10010000 $
+b10100000 %
+0(
+b1 -
+0/
+b10010000 0
+b10100000 1
+04
+#19000000
+1#
+1(
+1/
+14
+#20000000
+b10 !
+0#
+b10110000 $
+b11000000 %
+0(
+b10 -
+0/
+b10110000 0
+b11000000 1
+04
+#21000000
+1#
+1(
+1/
+14
+#22000000
+0#
+0(
+0/
+04

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

@@ -0,0 +1,363 @@
+$timescale 1 ps $end
+$scope module memories2 $end
+$scope struct rw $end
+$var wire 3 ! addr $end
+$var wire 1 " en $end
+$var wire 1 # clk $end
+$var wire 2 $ rdata $end
+$var wire 1 % wmode $end
+$var wire 2 & wdata $end
+$var wire 1 ' wmask $end
+$upscope $end
+$scope struct mem $end
+$scope struct contents $end
+$scope struct [0] $end
+$scope struct mem $end
+$var string 1 1 \$tag $end
+$var reg 1 6 HdlSome $end
+$upscope $end
+$upscope $end
+$scope struct [1] $end
+$scope struct mem $end
+$var string 1 2 \$tag $end
+$var reg 1 7 HdlSome $end
+$upscope $end
+$upscope $end
+$scope struct [2] $end
+$scope struct mem $end
+$var string 1 3 \$tag $end
+$var reg 1 8 HdlSome $end
+$upscope $end
+$upscope $end
+$scope struct [3] $end
+$scope struct mem $end
+$var string 1 4 \$tag $end
+$var reg 1 9 HdlSome $end
+$upscope $end
+$upscope $end
+$scope struct [4] $end
+$scope struct mem $end
+$var string 1 5 \$tag $end
+$var reg 1 : HdlSome $end
+$upscope $end
+$upscope $end
+$upscope $end
+$scope struct rw0 $end
+$var wire 3 ( addr $end
+$var wire 1 ) en $end
+$var wire 1 * clk $end
+$scope struct rdata $end
+$var string 1 + \$tag $end
+$var wire 1 , HdlSome $end
+$upscope $end
+$var wire 1 - wmode $end
+$scope struct wdata $end
+$var string 1 . \$tag $end
+$var wire 1 / HdlSome $end
+$upscope $end
+$var wire 1 0 wmask $end
+$upscope $end
+$upscope $end
+$upscope $end
+$enddefinitions $end
+$dumpvars
+sHdlSome\x20(1) 1
+16
+sHdlSome\x20(1) 2
+17
+sHdlSome\x20(1) 3
+18
+sHdlSome\x20(1) 4
+19
+sHdlSome\x20(1) 5
+1:
+b0 !
+0"
+0#
+b0 $
+0%
+b0 &
+0'
+b0 (
+0)
+0*
+sHdlNone\x20(0) +
+0,
+0-
+sHdlNone\x20(0) .
+0/
+00
+$end
+#250000
+1#
+1*
+#500000
+#750000
+0#
+0*
+#1000000
+1"
+1)
+#1250000
+1#
+1*
+b11 $
+sHdlSome\x20(1) +
+1,
+#1500000
+#1750000
+0#
+0*
+#2000000
+0"
+0)
+#2250000
+1#
+1*
+b0 $
+sHdlNone\x20(0) +
+0,
+#2500000
+#2750000
+0#
+0*
+#3000000
+1"
+1%
+1'
+1)
+1-
+10
+#3250000
+sHdlNone\x20(0) 1
+06
+1#
+1*
+#3500000
+#3750000
+0#
+0*
+#4000000
+0%
+0'
+0-
+00
+#4250000
+1#
+1*
+#4500000
+#4750000
+0#
+0*
+#5000000
+1%
+b11 &
+1-
+sHdlSome\x20(1) .
+1/
+#5250000
+1#
+1*
+#5500000
+#5750000
+0#
+0*
+#6000000
+b1 !
+b1 &
+1'
+b1 (
+0/
+10
+#6250000
+sHdlSome\x20(1) 2
+07
+1#
+1*
+#6500000
+#6750000
+0#
+0*
+#7000000
+b10 !
+b10 &
+b10 (
+sHdlNone\x20(0) .
+#7250000
+sHdlNone\x20(0) 3
+08
+1#
+1*
+#7500000
+#7750000
+0#
+0*
+#8000000
+b11 !
+b11 &
+b11 (
+sHdlSome\x20(1) .
+1/
+#8250000
+sHdlSome\x20(1) 4
+19
+1#
+1*
+#8500000
+#8750000
+0#
+0*
+#9000000
+b100 !
+b10 &
+b100 (
+sHdlNone\x20(0) .
+0/
+#9250000
+sHdlNone\x20(0) 5
+0:
+1#
+1*
+#9500000
+#9750000
+0#
+0*
+#10000000
+b101 !
+b1 &
+b101 (
+sHdlSome\x20(1) .
+#10250000
+1#
+1*
+#10500000
+#10750000
+0#
+0*
+#11000000
+b110 !
+b110 (
+#11250000
+1#
+1*
+#11500000
+#11750000
+0#
+0*
+#12000000
+b111 !
+b111 (
+#12250000
+1#
+1*
+#12500000
+#12750000
+0#
+0*
+#13000000
+0%
+b0 &
+0'
+0-
+sHdlNone\x20(0) .
+00
+#13250000
+1#
+1*
+#13500000
+#13750000
+0#
+0*
+#14000000
+b110 !
+b110 (
+#14250000
+1#
+1*
+#14500000
+#14750000
+0#
+0*
+#15000000
+b101 !
+b101 (
+#15250000
+1#
+1*
+#15500000
+#15750000
+0#
+0*
+#16000000
+b100 !
+b100 (
+#16250000
+1#
+1*
+#16500000
+#16750000
+0#
+0*
+#17000000
+b11 !
+b11 (
+#17250000
+1#
+1*
+b11 $
+sHdlSome\x20(1) +
+1,
+#17500000
+#17750000
+0#
+0*
+#18000000
+b10 !
+b10 (
+#18250000
+1#
+1*
+b0 $
+sHdlNone\x20(0) +
+0,
+#18500000
+#18750000
+0#
+0*
+#19000000
+b0 !
+b0 (
+#19250000
+1#
+1*
+#19500000
+#19750000
+0#
+0*
+#20000000
+b1 !
+b1 (
+#20250000
+1#
+1*
+b1 $
+sHdlSome\x20(1) +
+#20500000
+#20750000
+0#
+0*
+#21000000
+b0 !
+0"
+b0 (
+0)
+#21250000
+1#
+1*
+b0 $
+sHdlNone\x20(0) +
+#21500000
+#21750000
+0#
+0*
+#22000000

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

@@ -0,0 +1,836 @@
+$timescale 1 ps $end
+$scope module memories3 $end
+$scope struct r $end
+$var wire 3 ! addr $end
+$var wire 1 " en $end
+$var wire 1 # clk $end
+$scope struct data $end
+$var wire 8 $ \[0] $end
+$var wire 8 % \[1] $end
+$var wire 8 & \[2] $end
+$var wire 8 ' \[3] $end
+$var wire 8 ( \[4] $end
+$var wire 8 ) \[5] $end
+$var wire 8 * \[6] $end
+$var wire 8 + \[7] $end
+$upscope $end
+$upscope $end
+$scope struct w $end
+$var wire 3 , addr $end
+$var wire 1 - en $end
+$var wire 1 . clk $end
+$scope struct data $end
+$var wire 8 / \[0] $end
+$var wire 8 0 \[1] $end
+$var wire 8 1 \[2] $end
+$var wire 8 2 \[3] $end
+$var wire 8 3 \[4] $end
+$var wire 8 4 \[5] $end
+$var wire 8 5 \[6] $end
+$var wire 8 6 \[7] $end
+$upscope $end
+$scope struct mask $end
+$var wire 1 7 \[0] $end
+$var wire 1 8 \[1] $end
+$var wire 1 9 \[2] $end
+$var wire 1 : \[3] $end
+$var wire 1 ; \[4] $end
+$var wire 1 < \[5] $end
+$var wire 1 = \[6] $end
+$var wire 1 > \[7] $end
+$upscope $end
+$upscope $end
+$scope struct mem $end
+$scope struct contents $end
+$scope struct [0] $end
+$scope struct mem $end
+$var reg 8 ] \[0] $end
+$var reg 8 e \[1] $end
+$var reg 8 m \[2] $end
+$var reg 8 u \[3] $end
+$var reg 8 } \[4] $end
+$var reg 8 '" \[5] $end
+$var reg 8 /" \[6] $end
+$var reg 8 7" \[7] $end
+$upscope $end
+$upscope $end
+$scope struct [1] $end
+$scope struct mem $end
+$var reg 8 ^ \[0] $end
+$var reg 8 f \[1] $end
+$var reg 8 n \[2] $end
+$var reg 8 v \[3] $end
+$var reg 8 ~ \[4] $end
+$var reg 8 (" \[5] $end
+$var reg 8 0" \[6] $end
+$var reg 8 8" \[7] $end
+$upscope $end
+$upscope $end
+$scope struct [2] $end
+$scope struct mem $end
+$var reg 8 _ \[0] $end
+$var reg 8 g \[1] $end
+$var reg 8 o \[2] $end
+$var reg 8 w \[3] $end
+$var reg 8 !" \[4] $end
+$var reg 8 )" \[5] $end
+$var reg 8 1" \[6] $end
+$var reg 8 9" \[7] $end
+$upscope $end
+$upscope $end
+$scope struct [3] $end
+$scope struct mem $end
+$var reg 8 ` \[0] $end
+$var reg 8 h \[1] $end
+$var reg 8 p \[2] $end
+$var reg 8 x \[3] $end
+$var reg 8 "" \[4] $end
+$var reg 8 *" \[5] $end
+$var reg 8 2" \[6] $end
+$var reg 8 :" \[7] $end
+$upscope $end
+$upscope $end
+$scope struct [4] $end
+$scope struct mem $end
+$var reg 8 a \[0] $end
+$var reg 8 i \[1] $end
+$var reg 8 q \[2] $end
+$var reg 8 y \[3] $end
+$var reg 8 #" \[4] $end
+$var reg 8 +" \[5] $end
+$var reg 8 3" \[6] $end
+$var reg 8 ;" \[7] $end
+$upscope $end
+$upscope $end
+$scope struct [5] $end
+$scope struct mem $end
+$var reg 8 b \[0] $end
+$var reg 8 j \[1] $end
+$var reg 8 r \[2] $end
+$var reg 8 z \[3] $end
+$var reg 8 $" \[4] $end
+$var reg 8 ," \[5] $end
+$var reg 8 4" \[6] $end
+$var reg 8 <" \[7] $end
+$upscope $end
+$upscope $end
+$scope struct [6] $end
+$scope struct mem $end
+$var reg 8 c \[0] $end
+$var reg 8 k \[1] $end
+$var reg 8 s \[2] $end
+$var reg 8 { \[3] $end
+$var reg 8 %" \[4] $end
+$var reg 8 -" \[5] $end
+$var reg 8 5" \[6] $end
+$var reg 8 =" \[7] $end
+$upscope $end
+$upscope $end
+$scope struct [7] $end
+$scope struct mem $end
+$var reg 8 d \[0] $end
+$var reg 8 l \[1] $end
+$var reg 8 t \[2] $end
+$var reg 8 | \[3] $end
+$var reg 8 &" \[4] $end
+$var reg 8 ." \[5] $end
+$var reg 8 6" \[6] $end
+$var reg 8 >" \[7] $end
+$upscope $end
+$upscope $end
+$upscope $end
+$scope struct r0 $end
+$var wire 3 ? addr $end
+$var wire 1 @ en $end
+$var wire 1 A clk $end
+$scope struct data $end
+$var wire 8 B \[0] $end
+$var wire 8 C \[1] $end
+$var wire 8 D \[2] $end
+$var wire 8 E \[3] $end
+$var wire 8 F \[4] $end
+$var wire 8 G \[5] $end
+$var wire 8 H \[6] $end
+$var wire 8 I \[7] $end
+$upscope $end
+$upscope $end
+$scope struct w1 $end
+$var wire 3 J addr $end
+$var wire 1 K en $end
+$var wire 1 L clk $end
+$scope struct data $end
+$var wire 8 M \[0] $end
+$var wire 8 N \[1] $end
+$var wire 8 O \[2] $end
+$var wire 8 P \[3] $end
+$var wire 8 Q \[4] $end
+$var wire 8 R \[5] $end
+$var wire 8 S \[6] $end
+$var wire 8 T \[7] $end
+$upscope $end
+$scope struct mask $end
+$var wire 1 U \[0] $end
+$var wire 1 V \[1] $end
+$var wire 1 W \[2] $end
+$var wire 1 X \[3] $end
+$var wire 1 Y \[4] $end
+$var wire 1 Z \[5] $end
+$var wire 1 [ \[6] $end
+$var wire 1 \ \[7] $end
+$upscope $end
+$upscope $end
+$upscope $end
+$upscope $end
+$enddefinitions $end
+$dumpvars
+b0 ]
+b0 e
+b0 m
+b0 u
+b0 }
+b0 '"
+b0 /"
+b0 7"
+b0 ^
+b0 f
+b0 n
+b0 v
+b0 ~
+b0 ("
+b0 0"
+b0 8"
+b0 _
+b0 g
+b0 o
+b0 w
+b0 !"
+b0 )"
+b0 1"
+b0 9"
+b0 `
+b0 h
+b0 p
+b0 x
+b0 ""
+b0 *"
+b0 2"
+b0 :"
+b0 a
+b0 i
+b0 q
+b0 y
+b0 #"
+b0 +"
+b0 3"
+b0 ;"
+b0 b
+b0 j
+b0 r
+b0 z
+b0 $"
+b0 ,"
+b0 4"
+b0 <"
+b0 c
+b0 k
+b0 s
+b0 {
+b0 %"
+b0 -"
+b0 5"
+b0 ="
+b0 d
+b0 l
+b0 t
+b0 |
+b0 &"
+b0 ."
+b0 6"
+b0 >"
+b0 !
+0"
+0#
+b0 $
+b0 %
+b0 &
+b0 '
+b0 (
+b0 )
+b0 *
+b0 +
+b0 ,
+1-
+0.
+b10010 /
+b110100 0
+b1010110 1
+b1111000 2
+b10011010 3
+b10111100 4
+b11011110 5
+b11110000 6
+07
+18
+09
+1:
+1;
+0<
+0=
+1>
+b0 ?
+0@
+0A
+b0 B
+b0 C
+b0 D
+b0 E
+b0 F
+b0 G
+b0 H
+b0 I
+b0 J
+1K
+0L
+b10010 M
+b110100 N
+b1010110 O
+b1111000 P
+b10011010 Q
+b10111100 R
+b11011110 S
+b11110000 T
+0U
+1V
+0W
+1X
+1Y
+0Z
+0[
+1\
+$end
+#250000
+1#
+1.
+1A
+1L
+#500000
+#750000
+0#
+0.
+0A
+0L
+#1000000
+1"
+b1 ,
+0-
+b0 /
+b0 0
+b0 1
+b0 2
+b0 3
+b0 4
+b0 5
+b0 6
+08
+0:
+0;
+0>
+1@
+b1 J
+0K
+b0 M
+b0 N
+b0 O
+b0 P
+b0 Q
+b0 R
+b0 S
+b0 T
+0V
+0X
+0Y
+0\
+#1250000
+b0 ]
+b110100 e
+b0 m
+b1111000 u
+b10011010 }
+b0 '"
+b0 /"
+b11110000 7"
+1#
+1.
+1A
+1L
+#1500000
+#1750000
+0#
+0.
+0A
+0L
+#2000000
+#2250000
+1#
+1.
+1A
+1L
+#2500000
+#2750000
+0#
+0.
+0A
+0L
+#3000000
+b0 ,
+1-
+b11111110 /
+b11011100 0
+b10111010 1
+b10011000 2
+b1110110 3
+b1010100 4
+b110010 5
+b10000 6
+17
+18
+19
+1:
+1;
+1<
+1=
+1>
+b0 J
+1K
+b11111110 M
+b11011100 N
+b10111010 O
+b10011000 P
+b1110110 Q
+b1010100 R
+b110010 S
+b10000 T
+1U
+1V
+1W
+1X
+1Y
+1Z
+1[
+1\
+#3250000
+1#
+1.
+1A
+b110100 C
+b1111000 E
+b10011010 F
+b11110000 I
+1L
+b110100 %
+b1111000 '
+b10011010 (
+b11110000 +
+#3500000
+#3750000
+0#
+0.
+0A
+0L
+#4000000
+#4250000
+b11111110 ]
+b11011100 e
+b10111010 m
+b10011000 u
+b1110110 }
+b1010100 '"
+b110010 /"
+b10000 7"
+1#
+1.
+1A
+1L
+#4500000
+#4750000
+0#
+0.
+0A
+0L
+#5000000
+#5250000
+b11111110 ]
+b11011100 e
+b10111010 m
+b10011000 u
+b1110110 }
+b1010100 '"
+b110010 /"
+b10000 7"
+1#
+1.
+1A
+1L
+#5500000
+#5750000
+0#
+0.
+0A
+0L
+#6000000
+0"
+b1 ,
+b10011 /
+b1010111 0
+b10011011 1
+b11011111 2
+b10 3
+b1000110 4
+b10001010 5
+b11001110 6
+0@
+b1 J
+b10011 M
+b1010111 N
+b10011011 O
+b11011111 P
+b10 Q
+b1000110 R
+b10001010 S
+b11001110 T
+#6250000
+b11111110 ]
+b11011100 e
+b10111010 m
+b10011000 u
+b1110110 }
+b1010100 '"
+b110010 /"
+b10000 7"
+1#
+1.
+1A
+b11111110 B
+b11011100 C
+b10111010 D
+b10011000 E
+b1110110 F
+b1010100 G
+b110010 H
+b10000 I
+1L
+b11111110 $
+b11011100 %
+b10111010 &
+b10011000 '
+b1110110 (
+b1010100 )
+b110010 *
+b10000 +
+#6500000
+#6750000
+0#
+0.
+0A
+0L
+#7000000
+b10 ,
+b1110100 /
+b1100101 0
+b1110011 1
+b1110100 2
+b1101001 3
+b1101110 4
+b1100111 5
+b100001 6
+b10 J
+b1110100 M
+b1100101 N
+b1110011 O
+b1110100 P
+b1101001 Q
+b1101110 R
+b1100111 S
+b100001 T
+#7250000
+b10011 ^
+b1010111 f
+b10011011 n
+b11011111 v
+b10 ~
+b1000110 ("
+b10001010 0"
+b11001110 8"
+1#
+1.
+1A
+b0 B
+b0 C
+b0 D
+b0 E
+b0 F
+b0 G
+b0 H
+b0 I
+1L
+b0 $
+b0 %
+b0 &
+b0 '
+b0 (
+b0 )
+b0 *
+b0 +
+#7500000
+#7750000
+0#
+0.
+0A
+0L
+#8000000
+b11 ,
+b1101101 /
+b1101111 0
+b1110010 1
+b1100101 2
+b100000 3
+b1110100 4
+b1110011 5
+b1110100 6
+b11 J
+b1101101 M
+b1101111 N
+b1110010 O
+b1100101 P
+b100000 Q
+b1110100 R
+b1110011 S
+b1110100 T
+#8250000
+b1110100 _
+b1100101 g
+b1110011 o
+b1110100 w
+b1101001 !"
+b1101110 )"
+b1100111 1"
+b100001 9"
+1#
+1.
+1A
+1L
+#8500000
+#8750000
+0#
+0.
+0A
+0L
+#9000000
+1"
+b0 ,
+0-
+b0 /
+b0 0
+b0 1
+b0 2
+b0 3
+b0 4
+b0 5
+b0 6
+07
+08
+09
+0:
+0;
+0<
+0=
+0>
+1@
+b0 J
+0K
+b0 M
+b0 N
+b0 O
+b0 P
+b0 Q
+b0 R
+b0 S
+b0 T
+0U
+0V
+0W
+0X
+0Y
+0Z
+0[
+0\
+#9250000
+b1101101 `
+b1101111 h
+b1110010 p
+b1100101 x
+b100000 ""
+b1110100 *"
+b1110011 2"
+b1110100 :"
+1#
+1.
+1A
+1L
+#9500000
+#9750000
+0#
+0.
+0A
+0L
+#10000000
+b1 !
+b1 ?
+#10250000
+1#
+1.
+1A
+b11111110 B
+b11011100 C
+b10111010 D
+b10011000 E
+b1110110 F
+b1010100 G
+b110010 H
+b10000 I
+1L
+b11111110 $
+b11011100 %
+b10111010 &
+b10011000 '
+b1110110 (
+b1010100 )
+b110010 *
+b10000 +
+#10500000
+#10750000
+0#
+0.
+0A
+0L
+#11000000
+b10 !
+b10 ?
+#11250000
+1#
+1.
+1A
+b10011 B
+b1010111 C
+b10011011 D
+b11011111 E
+b10 F
+b1000110 G
+b10001010 H
+b11001110 I
+1L
+b10011 $
+b1010111 %
+b10011011 &
+b11011111 '
+b10 (
+b1000110 )
+b10001010 *
+b11001110 +
+#11500000
+#11750000
+0#
+0.
+0A
+0L
+#12000000
+b11 !
+b11 ?
+#12250000
+1#
+1.
+1A
+b1110100 B
+b1100101 C
+b1110011 D
+b1110100 E
+b1101001 F
+b1101110 G
+b1100111 H
+b100001 I
+1L
+b1110100 $
+b1100101 %
+b1110011 &
+b1110100 '
+b1101001 (
+b1101110 )
+b1100111 *
+b100001 +
+#12500000
+#12750000
+0#
+0.
+0A
+0L
+#13000000
+b0 !
+0"
+b0 ?
+0@
+#13250000
+1#
+1.
+1A
+b1101101 B
+b1101111 C
+b1110010 D
+b1100101 E
+b100000 F
+b1110100 G
+b1110011 H
+b1110100 I
+1L
+b1101101 $
+b1101111 %
+b1110010 &
+b1100101 '
+b100000 (
+b1110100 )
+b1110011 *
+b1110100 +
+#13500000
+#13750000
+0#
+0.
+0A
+0L
+#14000000
+#14250000
+1#
+1.
+1A
+b0 B
+b0 C
+b0 D
+b0 E
+b0 F
+b0 G
+b0 H
+b0 I
+1L
+b0 $
+b0 %
+b0 &
+b0 '
+b0 (
+b0 )
+b0 *
+b0 +
+#14500000
+#14750000
+0#
+0.
+0A
+0L
+#15000000

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

@@ -3,12 +3,12 @@ Simulation {
         insns: Insns {
             state_layout: StateLayout {
                 ty: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 17,
                         debug_data: [
                             SlotDebugData {
@@ -83,7 +83,7 @@ Simulation {
                         ..
                     },
                 },
-                memories: StatePartAllocationLayout<Memories> {
+                memories: StatePartLayout<Memories> {
                     len: 0,
                     debug_data: [],
                     layout_data: [],
@@ -92,90 +92,90 @@ Simulation {
             },
             insns: [
                 // at: module-XXXXXXXXXX.rs:4:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(6), // SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.i2", ty: SInt<2> },
-                    src: StatePartIndex<BigSlots>(2), // SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::o.i2", ty: SInt<2> },
+                0: Copy {
+                    dest: StatePartIndex<BigSlots>(6), // (-0x2) SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.i2", ty: SInt<2> },
+                    src: StatePartIndex<BigSlots>(2), // (-0x2) SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::o.i2", ty: SInt<2> },
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(4), // SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.i", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(0), // SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::o.i", ty: UInt<4> },
+                1: Copy {
+                    dest: StatePartIndex<BigSlots>(4), // (0xa) SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.i", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(0), // (0xa) SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::o.i", ty: UInt<4> },
                 },
                 // at: module-XXXXXXXXXX.rs:2:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(10), // SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::i2", ty: SInt<2> },
-                    src: StatePartIndex<BigSlots>(6), // SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.i2", ty: SInt<2> },
+                2: Copy {
+                    dest: StatePartIndex<BigSlots>(10), // (-0x2) SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::i2", ty: SInt<2> },
+                    src: StatePartIndex<BigSlots>(6), // (-0x2) SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.i2", ty: SInt<2> },
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(8), // SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::i", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(4), // SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.i", ty: UInt<4> },
+                3: Copy {
+                    dest: StatePartIndex<BigSlots>(8), // (0xa) SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::i", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(4), // (0xa) SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.i", ty: UInt<4> },
                 },
                 // at: module-XXXXXXXXXX-2.rs:1:1
-                Const {
-                    dest: StatePartIndex<BigSlots>(16), // SlotDebugData { name: "", ty: UInt<4> },
-                    value: 15,
+                4: Const {
+                    dest: StatePartIndex<BigSlots>(16), // (0xf) SlotDebugData { name: "", ty: UInt<4> },
+                    value: 0xf,
                 },
-                Const {
-                    dest: StatePartIndex<BigSlots>(14), // SlotDebugData { name: "", ty: UInt<4> },
-                    value: 5,
+                5: Const {
+                    dest: StatePartIndex<BigSlots>(14), // (0x5) SlotDebugData { name: "", ty: UInt<4> },
+                    value: 0x5,
                 },
-                CmpLt {
-                    dest: StatePartIndex<BigSlots>(15), // SlotDebugData { name: "", ty: Bool },
-                    lhs: StatePartIndex<BigSlots>(14), // SlotDebugData { name: "", ty: UInt<4> },
-                    rhs: StatePartIndex<BigSlots>(8), // SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::i", ty: UInt<4> },
+                6: CmpLt {
+                    dest: StatePartIndex<BigSlots>(15), // (0x1) SlotDebugData { name: "", ty: Bool },
+                    lhs: StatePartIndex<BigSlots>(14), // (0x5) SlotDebugData { name: "", ty: UInt<4> },
+                    rhs: StatePartIndex<BigSlots>(8), // (0xa) SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::i", ty: UInt<4> },
                 },
-                CastToUInt {
-                    dest: StatePartIndex<BigSlots>(13), // SlotDebugData { name: "", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(10), // SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::i2", ty: SInt<2> },
+                7: CastToUInt {
+                    dest: StatePartIndex<BigSlots>(13), // (0xe) SlotDebugData { name: "", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(10), // (-0x2) SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::i2", ty: SInt<2> },
                     dest_width: 4,
                 },
                 // at: module-XXXXXXXXXX-2.rs:7:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(11), // SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::o2", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(13), // SlotDebugData { name: "", ty: UInt<4> },
+                8: Copy {
+                    dest: StatePartIndex<BigSlots>(11), // (0xf) SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::o2", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(13), // (0xe) SlotDebugData { name: "", ty: UInt<4> },
                 },
                 // at: module-XXXXXXXXXX-2.rs:8:1
-                BranchIfZero {
+                9: BranchIfZero {
                     target: 11,
-                    value: StatePartIndex<BigSlots>(15), // SlotDebugData { name: "", ty: Bool },
+                    value: StatePartIndex<BigSlots>(15), // (0x1) SlotDebugData { name: "", ty: Bool },
                 },
                 // at: module-XXXXXXXXXX-2.rs:9:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(11), // SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::o2", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(16), // SlotDebugData { name: "", ty: UInt<4> },
+                10: Copy {
+                    dest: StatePartIndex<BigSlots>(11), // (0xf) SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::o2", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(16), // (0xf) SlotDebugData { name: "", ty: UInt<4> },
                 },
                 // at: module-XXXXXXXXXX.rs:2:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(7), // SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.o2", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(11), // SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::o2", ty: UInt<4> },
+                11: Copy {
+                    dest: StatePartIndex<BigSlots>(7), // (0xf) SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.o2", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(11), // (0xf) SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::o2", ty: UInt<4> },
                 },
                 // at: module-XXXXXXXXXX.rs:4:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(3), // SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::o.o2", ty: UInt<4> },
-                    src: StatePartIndex<BigSlots>(7), // SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.o2", ty: UInt<4> },
+                12: Copy {
+                    dest: StatePartIndex<BigSlots>(3), // (0xf) SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::o.o2", ty: UInt<4> },
+                    src: StatePartIndex<BigSlots>(7), // (0xf) SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.o2", ty: UInt<4> },
                 },
                 // at: module-XXXXXXXXXX-2.rs:1:1
-                CastToSInt {
-                    dest: StatePartIndex<BigSlots>(12), // SlotDebugData { name: "", ty: SInt<2> },
-                    src: StatePartIndex<BigSlots>(8), // SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::i", ty: UInt<4> },
+                13: CastToSInt {
+                    dest: StatePartIndex<BigSlots>(12), // (-0x2) SlotDebugData { name: "", ty: SInt<2> },
+                    src: StatePartIndex<BigSlots>(8), // (0xa) SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::i", ty: UInt<4> },
                     dest_width: 2,
                 },
                 // at: module-XXXXXXXXXX-2.rs:6:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(9), // SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::o", ty: SInt<2> },
-                    src: StatePartIndex<BigSlots>(12), // SlotDebugData { name: "", ty: SInt<2> },
+                14: Copy {
+                    dest: StatePartIndex<BigSlots>(9), // (-0x2) SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::o", ty: SInt<2> },
+                    src: StatePartIndex<BigSlots>(12), // (-0x2) SlotDebugData { name: "", ty: SInt<2> },
                 },
                 // at: module-XXXXXXXXXX.rs:2:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(5), // SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.o", ty: SInt<2> },
-                    src: StatePartIndex<BigSlots>(9), // SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::o", ty: SInt<2> },
+                15: Copy {
+                    dest: StatePartIndex<BigSlots>(5), // (-0x2) SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.o", ty: SInt<2> },
+                    src: StatePartIndex<BigSlots>(9), // (-0x2) SlotDebugData { name: "InstantiatedModule(mod1.child: mod1_child).mod1_child::o", ty: SInt<2> },
                 },
                 // at: module-XXXXXXXXXX.rs:4:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(1), // SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::o.o", ty: SInt<2> },
-                    src: StatePartIndex<BigSlots>(5), // SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.o", ty: SInt<2> },
+                16: Copy {
+                    dest: StatePartIndex<BigSlots>(1), // (-0x2) SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::o.o", ty: SInt<2> },
+                    src: StatePartIndex<BigSlots>(5), // (-0x2) SlotDebugData { name: "InstantiatedModule(mod1: mod1).mod1::child.o", ty: SInt<2> },
                 },
                 // at: module-XXXXXXXXXX.rs:1:1
-                Return,
+                17: Return,
             ],
             ..
         },
@@ -237,12 +237,12 @@ Simulation {
                     o2: UInt<4>,
                 },
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 4,
                         debug_data: [
                             SlotDebugData {
@@ -275,12 +275,12 @@ Simulation {
                             ty: CompiledTypeLayout {
                                 ty: UInt<4>,
                                 layout: TypeLayout {
-                                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                                    small_slots: StatePartLayout<SmallSlots> {
                                         len: 0,
                                         debug_data: [],
                                         ..
                                     },
-                                    big_slots: StatePartAllocationLayout<BigSlots> {
+                                    big_slots: StatePartLayout<BigSlots> {
                                         len: 1,
                                         debug_data: [
                                             SlotDebugData {
@@ -302,12 +302,12 @@ Simulation {
                             ty: CompiledTypeLayout {
                                 ty: SInt<2>,
                                 layout: TypeLayout {
-                                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                                    small_slots: StatePartLayout<SmallSlots> {
                                         len: 0,
                                         debug_data: [],
                                         ..
                                     },
-                                    big_slots: StatePartAllocationLayout<BigSlots> {
+                                    big_slots: StatePartLayout<BigSlots> {
                                         len: 1,
                                         debug_data: [
                                             SlotDebugData {
@@ -329,12 +329,12 @@ Simulation {
                             ty: CompiledTypeLayout {
                                 ty: SInt<2>,
                                 layout: TypeLayout {
-                                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                                    small_slots: StatePartLayout<SmallSlots> {
                                         len: 0,
                                         debug_data: [],
                                         ..
                                     },
-                                    big_slots: StatePartAllocationLayout<BigSlots> {
+                                    big_slots: StatePartLayout<BigSlots> {
                                         len: 1,
                                         debug_data: [
                                             SlotDebugData {
@@ -356,12 +356,12 @@ Simulation {
                             ty: CompiledTypeLayout {
                                 ty: UInt<4>,
                                 layout: TypeLayout {
-                                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                                    small_slots: StatePartLayout<SmallSlots> {
                                         len: 0,
                                         debug_data: [],
                                         ..
                                     },
-                                    big_slots: StatePartAllocationLayout<BigSlots> {
+                                    big_slots: StatePartLayout<BigSlots> {
                                         len: 1,
                                         debug_data: [
                                             SlotDebugData {
@@ -394,12 +394,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: UInt<4>,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -428,12 +428,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: SInt<2>,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -462,12 +462,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: SInt<2>,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -496,12 +496,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: UInt<4>,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -806,4 +806,5 @@ Simulation {
     ],
     instant: 2 μs,
     clocks_triggered: [],
+    ..
 }

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

@@ -3,7 +3,7 @@ Simulation {
         insns: Insns {
             state_layout: StateLayout {
                 ty: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 4,
                         debug_data: [
                             SlotDebugData {
@@ -25,7 +25,7 @@ Simulation {
                         ],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 13,
                         debug_data: [
                             SlotDebugData {
@@ -84,7 +84,7 @@ Simulation {
                         ..
                     },
                 },
-                memories: StatePartAllocationLayout<Memories> {
+                memories: StatePartLayout<Memories> {
                     len: 0,
                     debug_data: [],
                     layout_data: [],
@@ -93,136 +93,137 @@ Simulation {
             },
             insns: [
                 // at: module-XXXXXXXXXX.rs:13:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(3), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::q", ty: Bool },
-                    src: StatePartIndex<BigSlots>(11), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg3", ty: Bool },
+                0: Copy {
+                    dest: StatePartIndex<BigSlots>(3), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::q", ty: Bool },
+                    src: StatePartIndex<BigSlots>(11), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg3", ty: Bool },
                 },
                 // at: module-XXXXXXXXXX.rs:12:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(12), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg3$next", ty: Bool },
-                    src: StatePartIndex<BigSlots>(9), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg2", ty: Bool },
+                1: Copy {
+                    dest: StatePartIndex<BigSlots>(12), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg3$next", ty: Bool },
+                    src: StatePartIndex<BigSlots>(9), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg2", ty: Bool },
                 },
                 // at: module-XXXXXXXXXX.rs:10:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(10), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg2$next", ty: Bool },
-                    src: StatePartIndex<BigSlots>(7), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg1", ty: Bool },
+                2: Copy {
+                    dest: StatePartIndex<BigSlots>(10), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg2$next", ty: Bool },
+                    src: StatePartIndex<BigSlots>(7), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg1", ty: Bool },
                 },
                 // at: module-XXXXXXXXXX.rs:8:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(8), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg1$next", ty: Bool },
-                    src: StatePartIndex<BigSlots>(4), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg0", ty: Bool },
+                3: Copy {
+                    dest: StatePartIndex<BigSlots>(8), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg1$next", ty: Bool },
+                    src: StatePartIndex<BigSlots>(4), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg0", ty: Bool },
                 },
                 // at: module-XXXXXXXXXX.rs:6:1
-                Copy {
-                    dest: StatePartIndex<BigSlots>(5), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg0$next", ty: Bool },
-                    src: StatePartIndex<BigSlots>(2), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::d", ty: Bool },
+                4: Copy {
+                    dest: StatePartIndex<BigSlots>(5), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg0$next", ty: Bool },
+                    src: StatePartIndex<BigSlots>(2), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::d", ty: Bool },
                 },
                 // at: module-XXXXXXXXXX.rs:5:1
-                IsNonZeroDestIsSmall {
-                    dest: StatePartIndex<SmallSlots>(3), // SlotDebugData { name: "", ty: Bool },
-                    src: StatePartIndex<BigSlots>(1), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::cd.rst", ty: SyncReset },
+                5: IsNonZeroDestIsSmall {
+                    dest: StatePartIndex<SmallSlots>(3), // (0x0 0) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(1), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::cd.rst", ty: SyncReset },
                 },
                 // at: module-XXXXXXXXXX.rs:1:1
-                Const {
-                    dest: StatePartIndex<BigSlots>(6), // SlotDebugData { name: "", ty: Bool },
-                    value: 0,
+                6: Const {
+                    dest: StatePartIndex<BigSlots>(6), // (0x0) SlotDebugData { name: "", ty: Bool },
+                    value: 0x0,
                 },
                 // at: module-XXXXXXXXXX.rs:5:1
-                IsNonZeroDestIsSmall {
-                    dest: StatePartIndex<SmallSlots>(2), // SlotDebugData { name: "", ty: Bool },
-                    src: StatePartIndex<BigSlots>(0), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::cd.clk", ty: Clock },
+                7: IsNonZeroDestIsSmall {
+                    dest: StatePartIndex<SmallSlots>(2), // (0x1 1) SlotDebugData { name: "", ty: Bool },
+                    src: StatePartIndex<BigSlots>(0), // (0x1) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::cd.clk", ty: Clock },
                 },
-                AndSmall {
-                    dest: StatePartIndex<SmallSlots>(1), // SlotDebugData { name: "", ty: Bool },
-                    lhs: StatePartIndex<SmallSlots>(2), // SlotDebugData { name: "", ty: Bool },
-                    rhs: StatePartIndex<SmallSlots>(0), // SlotDebugData { name: "", ty: Bool },
+                8: 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 },
                 },
-                BranchIfSmallZero {
+                9: BranchIfSmallZero {
                     target: 14,
-                    value: StatePartIndex<SmallSlots>(1), // SlotDebugData { name: "", ty: Bool },
+                    value: StatePartIndex<SmallSlots>(1), // (0x0 0) SlotDebugData { name: "", ty: Bool },
                 },
-                BranchIfSmallNonZero {
+                10: BranchIfSmallNonZero {
                     target: 13,
-                    value: StatePartIndex<SmallSlots>(3), // SlotDebugData { name: "", ty: Bool },
+                    value: StatePartIndex<SmallSlots>(3), // (0x0 0) SlotDebugData { name: "", ty: Bool },
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(4), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg0", ty: Bool },
-                    src: StatePartIndex<BigSlots>(5), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg0$next", ty: Bool },
+                11: Copy {
+                    dest: StatePartIndex<BigSlots>(4), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg0", ty: Bool },
+                    src: StatePartIndex<BigSlots>(5), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg0$next", ty: Bool },
                 },
-                Branch {
+                12: Branch {
                     target: 14,
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(4), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg0", ty: Bool },
-                    src: StatePartIndex<BigSlots>(6), // SlotDebugData { name: "", ty: Bool },
+                13: Copy {
+                    dest: StatePartIndex<BigSlots>(4), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg0", ty: Bool },
+                    src: StatePartIndex<BigSlots>(6), // (0x0) SlotDebugData { name: "", ty: Bool },
                 },
                 // at: module-XXXXXXXXXX.rs:7:1
-                BranchIfSmallZero {
+                14: BranchIfSmallZero {
                     target: 19,
-                    value: StatePartIndex<SmallSlots>(1), // SlotDebugData { name: "", ty: Bool },
+                    value: StatePartIndex<SmallSlots>(1), // (0x0 0) SlotDebugData { name: "", ty: Bool },
                 },
-                BranchIfSmallNonZero {
+                15: BranchIfSmallNonZero {
                     target: 18,
-                    value: StatePartIndex<SmallSlots>(3), // SlotDebugData { name: "", ty: Bool },
+                    value: StatePartIndex<SmallSlots>(3), // (0x0 0) SlotDebugData { name: "", ty: Bool },
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(7), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg1", ty: Bool },
-                    src: StatePartIndex<BigSlots>(8), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg1$next", ty: Bool },
+                16: Copy {
+                    dest: StatePartIndex<BigSlots>(7), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg1", ty: Bool },
+                    src: StatePartIndex<BigSlots>(8), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg1$next", ty: Bool },
                 },
-                Branch {
+                17: Branch {
                     target: 19,
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(7), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg1", ty: Bool },
-                    src: StatePartIndex<BigSlots>(6), // SlotDebugData { name: "", ty: Bool },
+                18: Copy {
+                    dest: StatePartIndex<BigSlots>(7), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg1", ty: Bool },
+                    src: StatePartIndex<BigSlots>(6), // (0x0) SlotDebugData { name: "", ty: Bool },
                 },
                 // at: module-XXXXXXXXXX.rs:9:1
-                BranchIfSmallZero {
+                19: BranchIfSmallZero {
                     target: 24,
-                    value: StatePartIndex<SmallSlots>(1), // SlotDebugData { name: "", ty: Bool },
+                    value: StatePartIndex<SmallSlots>(1), // (0x0 0) SlotDebugData { name: "", ty: Bool },
                 },
-                BranchIfSmallNonZero {
+                20: BranchIfSmallNonZero {
                     target: 23,
-                    value: StatePartIndex<SmallSlots>(3), // SlotDebugData { name: "", ty: Bool },
+                    value: StatePartIndex<SmallSlots>(3), // (0x0 0) SlotDebugData { name: "", ty: Bool },
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(9), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg2", ty: Bool },
-                    src: StatePartIndex<BigSlots>(10), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg2$next", ty: Bool },
+                21: Copy {
+                    dest: StatePartIndex<BigSlots>(9), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg2", ty: Bool },
+                    src: StatePartIndex<BigSlots>(10), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg2$next", ty: Bool },
                 },
-                Branch {
+                22: Branch {
                     target: 24,
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(9), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg2", ty: Bool },
-                    src: StatePartIndex<BigSlots>(6), // SlotDebugData { name: "", ty: Bool },
+                23: Copy {
+                    dest: StatePartIndex<BigSlots>(9), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg2", ty: Bool },
+                    src: StatePartIndex<BigSlots>(6), // (0x0) SlotDebugData { name: "", ty: Bool },
                 },
                 // at: module-XXXXXXXXXX.rs:11:1
-                BranchIfSmallZero {
+                24: BranchIfSmallZero {
                     target: 29,
-                    value: StatePartIndex<SmallSlots>(1), // SlotDebugData { name: "", ty: Bool },
+                    value: StatePartIndex<SmallSlots>(1), // (0x0 0) SlotDebugData { name: "", ty: Bool },
                 },
-                BranchIfSmallNonZero {
+                25: BranchIfSmallNonZero {
                     target: 28,
-                    value: StatePartIndex<SmallSlots>(3), // SlotDebugData { name: "", ty: Bool },
+                    value: StatePartIndex<SmallSlots>(3), // (0x0 0) SlotDebugData { name: "", ty: Bool },
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(11), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg3", ty: Bool },
-                    src: StatePartIndex<BigSlots>(12), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg3$next", ty: Bool },
+                26: Copy {
+                    dest: StatePartIndex<BigSlots>(11), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg3", ty: Bool },
+                    src: StatePartIndex<BigSlots>(12), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg3$next", ty: Bool },
                 },
-                Branch {
+                27: Branch {
                     target: 29,
                 },
-                Copy {
-                    dest: StatePartIndex<BigSlots>(11), // SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg3", ty: Bool },
-                    src: StatePartIndex<BigSlots>(6), // SlotDebugData { name: "", ty: Bool },
+                28: Copy {
+                    dest: StatePartIndex<BigSlots>(11), // (0x0) SlotDebugData { name: "InstantiatedModule(shift_register: shift_register).shift_register::reg3", ty: Bool },
+                    src: StatePartIndex<BigSlots>(6), // (0x0) SlotDebugData { name: "", ty: Bool },
                 },
                 // at: module-XXXXXXXXXX.rs:5:1
-                NotSmall {
-                    dest: StatePartIndex<SmallSlots>(0), // SlotDebugData { name: "", ty: Bool },
-                    src: StatePartIndex<SmallSlots>(2), // SlotDebugData { name: "", ty: Bool },
+                29: 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
-                Return,
+                30: Return,
             ],
             ..
         },
@@ -233,7 +234,7 @@ Simulation {
         },
         small_slots: StatePart {
             value: [
-                18446744073709551614,
+                0,
                 0,
                 1,
                 0,
@@ -281,12 +282,12 @@ Simulation {
                     rst: SyncReset,
                 },
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 2,
                         debug_data: [
                             SlotDebugData {
@@ -311,12 +312,12 @@ Simulation {
                             ty: CompiledTypeLayout {
                                 ty: Clock,
                                 layout: TypeLayout {
-                                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                                    small_slots: StatePartLayout<SmallSlots> {
                                         len: 0,
                                         debug_data: [],
                                         ..
                                     },
-                                    big_slots: StatePartAllocationLayout<BigSlots> {
+                                    big_slots: StatePartLayout<BigSlots> {
                                         len: 1,
                                         debug_data: [
                                             SlotDebugData {
@@ -338,12 +339,12 @@ Simulation {
                             ty: CompiledTypeLayout {
                                 ty: SyncReset,
                                 layout: TypeLayout {
-                                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                                    small_slots: StatePartLayout<SmallSlots> {
                                         len: 0,
                                         debug_data: [],
                                         ..
                                     },
-                                    big_slots: StatePartAllocationLayout<BigSlots> {
+                                    big_slots: StatePartLayout<BigSlots> {
                                         len: 1,
                                         debug_data: [
                                             SlotDebugData {
@@ -376,12 +377,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: Clock,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -410,12 +411,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: SyncReset,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -444,12 +445,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: Bool,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -478,12 +479,12 @@ Simulation {
             layout: CompiledTypeLayout {
                 ty: Bool,
                 layout: TypeLayout {
-                    small_slots: StatePartAllocationLayout<SmallSlots> {
+                    small_slots: StatePartLayout<SmallSlots> {
                         len: 0,
                         debug_data: [],
                         ..
                     },
-                    big_slots: StatePartAllocationLayout<BigSlots> {
+                    big_slots: StatePartLayout<BigSlots> {
                         len: 1,
                         debug_data: [
                             SlotDebugData {
@@ -678,4 +679,5 @@ Simulation {
     clocks_triggered: [
         StatePartIndex<SmallSlots>(1),
     ],
+    ..
 }