change SimulationImpl::trace_memories to a BTreeMap for consistent iteration order

.forgejo/workflows/test.yml

@@ -22,3 +22,4 @@ jobs:
       - run: cargo doc --features=unstable-doc
       - run: FAYALITE_TEST_HASHER=always_zero cargo test --test=module --features=unstable-doc,unstable-test-hasher
       - run: cargo run --example blinky yosys-nextpnr-xray --platform=arty-a7-100t --nextpnr-xilinx-chipdb-dir /opt/fayalite-deps/nextpnr-xilinx/xilinx --prjxray-db-dir /opt/fayalite-deps/prjxray-db -o target/blinky-out
+      - run: cargo run --example tx_only_uart yosys-nextpnr-xray --platform=arty-a7-100t --nextpnr-xilinx-chipdb-dir /opt/fayalite-deps/nextpnr-xilinx/xilinx --prjxray-db-dir /opt/fayalite-deps/prjxray-db -o target/tx_only_uart-out

README.md

@@ -8,6 +8,73 @@ Fayalite is a library for designing digital hardware -- a hardware description l
 
 [FIRRTL]: https://github.com/chipsalliance/firrtl-spec
 
+# Building the [Blinky example] for the Arty A7 100T on Linux
+
+[Blinky example]: crates/fayalite/examples/blinky.rs
+
+This uses the container image containing all the external programs and files that Fayalite needs to build for FPGAs, the sources for the container image are in https://git.libre-chip.org/libre-chip/fayalite-deps
+
+Steps:
+
+Install podman (or docker).
+
+Run:
+```bash
+podman run --rm --security-opt label=disable --volume="$(pwd):$(pwd)" -w="$(pwd)" -it git.libre-chip.org/libre-chip/fayalite-deps:latest cargo run --example blinky yosys-nextpnr-xray --nextpnr-xilinx-chipdb-dir /opt/fayalite-deps/nextpnr-xilinx/xilinx --prjxray-db-dir /opt/fayalite-deps/prjxray-db --platform arty-a7-100t -o target/blinky-out
+```
+
+To actually program the FPGA, you'll need to install [openFPGALoader] on your host OS:
+
+[openFPGALoader]: https://github.com/trabucayre/openFPGALoader
+
+On Debian 12:
+```bash
+sudo apt update && sudo apt install openfpgaloader
+```
+
+Then program the FPGA:
+```bash
+sudo openFPGALoader --board arty_a7_100t target/blinky-out/blinky.bit
+```
+
+This will program the FPGA but leave the Flash chip unmodified, so the FPGA will revert when the board is power-cycled.
+
+To program the Flash also, so it stays programmed when power-cycling the board:
+
+```bash
+sudo openFPGALoader --board arty_a7_100t -f target/blinky-out/blinky.bit
+```
+
+# Building the [Transmit-only UART example] for the Arty A7 100T on Linux
+
+[Transmit-only UART example]: crates/fayalite/examples/tx_only_uart.rs
+
+Follow the steps above of building the Blinky example, but replace `blinky` with `tx_only_uart`.
+
+View the output using [tio](https://github.com/tio/tio) which you can install in Debian using `apt`.
+
+Find the correct USB device:
+```bash
+sudo tio --list
+```
+
+You want the device with a name like (note the `if01`, `if00` is presumably the JTAG port):
+`/dev/serial/by-id/usb-Digilent_Digilent_USB_Device_210319B4A51E-if01-port0`
+
+Connect to the serial port:
+```bash
+sudo tio -b115200 /dev/serial/by-id/put-your-device-id-here
+```
+
+You'll see (repeating endlessly):
+```text
+Hello World from Fayalite!!!
+Hello World from Fayalite!!!
+Hello World from Fayalite!!!
+```
+
+Press Ctrl+T then `q` to exit tio.
+
 # Funding
 
 ## NLnet Grants

crates/fayalite/examples/tx_only_uart.rs

@@ -0,0 +1,188 @@
+// SPDX-License-Identifier: LGPL-3.0-or-later
+// See Notices.txt for copyright information
+use clap::builder::TypedValueParser;
+use fayalite::{
+    build::{ToArgs, WriteArgs},
+    platform::PeripheralRef,
+    prelude::*,
+};
+use ordered_float::NotNan;
+
+fn pick_clock<'a>(
+    platform_io_builder: &PlatformIOBuilder<'a>,
+) -> PeripheralRef<'a, peripherals::ClockInput> {
+    let mut clks = platform_io_builder.peripherals_with_type::<peripherals::ClockInput>();
+    clks.sort_by_key(|clk| {
+        // sort clocks by preference, smaller return values means higher preference
+        let mut frequency = clk.ty().frequency();
+        let priority;
+        if frequency < 10e6 {
+            frequency = -frequency; // prefer bigger frequencies
+            priority = 1;
+        } else if frequency > 50e6 {
+            // prefer smaller frequencies
+            priority = 2; // least preferred
+        } else {
+            priority = 0; // most preferred
+            frequency = (frequency - 25e6).abs(); // prefer closer to 25MHz
+        }
+        (priority, NotNan::new(frequency).expect("should be valid"))
+    });
+    clks[0]
+}
+
+#[hdl_module]
+fn tx_only_uart(
+    platform_io_builder: PlatformIOBuilder<'_>,
+    divisor: f64,
+    message: impl AsRef<[u8]>,
+) {
+    let message = message.as_ref();
+    let clk_input = pick_clock(&platform_io_builder).use_peripheral();
+    let rst = platform_io_builder.peripherals_with_type::<Reset>()[0].use_peripheral();
+    let cd = #[hdl]
+    ClockDomain {
+        clk: clk_input.clk,
+        rst,
+    };
+    let numerator = 1u128 << 16;
+    let denominator = (divisor * numerator as f64).round() as u128;
+
+    #[hdl]
+    let remainder_reg: UInt<128> = reg_builder().clock_domain(cd).reset(0u128);
+
+    #[hdl]
+    let sum: UInt<128> = wire();
+    connect_any(sum, remainder_reg + numerator);
+
+    #[hdl]
+    let tick_reg = reg_builder().clock_domain(cd).reset(false);
+    connect(tick_reg, false);
+
+    #[hdl]
+    let next_remainder: UInt<128> = wire();
+    connect(remainder_reg, next_remainder);
+
+    #[hdl]
+    if sum.cmp_ge(denominator) {
+        connect_any(next_remainder, sum - denominator);
+        connect(tick_reg, true);
+    } else {
+        connect(next_remainder, sum);
+    }
+
+    #[hdl]
+    let uart_state_reg = reg_builder().clock_domain(cd).reset(0_hdl_u4);
+    #[hdl]
+    let next_uart_state: UInt<4> = wire();
+
+    connect_any(next_uart_state, uart_state_reg + 1u8);
+
+    #[hdl]
+    let message_mem: Array<UInt<8>> = wire(Array[UInt::new_static()][message.len()]);
+    for (message, message_mem) in message.iter().zip(message_mem) {
+        connect(message_mem, *message);
+    }
+    #[hdl]
+    let addr_reg: UInt<32> = reg_builder().clock_domain(cd).reset(0u32);
+    #[hdl]
+    let next_addr: UInt<32> = wire();
+    connect(next_addr, addr_reg);
+
+    #[hdl]
+    let tx = reg_builder().clock_domain(cd).reset(true);
+
+    #[hdl]
+    let tx_bits: Array<Bool, 10> = wire();
+
+    connect(tx_bits[0], false); // start bit
+    connect(tx_bits[9], true); // stop bit
+
+    for i in 0..8 {
+        connect(tx_bits[i + 1], message_mem[addr_reg][i]); // data bits
+    }
+
+    connect(tx, tx_bits[uart_state_reg]);
+
+    #[hdl]
+    if uart_state_reg.cmp_eq(Expr::ty(tx_bits).len() - 1) {
+        connect(next_uart_state, 0_hdl_u4);
+        let next_addr_val = addr_reg + 1u8;
+        #[hdl]
+        if next_addr_val.cmp_lt(message.len()) {
+            connect_any(next_addr, next_addr_val);
+        } else {
+            connect(next_addr, 0u32);
+        }
+    }
+
+    #[hdl]
+    if tick_reg {
+        connect(uart_state_reg, next_uart_state);
+        connect(addr_reg, next_addr);
+    }
+
+    for uart in platform_io_builder.peripherals_with_type::<peripherals::Uart>() {
+        connect(uart.use_peripheral().tx, tx);
+    }
+
+    #[hdl]
+    let io = m.add_platform_io(platform_io_builder);
+}
+
+fn parse_baud_rate(
+    v: impl AsRef<str>,
+) -> Result<NotNan<f64>, Box<dyn std::error::Error + Send + Sync>> {
+    let retval: NotNan<f64> = v
+        .as_ref()
+        .parse()
+        .map_err(|_| "invalid baud rate, must be a finite positive floating-point value")?;
+    if *retval > 0.0 && retval.is_finite() {
+        Ok(retval)
+    } else {
+        Err("baud rate must be finite and positive".into())
+    }
+}
+
+#[derive(Clone, PartialEq, Eq, Hash, Debug, clap::Args)]
+pub struct ExtraArgs {
+    #[arg(long, value_parser = clap::builder::StringValueParser::new().try_map(parse_baud_rate), default_value = "115200")]
+    pub baud_rate: NotNan<f64>,
+    #[arg(long, default_value = "Hello World from Fayalite!!!\r\n", value_parser = clap::builder::NonEmptyStringValueParser::new())]
+    pub message: String,
+}
+
+impl ToArgs for ExtraArgs {
+    fn to_args(&self, args: &mut (impl WriteArgs + ?Sized)) {
+        let Self { baud_rate, message } = self;
+        args.write_display_arg(format_args!("--baud-rate={baud_rate}"));
+        args.write_long_option_eq("message", message);
+    }
+}
+
+fn main() {
+    type Cli = BuildCli<ExtraArgs>;
+    Cli::main(
+        "tx_only_uart",
+        |_, platform, ExtraArgs { baud_rate, message }| {
+            Ok(JobParams::new(platform.try_wrap_main_module(|io| {
+                let clk = pick_clock(&io).ty();
+                let divisor = clk.frequency() / *baud_rate;
+                let baud_rate_error = |msg| {
+                    <Cli as clap::CommandFactory>::command()
+                        .error(clap::error::ErrorKind::ValueValidation, msg)
+                };
+                const HUGE_DIVISOR: f64 = u64::MAX as f64;
+                match divisor {
+                    divisor if !divisor.is_finite() => {
+                        return Err(baud_rate_error("bad baud rate"));
+                    }
+                    HUGE_DIVISOR.. => return Err(baud_rate_error("baud rate is too small")),
+                    4.0.. => {}
+                    _ => return Err(baud_rate_error("baud rate is too large")),
+                }
+                Ok(tx_only_uart(io, divisor, message))
+            })?))
+        },
+    );
+}

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/firrtl.rs

@@ -1883,7 +1883,11 @@ impl<'a> Exporter<'a> {
     }
     fn annotation(&mut self, path: AnnotationTargetPath, annotation: &Annotation) {
         let data = match annotation {
-            Annotation::DontTouch(DontTouchAnnotation {}) => AnnotationData::DontTouch,
+            Annotation::DontTouch(DontTouchAnnotation {}) => {
+                // TODO: error if the annotated thing was renamed because of a naming conflict,
+                // unless Target::base() is one of the ports of the top-level module since that's handled by ScalarizedModuleABI
+                AnnotationData::DontTouch
+            }
             Annotation::SVAttribute(SVAttributeAnnotation { text }) => {
                 AnnotationData::AttributeAnnotation { description: *text }
             }

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> {
-            fn cast_to(src: Expr<Self>, to_type: UInt) -> Expr<UInt> {
+        impl<Start: Size, End: Size, Width: Size> ExprCastTo<UIntType<Width>>
+            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/platform/peripherals.rs

@@ -50,3 +50,13 @@ pub struct RgbLed {
     pub g: Bool,
     pub b: Bool,
 }
+
+#[hdl]
+/// UART, used as an output from the FPGA
+pub struct Uart {
+    /// transmit from the FPGA's perspective
+    pub tx: Bool,
+    /// receive from the FPGA's perspective
+    #[hdl(flip)]
+    pub rx: Bool,
+}

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,
-        module::transform::simplify_enums::SimplifyEnumsKind, testing::assert_formal,
-        ty::StaticType,
+        firrtl::ExportOptions, module::transform::simplify_enums::SimplifyEnumsKind, ty::StaticType,
     };
     use std::num::NonZero;
 

crates/fayalite/src/vendor/xilinx/arty_a7.rs

@@ -1,25 +1,22 @@
 // SPDX-License-Identifier: LGPL-3.0-or-later
 // See Notices.txt for copyright information
 
-use std::sync::OnceLock;
-
-use ordered_float::NotNan;
-
 use crate::{
-    annotations::Annotation,
     intern::{Intern, Interned},
     module::{instance_with_loc, reg_builder_with_loc, wire_with_loc},
     platform::{
         DynPlatform, Peripheral, PeripheralRef, Peripherals, PeripheralsBuilderFactory,
         PeripheralsBuilderFinished, Platform, PlatformAspectSet,
-        peripherals::{ClockInput, Led, RgbLed},
+        peripherals::{ClockInput, Led, RgbLed, Uart},
     },
     prelude::*,
     vendor::xilinx::{
         Device, XdcCreateClockAnnotation, XdcIOStandardAnnotation, XdcLocationAnnotation,
-        primitives::{self, BUFGCE, STARTUPE2_default_inputs},
+        primitives,
     },
 };
+use ordered_float::NotNan;
+use std::sync::OnceLock;
 
 macro_rules! arty_a7_platform {
     (
@@ -69,7 +66,7 @@ arty_a7_platform! {
 
 #[derive(Debug)]
 pub struct ArtyA7Peripherals {
-    clk100: Peripheral<ClockInput>,
+    clk100_div_pow2: [Peripheral<ClockInput>; 4],
     rst: Peripheral<Reset>,
     rst_sync: Peripheral<SyncReset>,
     ld0: Peripheral<RgbLed>,
@@ -80,13 +77,14 @@ pub struct ArtyA7Peripherals {
     ld5: Peripheral<Led>,
     ld6: Peripheral<Led>,
     ld7: Peripheral<Led>,
+    uart: Peripheral<Uart>,
     // TODO: add rest of peripherals when we need them
 }
 
 impl Peripherals for ArtyA7Peripherals {
     fn append_peripherals<'a>(&'a self, peripherals: &mut Vec<PeripheralRef<'a, CanonicalType>>) {
         let Self {
-            clk100,
+            clk100_div_pow2,
             rst,
             rst_sync,
             ld0,
@@ -97,8 +95,9 @@ impl Peripherals for ArtyA7Peripherals {
             ld5,
             ld6,
             ld7,
+            uart,
         } = self;
-        clk100.append_peripherals(peripherals);
+        clk100_div_pow2.append_peripherals(peripherals);
         rst.append_peripherals(peripherals);
         rst_sync.append_peripherals(peripherals);
         ld0.append_peripherals(peripherals);
@@ -109,6 +108,7 @@ impl Peripherals for ArtyA7Peripherals {
         ld5.append_peripherals(peripherals);
         ld6.append_peripherals(peripherals);
         ld7.append_peripherals(peripherals);
+        uart.append_peripherals(peripherals);
     }
 }
 
@@ -120,6 +120,45 @@ impl ArtyA7Platform {
     }
 }
 
+#[hdl_module(extern)]
+fn reset_sync() {
+    #[hdl]
+    let clk: Clock = m.input();
+    #[hdl]
+    let inp: Bool = m.input();
+    #[hdl]
+    let out: SyncReset = m.output();
+    m.annotate_module(BlackBoxInlineAnnotation {
+        path: "fayalite_arty_a7_reset_sync.v".intern(),
+        text: r#"module __fayalite_arty_a7_reset_sync(input clk, input inp, output out);
+    wire reset_0_out;
+    (* ASYNC_REG = "TRUE" *)
+    FDPE #(
+        .INIT(1'b1)
+    ) reset_0 (
+        .Q(reset_0_out),
+        .C(clk),
+        .CE(1'b1),
+        .PRE(inp),
+        .D(1'b0)
+    );
+    (* ASYNC_REG = "TRUE" *)
+    FDPE #(
+        .INIT(1'b1)
+    ) reset_1 (
+        .Q(out),
+        .C(clk),
+        .CE(1'b1),
+        .PRE(inp),
+        .D(reset_0_out)
+    );
+endmodule
+"#
+        .intern(),
+    });
+    m.verilog_name("__fayalite_arty_a7_reset_sync");
+}
+
 impl Platform for ArtyA7Platform {
     type Peripherals = ArtyA7Peripherals;
 
@@ -132,9 +171,20 @@ impl Platform for ArtyA7Platform {
         builder_factory: PeripheralsBuilderFactory<'builder>,
     ) -> (Self::Peripherals, PeripheralsBuilderFinished<'builder>) {
         let mut builder = builder_factory.builder();
+
+        let clk100_div_pow2 = std::array::from_fn(|log2_divisor| {
+            let divisor = 1u64 << log2_divisor;
+            let name = if divisor != 1 {
+                format!("clk100_div_{divisor}")
+            } else {
+                "clk100".into()
+            };
+            builder.input_peripheral(name, ClockInput::new(100e6 / divisor as f64))
+        });
+        builder.add_conflicts(Vec::from_iter(clk100_div_pow2.iter().map(|v| v.id())));
         (
             ArtyA7Peripherals {
-                clk100: builder.input_peripheral("clk100", ClockInput::new(100e6)),
+                clk100_div_pow2,
                 rst: builder.input_peripheral("rst", Reset),
                 rst_sync: builder.input_peripheral("rst_sync", SyncReset),
                 ld0: builder.output_peripheral("ld0", RgbLed),
@@ -145,6 +195,7 @@ impl Platform for ArtyA7Platform {
                 ld5: builder.output_peripheral("ld5", Led),
                 ld6: builder.output_peripheral("ld6", Led),
                 ld7: builder.output_peripheral("ld7", Led),
+                uart: builder.output_peripheral("uart", Uart),
             },
             builder.finish(),
         )
@@ -156,7 +207,7 @@ impl Platform for ArtyA7Platform {
 
     fn add_peripherals_in_wrapper_module(&self, m: &ModuleBuilder, peripherals: Self::Peripherals) {
         let ArtyA7Peripherals {
-            clk100,
+            clk100_div_pow2,
             rst,
             rst_sync,
             ld0,
@@ -167,12 +218,9 @@ impl Platform for ArtyA7Platform {
             ld5,
             ld6,
             ld7,
+            uart,
         } = peripherals;
-        let make_buffered_input = |name: &str,
-                                   location: &str,
-                                   io_standard: &str,
-                                   additional_annotations: &[Annotation],
-                                   invert: bool| {
+        let make_buffered_input = |name: &str, location: &str, io_standard: &str, invert: bool| {
             let pin = m.input_with_loc(name, SourceLocation::builtin(), Bool);
             annotate(
                 pin,
@@ -186,7 +234,6 @@ impl Platform for ArtyA7Platform {
                     value: io_standard.intern(),
                 },
             );
-            annotate(pin, additional_annotations);
             let buf = instance_with_loc(
                 &format!("{name}_buf"),
                 primitives::IBUF(),
@@ -218,54 +265,84 @@ impl Platform for ArtyA7Platform {
             connect(buf.T, false);
             buf.I
         };
-        let clock_annotation = XdcCreateClockAnnotation {
-            period: NotNan::new(1e9 / clk100.ty().frequency()).expect("known to be valid"),
-        };
-        let clk100_buf = make_buffered_input(
-            "clk100",
-            "E3",
-            "LVCMOS33",
-            &[clock_annotation.into()],
-            false,
-        );
+        let mut frequency = clk100_div_pow2[0].ty().frequency();
+        let mut log2_divisor = 0;
+        let mut clk = None;
+        for (cur_log2_divisor, p) in clk100_div_pow2.into_iter().enumerate() {
+            let Some(p) = p.into_used() else {
+                continue;
+            };
+            debug_assert!(
+                clk.is_none(),
+                "conflict-handling logic should ensure at most one clock is used",
+            );
+            frequency = p.ty().frequency();
+            clk = Some(p);
+            log2_divisor = cur_log2_divisor;
+        }
+        let clk100_buf = make_buffered_input("clk100", "E3", "LVCMOS33", false);
         let startup = instance_with_loc(
             "startup",
-            STARTUPE2_default_inputs(),
+            primitives::STARTUPE2_default_inputs(),
             SourceLocation::builtin(),
         );
-        let clk100_sync = instance_with_loc("clk100_sync", BUFGCE(), SourceLocation::builtin());
-        connect(clk100_sync.CE, startup.EOS);
-        connect(clk100_sync.I, clk100_buf);
-        if let Some(clk100) = clk100.into_used() {
-            connect(clk100.instance_io_field().clk, clk100_sync.O);
-        }
-        let rst_buf = make_buffered_input("rst", "C2", "LVCMOS33", &[], true);
-        let rst_sync_cd = wire_with_loc(
-            "rst_sync_cd",
+        let clk_global_buf = instance_with_loc(
+            "clk_global_buf",
+            primitives::BUFGCE(),
             SourceLocation::builtin(),
-            ClockDomain[AsyncReset],
         );
-        annotate(clk100_sync.O, clock_annotation);
-        connect(rst_sync_cd.clk, clk100_sync.O);
-        connect(rst_sync_cd.rst, rst_buf.to_async_reset());
-        let [rst_sync_0, rst_sync_1] = std::array::from_fn(|index| {
-            let rst_sync =
-                reg_builder_with_loc(&format!("rst_sync_{index}"), SourceLocation::builtin())
-                    .clock_domain(rst_sync_cd)
-                    .reset(true)
-                    .build();
+        connect(clk_global_buf.CE, startup.EOS);
+        let mut clk_global_buf_in = clk100_buf.to_clock();
+        for prev_log2_divisor in 0..log2_divisor {
+            let prev_divisor = 1u64 << prev_log2_divisor;
+            let clk_in = wire_with_loc(
+                &format!("clk_div_{prev_divisor}"),
+                SourceLocation::builtin(),
+                Clock,
+            );
+            connect(clk_in, clk_global_buf_in);
             annotate(
-                rst_sync,
-                SVAttributeAnnotation {
-                    text: "ASYNC_REG = \"TRUE\"".intern(),
+                clk_in,
+                XdcCreateClockAnnotation {
+                    period: NotNan::new(1e9 / (100e6 / prev_divisor as f64))
+                        .expect("known to be valid"),
                 },
             );
-            annotate(rst_sync, DontTouchAnnotation);
-            rst_sync
-        });
-        connect(rst_sync_0, false);
-        connect(rst_sync_1, rst_sync_0);
-        let rst_value = rst_sync_1.to_sync_reset();
+            annotate(clk_in, DontTouchAnnotation);
+            let cd = wire_with_loc(
+                &format!("clk_div_{prev_divisor}_in"),
+                SourceLocation::builtin(),
+                ClockDomain[AsyncReset],
+            );
+            connect(cd.clk, clk_in);
+            connect(cd.rst, (!startup.EOS).to_async_reset());
+            let divider = reg_builder_with_loc("divider", SourceLocation::builtin())
+                .clock_domain(cd)
+                .reset(false)
+                .build();
+            connect(divider, !divider);
+            clk_global_buf_in = divider.to_clock();
+        }
+        connect(clk_global_buf.I, clk_global_buf_in);
+        let clk_out = wire_with_loc("clk_out", SourceLocation::builtin(), Clock);
+        connect(clk_out, clk_global_buf.O);
+        annotate(
+            clk_out,
+            XdcCreateClockAnnotation {
+                period: NotNan::new(1e9 / frequency).expect("known to be valid"),
+            },
+        );
+        annotate(clk_out, DontTouchAnnotation);
+        if let Some(clk) = clk {
+            connect(clk.instance_io_field().clk, clk_out);
+        }
+        let rst_value = {
+            let rst_buf = make_buffered_input("rst", "C2", "LVCMOS33", true);
+            let rst_sync = instance_with_loc("rst_sync", reset_sync(), SourceLocation::builtin());
+            connect(rst_sync.clk, clk_out);
+            connect(rst_sync.inp, rst_buf | !startup.EOS);
+            rst_sync.out
+        };
         if let Some(rst) = rst.into_used() {
             connect(rst.instance_io_field(), rst_value.to_reset());
         }
@@ -301,6 +378,14 @@ impl Platform for ArtyA7Platform {
                 connect(o, false);
             }
         }
+        let uart_tx = make_buffered_output("uart_tx", "D10", "LVCMOS33");
+        let uart_rx = make_buffered_input("uart_rx", "A9", "LVCMOS33", false);
+        if let Some(uart) = uart.into_used() {
+            connect(uart_tx, uart.instance_io_field().tx);
+            connect(uart.instance_io_field().rx, uart_rx);
+        } else {
+            connect(uart_tx, true); // idle
+        }
     }
 
     fn aspects(&self) -> PlatformAspectSet {

crates/fayalite/src/vendor/xilinx/primitives.rs

@@ -33,7 +33,7 @@ pub fn BUFGCE() {
     #[hdl]
     let CE: Bool = m.input();
     #[hdl]
-    let I: Bool = m.input();
+    let I: Clock = m.input();
 }
 
 #[hdl_module(extern)]

crates/fayalite/src/vendor/xilinx/yosys_nextpnr_prjxray.rs

@@ -2,7 +2,7 @@
 // See Notices.txt for copyright information
 
 use crate::{
-    annotations::Annotation,
+    annotations::{Annotation, TargetedAnnotation},
     build::{
         BaseJob, CommandParams, DynJobKind, GetJobPositionDependencies, GlobalParams,
         JobAndDependencies, JobArgsAndDependencies, JobDependencies, JobItem, JobItemName, JobKind,
@@ -12,12 +12,17 @@ use crate::{
         },
         verilog::{UnadjustedVerilog, VerilogDialect, VerilogJob, VerilogJobKind},
     },
-    bundle::Bundle,
+    bundle::{Bundle, BundleType},
+    expr::target::{Target, TargetBase},
     firrtl::{ScalarizedModuleABI, ScalarizedModuleABIAnnotations, ScalarizedModuleABIPort},
     intern::{Intern, InternSlice, Interned},
-    module::{Module, NameId},
-    prelude::JobParams,
-    util::job_server::AcquiredJob,
+    module::{
+        NameId, ScopedNameId, TargetName,
+        transform::visit::{Visit, Visitor},
+    },
+    prelude::*,
+    source_location::SourceLocation,
+    util::{HashSet, job_server::AcquiredJob},
     vendor::xilinx::{
         Device, XdcCreateClockAnnotation, XdcIOStandardAnnotation, XdcLocationAnnotation,
         XilinxAnnotation, XilinxArgs,
@@ -26,6 +31,7 @@ use crate::{
 use eyre::Context;
 use serde::{Deserialize, Serialize};
 use std::{
+    convert::Infallible,
     ffi::{OsStr, OsString},
     fmt::{self, Write},
     ops::ControlFlow,
@@ -370,6 +376,228 @@ fn tcl_escape(s: impl AsRef<str>) -> String {
     retval
 }
 
+#[derive(Copy, Clone, Debug)]
+enum AnnotationTarget {
+    None,
+    Module(Module<Bundle>),
+    Mem(Mem),
+    Target(Interned<Target>),
+}
+
+impl AnnotationTarget {
+    fn source_location(self) -> SourceLocation {
+        match self {
+            AnnotationTarget::None => unreachable!(),
+            AnnotationTarget::Module(module) => module.source_location(),
+            AnnotationTarget::Mem(mem) => mem.source_location(),
+            AnnotationTarget::Target(target) => target.base().source_location(),
+        }
+    }
+}
+
+struct XdcFileWriter<W: fmt::Write> {
+    output: W,
+    module_depth: usize,
+    annotation_target: AnnotationTarget,
+    dont_touch_targets: HashSet<Interned<Target>>,
+    required_dont_touch_targets: HashSet<Interned<Target>>,
+}
+
+impl<W: fmt::Write> XdcFileWriter<W> {
+    fn run(output: W, top_module: Module<Bundle>) -> Result<(), WriteXdcContentsError> {
+        let mut this = Self {
+            output,
+            module_depth: 0,
+            annotation_target: AnnotationTarget::None,
+            dont_touch_targets: HashSet::default(),
+            required_dont_touch_targets: HashSet::default(),
+        };
+        top_module.visit(&mut this)?;
+        let Self {
+            output: _,
+            module_depth: _,
+            annotation_target: _,
+            dont_touch_targets,
+            required_dont_touch_targets,
+        } = this;
+        for &target in required_dont_touch_targets.difference(&dont_touch_targets) {
+            return Err(eyre::eyre!(
+                "a DontTouchAnnotation is required since the target is also annotated with a XilinxAnnotation:\ntarget: {target:?}\nat: {}",
+                target.base().source_location(),
+            ).into());
+        }
+        Ok(())
+    }
+    fn default_visit_with<T: ?Sized + Visit<Self>>(
+        &mut self,
+        module_depth: usize,
+        annotation_target: AnnotationTarget,
+        v: &T,
+    ) -> Result<(), WriteXdcContentsError> {
+        let Self {
+            output: _,
+            module_depth: old_module_depth,
+            annotation_target: old_annotation_target,
+            dont_touch_targets: _,
+            required_dont_touch_targets: _,
+        } = *self;
+        self.module_depth = module_depth;
+        self.annotation_target = annotation_target;
+        let retval = v.default_visit(self);
+        self.module_depth = old_module_depth;
+        self.annotation_target = old_annotation_target;
+        retval
+    }
+}
+
+impl<W: fmt::Write> Visitor for XdcFileWriter<W> {
+    type Error = WriteXdcContentsError;
+
+    fn visit_targeted_annotation(&mut self, v: &TargetedAnnotation) -> Result<(), Self::Error> {
+        self.default_visit_with(self.module_depth, AnnotationTarget::Target(v.target()), v)
+    }
+
+    fn visit_module<T: BundleType>(&mut self, v: &Module<T>) -> Result<(), Self::Error> {
+        self.default_visit_with(
+            self.module_depth + 1,
+            AnnotationTarget::Module(v.canonical()),
+            v,
+        )
+    }
+
+    fn visit_mem<Element: Type, Len: Size>(
+        &mut self,
+        v: &Mem<Element, Len>,
+    ) -> Result<(), Self::Error>
+    where
+        Element: Visit<Self>,
+    {
+        self.default_visit_with(
+            self.module_depth + 1,
+            AnnotationTarget::Mem(v.canonical()),
+            v,
+        )
+    }
+
+    fn visit_dont_touch_annotation(&mut self, _v: &DontTouchAnnotation) -> Result<(), Self::Error> {
+        if let AnnotationTarget::Target(target) = self.annotation_target {
+            self.dont_touch_targets.insert(target);
+        }
+        Ok(())
+    }
+
+    fn visit_xilinx_annotation(&mut self, v: &XilinxAnnotation) -> Result<(), Self::Error> {
+        fn todo(
+            msg: &str,
+            annotation: &XilinxAnnotation,
+            source_location: SourceLocation,
+        ) -> Result<Infallible, WriteXdcContentsError> {
+            Err(WriteXdcContentsError(eyre::eyre!(
+                "{msg}\nannotation: {annotation:?}\nat: {source_location}"
+            )))
+        }
+        if self.module_depth != 1 {
+            match todo(
+                "annotations are not yet supported outside of the top module since the logic to figure out the correct name isn't implemented",
+                v,
+                self.annotation_target.source_location(),
+            )? {}
+        }
+        match self.annotation_target {
+            AnnotationTarget::None => unreachable!(),
+            AnnotationTarget::Module(module) => match v {
+                XilinxAnnotation::XdcIOStandard(_)
+                | XilinxAnnotation::XdcLocation(_)
+                | XilinxAnnotation::XdcCreateClock(_) => {
+                    return Err(WriteXdcContentsError(eyre::eyre!(
+                        "annotation not allowed on a module: {v:?}\nat: {}",
+                        module.source_location(),
+                    )));
+                }
+            },
+            AnnotationTarget::Mem(mem) => match todo(
+                "xilinx annotations are not yet supported on memories since the logic to figure out the correct name isn't implemented",
+                v,
+                mem.source_location(),
+            )? {},
+            AnnotationTarget::Target(target) => {
+                let base = target.base();
+                match *base {
+                    TargetBase::ModuleIO(_) => {
+                        // already handled by write_xdc_contents handling the main module's ScalarizedModuleABI
+                        Ok(())
+                    }
+                    TargetBase::MemPort(mem_port) => {
+                        match todo(
+                            "xilinx annotations are not yet supported on memory ports since the logic to figure out the correct name isn't implemented",
+                            v,
+                            mem_port.source_location(),
+                        )? {}
+                    }
+                    TargetBase::Reg(_)
+                    | TargetBase::RegSync(_)
+                    | TargetBase::RegAsync(_)
+                    | TargetBase::Wire(_) => {
+                        match *target {
+                            Target::Base(_) => {}
+                            Target::Child(_) => match todo(
+                                "xilinx annotations are not yet supported on parts of registers/wires since the logic to figure out the correct name isn't implemented",
+                                v,
+                                base.source_location(),
+                            )? {},
+                        }
+                        match base.canonical_ty() {
+                            CanonicalType::UInt(_)
+                            | CanonicalType::SInt(_)
+                            | CanonicalType::Bool(_)
+                            | CanonicalType::AsyncReset(_)
+                            | CanonicalType::SyncReset(_)
+                            | CanonicalType::Reset(_)
+                            | CanonicalType::Clock(_) => {}
+                            CanonicalType::Enum(_)
+                            | CanonicalType::Array(_)
+                            | CanonicalType::Bundle(_)
+                            | CanonicalType::PhantomConst(_)
+                            | CanonicalType::DynSimOnly(_) => match todo(
+                                "xilinx annotations are not yet supported on types other than integers, Bool, resets, or Clock since the logic to figure out the correct name isn't implemented",
+                                v,
+                                base.source_location(),
+                            )? {},
+                        }
+                        self.required_dont_touch_targets.insert(target);
+                        match v {
+                            XilinxAnnotation::XdcIOStandard(_)
+                            | XilinxAnnotation::XdcLocation(_) => {
+                                return Err(WriteXdcContentsError(eyre::eyre!(
+                                    "annotation must be on a ModuleIO: {v:?}\nat: {}",
+                                    base.source_location(),
+                                )));
+                            }
+                            XilinxAnnotation::XdcCreateClock(XdcCreateClockAnnotation {
+                                period,
+                            }) => {
+                                let TargetName(ScopedNameId(_, NameId(name, _)), _) =
+                                    base.target_name();
+                                writeln!(
+                                    self.output,
+                                    "create_clock -period {period} [get_nets {}]",
+                                    tcl_escape(name),
+                                )?;
+                                Ok(())
+                            }
+                        }
+                    }
+                    TargetBase::Instance(instance) => match todo(
+                        "xilinx annotations are not yet supported on instances' IO since the logic to figure out the correct name isn't implemented",
+                        v,
+                        instance.source_location(),
+                    )? {},
+                }
+            }
+        }
+    }
+}
+
 impl YosysNextpnrXrayWriteXdcFile {
     fn write_xdc_contents_for_port_and_annotations(
         &self,
@@ -426,9 +654,10 @@ impl YosysNextpnrXrayWriteXdcFile {
                 Err(e) => ControlFlow::Break(e),
             }
         }) {
-            ControlFlow::Continue(()) => Ok(()),
-            ControlFlow::Break(e) => Err(e.0),
+            ControlFlow::Continue(()) => {}
+            ControlFlow::Break(e) => return Err(e.0),
         }
+        XdcFileWriter::run(output, *top_module).map_err(|e| e.0)
     }
 }
 

crates/fayalite/tests/formal.rs

@@ -2,19 +2,7 @@
 // See Notices.txt for copyright information
 //! Formal tests in Fayalite
 
-use fayalite::{
-    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,
-};
+use fayalite::prelude::*;
 
 /// 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(),
         );
     }
 }