crates/fayalite/src/build/formal.rs

@@ -13,9 +13,10 @@ use crate::{
     },
     intern::{Intern, InternSlice, Interned},
     module::NameId,
+    testing::FormalMode,
     util::job_server::AcquiredJob,
 };
-use clap::{Args, ValueEnum};
+use clap::Args;
 use eyre::Context;
 use serde::{Deserialize, Serialize};
 use std::{
@@ -24,33 +25,6 @@ use std::{
     path::Path,
 };
 
-#[derive(ValueEnum, Copy, Clone, Debug, PartialEq, Eq, Hash, Default, Deserialize, Serialize)]
-#[non_exhaustive]
-pub enum FormalMode {
-    #[default]
-    BMC,
-    Prove,
-    Live,
-    Cover,
-}
-
-impl FormalMode {
-    pub fn as_str(self) -> &'static str {
-        match self {
-            FormalMode::BMC => "bmc",
-            FormalMode::Prove => "prove",
-            FormalMode::Live => "live",
-            FormalMode::Cover => "cover",
-        }
-    }
-}
-
-impl fmt::Display for FormalMode {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        f.write_str(self.as_str())
-    }
-}
-
 #[derive(Args, Clone, Debug, PartialEq, Eq, Hash)]
 #[non_exhaustive]
 pub struct FormalArgs {

crates/fayalite/src/int/uint_in_range.rs

@@ -304,6 +304,15 @@ macro_rules! define_uint_in_range_type {
                     $SerdeRange { start, end }.intern_sized(),
                 ))
             }
+            pub fn bit_width(self) -> usize {
+                self.value.width()
+            }
+            pub fn start(self) -> Start::SizeType {
+                self.range.get().start
+            }
+            pub fn end(self) -> End::SizeType {
+                self.range.get().end
+            }
         }
 
         impl<Start: Size, End: Size> fmt::Debug for $UIntInRangeType<Start, End> {
@@ -477,18 +486,22 @@ macro_rules! define_uint_in_range_type {
             }
         }
 
-        impl<Start: Size, End: Size> ExprCastTo<UInt> for $UIntInRangeType<Start, End> {
+        impl<Start: Size, End: Size, Width: Size> ExprCastTo<UIntType<Width>>
-            fn cast_to(src: Expr<Self>, to_type: UInt) -> Expr<UInt> {
+            for $UIntInRangeType<Start, End>
+        {
+            fn cast_to(src: Expr<Self>, to_type: UIntType<Width>) -> Expr<UIntType<Width>> {
                 src.cast_to_bits().cast_to(to_type)
             }
         }
 
-        impl<Start: Size, End: Size> ExprCastTo<$UIntInRangeType<Start, End>> for UInt {
+        impl<Start: Size, End: Size, Width: Size> ExprCastTo<$UIntInRangeType<Start, End>>
+            for UIntType<Width>
+        {
             fn cast_to(
                 src: Expr<Self>,
                 to_type: $UIntInRangeType<Start, End>,
             ) -> Expr<$UIntInRangeType<Start, End>> {
-                src.cast_bits_to(to_type)
+                src.cast_to(to_type.value).cast_bits_to(to_type)
             }
         }
 

crates/fayalite/src/prelude.rs

@@ -37,7 +37,7 @@ pub use crate::{
         value::{SimOnly, SimOnlyValue, SimValue, ToSimValue, ToSimValueWithType},
     },
     source_location::SourceLocation,
-    testing::assert_formal,
+    testing::{FormalMode, assert_formal},
     ty::{AsMask, CanonicalType, Type},
     util::{ConstUsize, GenericConstUsize},
     wire::Wire,

crates/fayalite/src/sim.rs

@@ -1522,7 +1522,7 @@ struct SimulationImpl {
     state_ready_to_run: bool,
     trace_decls: TraceModule,
     traces: SimTraces<Box<[SimTrace<SimTraceKind, SimTraceState>]>>,
-    trace_memories: HashMap<StatePartIndex<StatePartKindMemories>, TraceMem>,
+    trace_memories: BTreeMap<StatePartIndex<StatePartKindMemories>, TraceMem>,
     trace_writers: Vec<TraceWriterState<DynTraceWriterDecls>>,
     instant: SimInstant,
     clocks_triggered: Interned<[StatePartIndex<StatePartKindSmallSlots>]>,
@@ -1622,7 +1622,7 @@ impl SimulationImpl {
                     last_state: kind.make_state(),
                 },
             ))),
-            trace_memories: HashMap::from_iter(compiled.trace_memories.iter().copied()),
+            trace_memories: BTreeMap::from_iter(compiled.trace_memories.iter().copied()),
             trace_writers: vec![],
             instant: SimInstant::START,
             clocks_triggered: compiled.clocks_triggered,

crates/fayalite/src/testing.rs

@@ -6,7 +6,7 @@ use crate::{
         NoArgs, RunBuild,
         external::{ExternalCommandArgs, ExternalCommandJobKind},
         firrtl::{FirrtlArgs, FirrtlJobKind},
-        formal::{Formal, FormalAdditionalArgs, FormalArgs, FormalMode, WriteSbyFileJobKind},
+        formal::{Formal, FormalAdditionalArgs, FormalArgs, WriteSbyFileJobKind},
         verilog::{UnadjustedVerilogArgs, VerilogJobArgs, VerilogJobKind},
     },
     bundle::BundleType,
@@ -14,14 +14,43 @@ use crate::{
     module::Module,
     util::HashMap,
 };
-use serde::Deserialize;
+use serde::{Deserialize, Serialize};
 use std::{
-    fmt::Write,
+    fmt::{self, Write},
     path::{Path, PathBuf},
     process::Command,
     sync::{Mutex, OnceLock},
 };
 
+#[derive(
+    clap::ValueEnum, Copy, Clone, Debug, PartialEq, Eq, Hash, Default, Deserialize, Serialize,
+)]
+#[non_exhaustive]
+pub enum FormalMode {
+    #[default]
+    BMC,
+    Prove,
+    Live,
+    Cover,
+}
+
+impl FormalMode {
+    pub fn as_str(self) -> &'static str {
+        match self {
+            FormalMode::BMC => "bmc",
+            FormalMode::Prove => "prove",
+            FormalMode::Live => "live",
+            FormalMode::Cover => "cover",
+        }
+    }
+}
+
+impl fmt::Display for FormalMode {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.write_str(self.as_str())
+    }
+}
+
 #[derive(Deserialize)]
 struct CargoMetadata {
     target_directory: String,

crates/fayalite/src/util/ready_valid.rs

@@ -212,9 +212,7 @@ pub fn queue<T: Type>(
 mod tests {
     use super::*;
     use crate::{
-        build::formal::FormalMode, firrtl::ExportOptions,
+        firrtl::ExportOptions, module::transform::simplify_enums::SimplifyEnumsKind, ty::StaticType,
-        module::transform::simplify_enums::SimplifyEnumsKind, testing::assert_formal,
-        ty::StaticType,
     };
     use std::num::NonZero;
 

crates/fayalite/tests/formal.rs

@@ -2,19 +2,7 @@
 // See Notices.txt for copyright information
 //! Formal tests in Fayalite
 
-use fayalite::{
+use fayalite::prelude::*;
-    build::formal::FormalMode,
-    clock::{Clock, ClockDomain},
-    expr::{CastTo, HdlPartialEq},
-    firrtl::ExportOptions,
-    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
 ///
@@ -119,7 +107,7 @@ mod hidden_state {
             FormalMode::Prove,
             16,
             None,
-            ExportOptions::default(),
+            Default::default(),
         );
         // here a couple of cycles is enough
         assert_formal(
@@ -128,7 +116,7 @@ mod hidden_state {
             FormalMode::Prove,
             2,
             None,
-            ExportOptions::default(),
+            Default::default(),
         );
     }
 }
@@ -242,7 +230,7 @@ mod memory {
             #[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.data, any_seq(UInt::<8>::new_static()));
             connect(wr.en, any_seq(Bool));
             #[hdl]
             let dut = instance(example_sram(n));
@@ -289,7 +277,7 @@ mod memory {
             FormalMode::Prove,
             2,
             None,
-            ExportOptions::default(),
+            Default::default(),
         );
     }
 }

crates/fayalite/tests/sim.rs

@@ -3,7 +3,7 @@
 
 use fayalite::{
     memory::{ReadStruct, ReadWriteStruct, WriteStruct},
-    module::{instance_with_loc, reg_builder_with_loc},
+    module::{instance_with_loc, memory_with_init_and_loc, reg_builder_with_loc},
     prelude::*,
     reset::ResetType,
     sim::vcd::VcdWriterDecls,
@@ -1261,6 +1261,310 @@ fn test_memories3() {
     }
 }
 
+#[hdl_module(outline_generated)]
+pub fn many_memories() {
+    #[hdl]
+    let r: Array<ReadStruct<Bool, ConstUsize<4>>, 8> = m.input();
+    #[hdl]
+    let w: Array<WriteStruct<Bool, ConstUsize<4>>, 8> = m.input();
+    for (mem_index, (r, w)) in r.into_iter().zip(w).enumerate() {
+        let mut mem = memory_with_init_and_loc(
+            &format!("mem_{mem_index}"),
+            (0..16)
+                .map(|bit_index| mem_index.pow(5).to_expr()[bit_index])
+                .collect::<Vec<_>>(),
+            SourceLocation::caller(),
+        );
+        connect_any(mem.new_read_port(), r);
+        connect_any(mem.new_write_port(), w);
+    }
+}
+
+#[hdl]
+#[test]
+fn test_many_memories() {
+    let _n = SourceLocation::normalize_files_for_tests();
+    let mut sim = Simulation::new(many_memories());
+    let mut writer = RcWriter::default();
+    sim.add_trace_writer(VcdWriterDecls::new(writer.clone()));
+    for r in sim.io().r {
+        sim.write_clock(r.clk, false);
+    }
+    for w in sim.io().w {
+        sim.write_clock(w.clk, false);
+    }
+    #[hdl(cmp_eq)]
+    struct IO {
+        r_addr: UInt<4>,
+        r_en: Bool,
+        r_data: Array<Bool, 8>,
+        w_addr: UInt<4>,
+        w_en: Bool,
+        w_data: Array<Bool, 8>,
+        w_mask: Array<Bool, 8>,
+    }
+    let io_cycles = [
+        #[hdl(sim)]
+        IO {
+            r_addr: 0_hdl_u4,
+            r_en: false,
+            r_data: [false; 8],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [false; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 0_hdl_u4,
+            r_en: true,
+            r_data: [false, true, false, true, false, true, false, true],
+            w_addr: 0_hdl_u4,
+            w_en: true,
+            w_data: [true; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 0_hdl_u4,
+            r_en: true,
+            r_data: [true; 8],
+            w_addr: 0_hdl_u4,
+            w_en: true,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 0_hdl_u4,
+            r_en: true,
+            r_data: [false; 8],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 1_hdl_u4,
+            r_en: true,
+            r_data: [false, false, false, true, false, false, false, true],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 2_hdl_u4,
+            r_en: true,
+            r_data: [false, false, false, false, false, true, false, true],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 3_hdl_u4,
+            r_en: true,
+            r_data: [false, false, false, false, false, false, false, false],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 4_hdl_u4,
+            r_en: true,
+            r_data: [false, false, false, true, false, true, false, false],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 5_hdl_u4,
+            r_en: true,
+            r_data: [false, false, true, true, false, true, true, true],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 6_hdl_u4,
+            r_en: true,
+            r_data: [false, false, false, true, false, false, true, false],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 7_hdl_u4,
+            r_en: true,
+            r_data: [false, false, false, true, false, false, false, true],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 8_hdl_u4,
+            r_en: true,
+            r_data: [false, false, false, false, false, false, false, true],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 9_hdl_u4,
+            r_en: true,
+            r_data: [false, false, false, false, false, false, true, false],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 0xA_hdl_u4,
+            r_en: true,
+            r_data: [false, false, false, false, true, true, true, false],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 0xB_hdl_u4,
+            r_en: true,
+            r_data: [false, false, false, false, false, true, true, false],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 0xC_hdl_u4,
+            r_en: true,
+            r_data: [false, false, false, false, false, false, true, false],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 0xD_hdl_u4,
+            r_en: true,
+            r_data: [false, false, false, false, false, false, false, false],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 0xE_hdl_u4,
+            r_en: true,
+            r_data: [false, false, false, false, false, false, false, true],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+        #[hdl(sim)]
+        IO {
+            r_addr: 0xF_hdl_u4,
+            r_en: true,
+            r_data: [false, false, false, false, false, false, false, false],
+            w_addr: 0_hdl_u4,
+            w_en: false,
+            w_data: [false; 8],
+            w_mask: [true; 8],
+        },
+    ];
+    for (cycle, expected) in io_cycles.into_iter().enumerate() {
+        #[hdl(sim)]
+        let IO {
+            r_addr,
+            r_en,
+            r_data: _,
+            w_addr,
+            w_en,
+            w_data,
+            w_mask,
+        } = expected;
+        for (((r, w), w_data), w_mask) in sim
+            .io()
+            .r
+            .into_iter()
+            .zip(sim.io().w)
+            .zip(w_data.iter())
+            .zip(w_mask.iter())
+        {
+            sim.write(r.addr, &r_addr);
+            sim.write(r.en, &r_en);
+            sim.write(w.addr, &w_addr);
+            sim.write(w.en, &w_en);
+            sim.write(w.data, w_data);
+            sim.write(w.mask, w_mask);
+        }
+        let io = #[hdl(sim)]
+        IO {
+            r_addr,
+            r_en,
+            r_data: std::array::from_fn(|i| sim.read(sim.io().r[i].data)),
+            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_micros(1));
+        for r in sim.io().r {
+            sim.write_clock(r.clk, true);
+        }
+        for w in sim.io().w {
+            sim.write_clock(w.clk, true);
+        }
+        sim.advance_time(SimDuration::from_micros(1));
+        for r in sim.io().r {
+            sim.write_clock(r.clk, false);
+        }
+        for w in sim.io().w {
+            sim.write_clock(w.clk, false);
+        }
+    }
+    sim.flush_traces().unwrap();
+    let vcd = String::from_utf8(writer.take()).unwrap();
+    println!("####### VCD:\n{vcd}\n#######");
+    if vcd != include_str!("sim/expected/many_memories.vcd") {
+        panic!();
+    }
+    let sim_debug = format!("{sim:#?}");
+    println!("#######\n{sim_debug}\n#######");
+    if sim_debug != include_str!("sim/expected/many_memories.txt") {
+        panic!();
+    }
+}
+
 #[hdl_module(outline_generated)]
 pub fn duplicate_names() {
     #[hdl]