vj-codegen 0.1.0

//! The compiled halves of a static concurrent assertion (16.14, plan T29): the
//! property is built (`build_property`) and every Boolean/value leaf, every clock
//! tick test and every `case` label comparison is compiled to a native function
//! the engine (`sv_sim_sim::sva::engine`) calls through its `Host`.
//!
//! ## The signal row
//!
//! An assertion reads *sampled* values (16.5.1): the value a signal had at the end
//! of the previous time step. The engine therefore works on a **row**, a flat
//! array of `u128` in the accessor's fixed layout (`val` in the low 64 bits,
//! `unk` in the high 64), one entry per signal the assertion's expressions name
//! ([`AssertionSpec::row_len`]). `{name}_snap(handle, out)` fills a row from the
//! live state; every other function takes a row and reads from it, never from the
//! state, so evaluating a leaf at an old tick is a pure function of that tick's
//! row.
//!
//! ## The functions (all `extern "C"`, resolved through `CompiledPipeline`)
//!
//! * `{name}_snap(handle, out: *mut u128)`;
//! * `{name}_l{i}(handle, row: *const u128, frame: *const i64) -> i64` per leaf
//!   `i` the IR uses: a Boolean leaf is 0/1 (a leaf negated by the builder is
//!   lowered negated, `lower_negated_condition`), a value leaf the two's-complement
//!   value in 64 bits. `frame` holds the sequence local variables, indexed by
//!   `LocalVarId`. When the property calls sampled value functions the `row` of a
//!   leaf (and of a `case` function) is a *position* row: the position's own
//!   sampled row, then `history_depth` rows of previous ticks for each clock
//!   (the assertion's clocks and the sampled value functions' own, see
//!   [`AssertionSpec::hist_clocks`]), latest first, then the next global tick's
//!   row when a future function is called ([`AssertionSpec::history_depth`]); a
//!   call reads its signals' `P` cell (this tick) and `S_k` cells (`k + 1` ticks
//!   back at its clock) from them;
//! * `{name}_lv{i}(handle, row, frame) -> i64` for a leaf the engine evaluates on
//!   the live state (a `disable iff` condition, an asynchronous abort condition,
//!   16.12) that holds a sampled value function: its signals read the live
//!   state, its sampled value functions the position row;
//! * `{name}_t{c}(handle, prev_row: *const u128) -> i8` per clock `c`: whether the
//!   clock's event occurred between the previous step's end (`prev_row`) and the
//!   live state, with its `iff` condition sampled in `prev_row`;
//! * `{name}_c{k}(handle, row, frame) -> i8` per `case` (selector, label) pair
//!   ([`AssertionSpec::case_pairs`]): case equality (`===`, 12.5).
//!
//! ## What is rejected, loudly
//!
//! Anything an engine cannot evaluate faithfully: a memory of more than
//! [`MAX_MEMORY_ROW_WORDS`] row words (any other memory, of elements of any width,
//! is sampled element by element into the row and read through a local array),
//! user function calls that would read state other than their sampled arguments
//! (a pure function is compiled with the leaf, [`impure_call_reason`]), and
//! otherwise complex clocking events. The sampled value functions are executed in every
//! context (own, explicit, global and gated clocks, multiclock assertions,
//! `disable iff` and asynchronous abort conditions); `hist_sites` lists the
//! shapes still refused: a call in a clocking event's signal, or in its `iff` with no
//! clock of its own (illegal, 16.9.3; an explicitly clocked one in an `iff` runs on the
//! position row, `EngineConfig::tick_history`), and a call with no clock of
//! its own in a property-level condition of a multiclock assertion.
//!
//! ## Subroutine-call match items (16.11)
//!
//! A call attached to a sequence is not compiled here: its by-value arguments are
//! ordinary [`LeafRole::Value`] leaves (sampled like any other), and the call
//! itself is dispatched by the assertion's kernel, which gets the call table
//! through [`crate::process_lower::ProcessLoweringPlan::assertion_calls`] (set by
//! [`emit_assertions`], which therefore runs before the kernels are lowered).

use std::collections::{BTreeMap, BTreeSet, HashMap};

use inkwell::AddressSpace;
use inkwell::context::Context;
use inkwell::module::Module;
use inkwell::values::{FunctionValue, IntValue, PointerValue};
use sv_lang::kinds::{AssertionExprKind, ExpressionKind, SymbolKind, TimingControlKind};
use sv_lang::{
    AssertionKind, Design, Expression, ProceduralBlockKind, SemNode, Statement, Symbol, SyntaxTree,
    TimingControl,
};
use sv_sim_sim::sva::engine::{AssertKind, live_leaves};
use sv_sim_sim::sva::ir::{
    CallArg, ClockId, LeafId, LocalVarDecl, LocalVarId, ThreadStateId, Transition,
};
use sv_sim_sim::sva::property::{Prop, PropertyIr};
use sv_sim_sim::sva::sampled::{
    ClockEvent, SampledCall, assertion_clock_event_of, decode, n_id, p_id, s_id,
    strict_site_signals_in,
};
use sv_sim_sim::symid::{SymbolId, SymbolUid};

use crate::accessor::{AccessorFns, build_fixed_to_packed, build_get_scalar_raw};
use crate::error::LoweringError;
use crate::expr::{
    LowerCtx, LoweredValue, MemAccessorCtx, lower_condition, lower_expr, lower_negated_condition,
};
use crate::module::static_assertion_statement;
use crate::ops::{OpBuilder, is_definitely_false, is_definitely_true};
use crate::process_lower::{
    ProcessLoweringPlan, SignalSlot, SignalSlotClass, collect_named_value_symbols, mem_signals_of,
    vif_candidates,
};
use crate::sampled::{edge_occurred, same_value};
use crate::sva::build::{LeafTable, LimbSel, is_inferred_clock_event, property::build_property_as};
use crate::sva::disable::{
    DefaultDisable, TermPred, resolve_checker_default_disable, resolve_default_disable,
};
use crate::sva::proc::{CaptureItem, capture_items, first_non_captured_read, items_used_by};
pub use crate::sva::proc::{HostedAssertion, assertion_key, queued_assertion_key};
use crate::value::{PackedValue, ValueRepr};

/// How the IR uses a leaf.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum LeafRole {
    /// A Boolean condition (an edge guard, `if`, an abort or the disable
    /// condition).
    Bool,
    /// A value (a `case` selector or label, a local variable initialiser).
    Value,
    /// The IR never evaluates it.
    Unused,
}

/// `extern "C" fn(handle, out: *mut u128)`: fills a signal row.
pub type SnapFn = extern "C" fn(sv_sim_abi::SimHandle, *mut u128);
/// `extern "C" fn(handle, row, frame) -> i64`: a leaf's value.
pub type LeafFn = extern "C" fn(sv_sim_abi::SimHandle, *const u128, *const i64) -> i64;
/// `extern "C" fn(handle, prev_row) -> u8`: whether a clock ticked.
pub type TickFn = extern "C" fn(sv_sim_abi::SimHandle, *const u128) -> u8;
/// `extern "C" fn(handle, row, frame) -> u8`: a `case` label match.
pub type CaseFn = extern "C" fn(sv_sim_abi::SimHandle, *const u128, *const i64) -> u8;

/// Refuses `plans` that hold a static concurrent assertion: the entry points that
/// cannot run the engine (AOT objects, the template-deduplicating compile) must
/// not silently drop one.
pub(crate) fn reject_static_assertions(
    plans: &[ProcessLoweringPlan<'_>],
    at: &str,
) -> Result<(), LoweringError> {
    for plan in plans {
        if plan.hosted_assertion.is_some()
            || plan.fn_sym.kind() == SymbolKind::ProceduralBlock
                && plan.fn_sym.procedural_block_procedure_kind() == ProceduralBlockKind::Always
                && sv_sim_sim::process::cfg::proc_body(&plan.fn_sym)
                    .and_then(static_assertion_statement)
                    .is_some()
        {
            return Err(LoweringError::unsupported(
                "a concurrent assertion needs the assertion engine of `sv-sim run`; it is not \
                 supported in this build mode",
                at,
            ));
        }
    }
    Ok(())
}

/// A subroutine call of a sequence that runs as a process of its own (16.11):
/// the call's index (its fired term is `2 + call`), the fork-branch kernel the
/// process runs, its frame size and its start pc.
#[derive(Clone, Debug)]
pub struct SpawnCallSpec {
    pub call: u32,
    pub kernel: String,
    pub frame_words: u32,
    pub entry_pc: u32,
}

/// Everything the runtime needs to drive one static concurrent assertion.
#[derive(Clone, Debug)]
pub struct AssertionSpec {
    /// The index of the assertion's process among the plans.
    pub plan_index: usize,
    /// The symbol prefix of the assertion's functions.
    pub name: String,
    pub kind: AssertKind,
    pub ir: PropertyIr,
    pub n_clocks: usize,
    /// Per leaf, the local variables its expression reads.
    pub leaf_reads: Vec<Vec<LocalVarId>>,
    /// Per leaf, the target of a plain assignment match item (`v = e`): its slot
    /// is handed to the kernel but need not be assigned (see
    /// `EngineConfig::leaf_writes`).
    pub leaf_writes: Vec<Option<LocalVarId>>,
    pub roles: Vec<LeafRole>,
    /// The number of signals in a row.
    pub row_len: usize,
    /// The `case` (selector, label) pairs, in the order of the `_c{k}` functions.
    pub case_pairs: Vec<(LeafId, LeafId)>,
    /// `$sformatf`-free label for diagnostics: the assertion's source name.
    pub label: String,
    /// A procedural assertion (16.14.6): attempts begin only for the instances
    /// the process queues, not at every clock tick.
    pub activated: bool,
    /// The local-variable slot of each value an instance captures (automatic
    /// variables and `const'(expr)`s, [`crate::sva::proc::capture_items`]), in
    /// the order the queue call lists them.
    pub captured: Vec<LocalVarId>,
    /// The `disable iff` condition reads captured values AND signals (16.12,
    /// 16.14.6.1): it is judged against the live signals per attempt
    /// (`EngineConfig::disable_mixed`).
    pub disable_mixed: bool,
    /// A clocking event's `iff` calls a sampled value function: the tick
    /// functions get the position row (`EngineConfig::tick_history`).
    pub tick_history: bool,
    /// How many previous ticks' rows the sampled value functions of the property
    /// read (`$rose` 1, `$past(x, n)` n, `$sampled` 0). The leaf and `case` functions
    /// take a row of `(1 + (n_clocks + hist_clocks) * history_depth + future) *
    /// row_len` entries: the position's own row, then for each clock the rows of
    /// its previous ticks, latest first, then the next global tick's row when
    /// `future`
    /// (`sv_sim_sim::sva::engine::EngineConfig::history_depth`).
    pub history_depth: usize,
    /// The assertion control registry's description of the assertion (20.11),
    /// `None` for a `restrict`, which no control task reaches.
    pub site: Option<sv_sim_sim::sched::assert_control::SiteDesc>,
    /// For the watcher of a sequence instance a procedure reads the end point
    /// of (`sv_sim_sim::sva::endpoint`): the slot of its cell, which a match
    /// stamps (no action block runs). `None` for an assertion.
    pub end_cell: Option<u32>,
    /// The property calls a global clocking future function (16.9.4): its
    /// position rows end with the next tick's row
    /// (`sv_sim_sim::sva::engine::EngineConfig::future`).
    pub future: bool,
    /// The clocks past [`n_clocks`](Self::n_clocks) the sampled value functions
    /// sample at (an explicit clocking event, the global clock, a `$past`
    /// gate): `{name}_t{n_clocks + j}` tests the `j`th. The position rows carry
    /// `(n_clocks + hist_clocks) * history_depth` history rows
    /// (`sv_sim_sim::sva::engine::EngineConfig::hist_clocks`).
    pub hist_clocks: usize,
    /// The clock (an index into all `n_clocks + hist_clocks`) whose next tick
    /// the future functions read (`EngineConfig::future_clock`).
    pub future_clock: u32,
    /// The leaves the engine evaluates on the live state (the `disable iff` and
    /// asynchronous abort conditions, sampled value functions or not): each has a `{name}_lv{i}` function taking the live
    /// state as its row and the history from a position row (16.12).
    pub live_calls: Vec<u32>,
    /// The active free checker variables (17.7.2) in the row: their id, first
    /// row word and word count. Their sampled value is the current one, so the
    /// runner refreshes these words when the variables are randomized.
    pub current_words: Vec<(SymbolId, usize, usize)>,
    /// The row words of clock variables with an explicit input skew (`#0`,
    /// `#N`; 14.4, 16.18): their sampled value is the block's own sample, which
    /// exists only once its sampler ran, so the runner refreshes these words
    /// from the live cells when the assertion fires (first word, word count).
    pub observed_words: Vec<(usize, usize)>,
    /// The row words holding a queue, dynamic array or associative array
    /// handle: the runner replaces each by an immutable snapshot of the
    /// collection when it samples the row, so a read of the collection (and a
    /// local variable assigned from it) sees the Preponed value (16.5.1)
    /// whatever the design does to the live collection afterwards.
    pub coll_words: Vec<usize>,
    /// Per `coll_words` entry, where the collections inside its elements sit
    /// (a queue of queues, a struct element with a queue field): the runner
    /// snapshots those by value too.
    pub coll_nests: Vec<sv_sim_sim::collections::Nest>,
    /// The match-item calls that run as processes of their own
    /// ([`crate::sva::actions::CallSite::spawns`]), each with the kernel the
    /// pipeline compiled for it (empty until `build_pipeline` has).
    pub spawn_calls: Vec<SpawnCallSpec>,
    /// The source offset of the assertion statement (`None` for a watcher):
    /// with `site.scope`, what a VPI assertion object is matched by.
    pub src_offset: Option<u64>,
    /// Per leaf, its expression's source range `(buffer, start, end)` (VPI
    /// assertion stepping and `failExpr`, 39.4.2: what the engine's leaf
    /// reads are reported as).
    pub leaf_src: Vec<(u32, u64, u64)>,
}

fn unsupported(plan: &ProcessLoweringPlan<'_>, what: &str) -> LoweringError {
    LoweringError::unsupported_at(what, &plan.fn_sym)
}

/// The kind of an assertion statement, or the reason it is not a static
/// concurrent assertion this module runs.
fn assert_kind(
    plan: &ProcessLoweringPlan<'_>,
    stmt: Statement<'_>,
) -> Result<AssertKind, LoweringError> {
    match stmt.assertion_kind() {
        Some(AssertionKind::Assert) => Ok(AssertKind::Assert),
        Some(AssertionKind::Assume) => Ok(AssertKind::Assume),
        Some(AssertionKind::CoverProperty) => Ok(AssertKind::CoverProperty),
        Some(AssertionKind::CoverSequence) => Ok(AssertKind::CoverSequence),
        Some(AssertionKind::Restrict) => Ok(AssertKind::Restrict),
        // 16.17: hosted like a procedural assertion; the blocked process runs
        // its pass/fail statements itself.
        Some(AssertionKind::Expect) => Ok(AssertKind::Expect),
        None => Err(unsupported(plan, "a concurrent assertion of unknown kind")),
    }
}

/// The event of the default clocking block (14.12) in effect for `scope`, an
/// assertion's host block, if any. The lookup climbs the LEXICAL scope chain
/// (`default_clocking_of`), not the flattened member list of the instance: a
/// checker's members are merged into its host instance, so a checker that
/// redefines its default clocking ("Explicitly redefines its default values",
/// 17.2) and a checker that inherits the host's must each find their own.
fn default_clocking_event<'d>(
    scope: &Symbol<'d>,
    tree: &SyntaxTree,
) -> Result<Option<SemNode<'d>>, LoweringError> {
    let found = sv_sim_sim::state::default_clocking_of(scope, tree).map_err(|e| {
        LoweringError::unsupported_at(&format!("default clocking (LRM 14.12): {e:?}"), scope)
    })?;
    Ok(found.and_then(|cb| cb.clocking_block_event()))
}

/// Per leaf, how the IR uses it; a leaf used both ways is an internal error.
fn leaf_roles(
    plan: &ProcessLoweringPlan<'_>,
    ir: &PropertyIr,
    n_leaves: usize,
) -> Result<Vec<LeafRole>, LoweringError> {
    let mut roles = vec![LeafRole::Unused; n_leaves];
    let mut set = |l: LeafId, r: LeafRole| -> Result<(), LoweringError> {
        let slot = &mut roles[l.0 as usize];
        if *slot != LeafRole::Unused && *slot != r {
            return Err(unsupported(
                plan,
                "internal error: an assertion leaf is used both as a condition and as a value",
            ));
        }
        *slot = r;
        Ok(())
    };
    // The automaton and, recursively, the instances its end-point methods test
    // (their leaves are evaluated by the same engine).
    let mut stack = vec![&ir.automaton];
    while let Some(a) = stack.pop() {
        stack.extend(a.end_points.iter().map(|ep| &ep.automaton));
        for state in &a.states {
            for edge in &state.edges {
                if let Some(g) = edge.guard {
                    set(g, LeafRole::Bool)?;
                }
                match &edge.label {
                    Transition::Abort { leaf, .. } => set(*leaf, LeafRole::Bool)?,
                    Transition::LocalVarWrite { value, .. } => set(*value, LeafRole::Value)?,
                    // A by-value argument is the sampled value of its expression.
                    Transition::SubroutineCall { args, .. } => {
                        for arg in args {
                            if let CallArg::Value(l) = arg {
                                set(*l, LeafRole::Value)?;
                            }
                        }
                    }
                    // The instance's status: no leaf of its own.
                    Transition::EndPoint { .. }
                    | Transition::Delay { .. }
                    | Transition::Epsilon
                    | Transition::Match { .. }
                    | Transition::LocalVarCopy { .. }
                    | Transition::FirstMatchBegin { .. }
                    | Transition::FirstMatchEnd { .. }
                    | Transition::LocalVarStep { .. }
                    | Transition::ClockSync { .. } => {}
                }
            }
        }
    }
    for p in &ir.props {
        match p {
            Prop::If { cond, .. } | Prop::Abort { cond, .. } => set(*cond, LeafRole::Bool)?,
            Prop::Case { selector, arms, .. } => {
                set(*selector, LeafRole::Value)?;
                for arm in arms {
                    for l in &arm.labels {
                        set(*l, LeafRole::Value)?;
                    }
                }
            }
            Prop::Let { writes, .. } => {
                for (_, l) in writes {
                    set(*l, LeafRole::Value)?;
                }
            }
            Prop::Call { args, inits, .. } => {
                for (_, l) in args.iter().chain(inits) {
                    set(*l, LeafRole::Value)?;
                }
            }
            Prop::Seq { .. }
            | Prop::Not(_)
            | Prop::And(..)
            | Prop::Or(..)
            | Prop::Implication { .. }
            | Prop::Nexttime { .. }
            | Prop::Always { .. }
            | Prop::Eventually { .. }
            | Prop::Until { .. }
            | Prop::Clocked { .. } => {}
        }
    }
    if let Some(d) = ir.disable {
        set(d, LeafRole::Bool)?;
    }
    Ok(roles)
}

/// The signal an input clock variable `sym` (`cb.a`) of a clocking block is
/// read from in the row of an assertion whose clocking events are `clocks`:
/// the signal it samples. LRM 16.18: "If a variable used in a concurrent
/// assertion is a clocking block variable, it will be sampled only in the
/// clocking block", i.e. at the block's clocking event, with the default
/// `#1step` input skew -- the Preponed value of the signal, the very value the
/// assertion's own sampling reads when the assertion is clocked by that event.
/// The clock variable's cell is written by the block's sampler after the
/// Preponed region, so reading it would lag a cycle behind.
///
/// `None` when the row should hold the clock variable's own cell: `sym` is not
/// a clock variable, or its block's event is none of the assertion's clocks (the
/// cell then holds the value of the block's last event, which is the right
/// value at any other clock's tick).
fn clock_var_source<'d>(
    plan: &ProcessLoweringPlan<'d>,
    sym: &Symbol<'d>,
    clocks: &[SemNode<'d>],
) -> Result<Option<SignalSlot>, LoweringError> {
    if sym.kind() != SymbolKind::ClockVar {
        return Ok(None);
    }
    let Some(cb) = sym.parent() else {
        return Ok(None);
    };
    let Some(event) = cb.clocking_block_event() else {
        return Ok(None);
    };
    let same = clocks
        .iter()
        .filter(|c| super::build::events_equivalent(**c, event))
        .count();
    if same == 0 {
        return Ok(None);
    }
    // In a multiclocked assertion where only some clocks are the block's own, a
    // `#1step` variable is the signal's Preponed value at the block's ticks and
    // the block's last sample (its own cell) at the other clocks' (16.18): the
    // row carries both ([`mixed_clock_var`]) and a leaf picks by its domain. A
    // skewed one (`#0`/`#N`) has its block-tick words refreshed at the Observed
    // region; the other clocks' leaves read the block's last sample.
    // `#N` reads the variable's own cell, refreshed at the Observed region.
    let skew = clock_var_skew(sym, &cb);
    if skew == InputSkew::Delayed {
        return Ok(None);
    }
    let Some(source) = sym
        .initializer()
        .filter(|e| sv_sim_sim::symid::is_value_name(e.kind()))
        .and_then(|e| e.referenced_symbol())
    else {
        return Ok(None);
    };
    Ok(plan.signals.get(&source.uid()).copied())
}

/// The row id under which a mixed-clock clock variable's own cell (the block's
/// last sample) sits beside its source signal's Preponed value (`row_signals`).
fn block_sample_id(id: &SymbolId) -> SymbolId {
    id.derive("cbs")
}

/// The kind of input skew of a clock variable (14.4), as the block's sampler
/// reads it (`sv-sim-bin`'s `input_skew`: an edge skew has no sampling time and
/// falls back to its delay, else `#1step`).
#[derive(Clone, Copy, PartialEq, Eq)]
enum InputSkew {
    /// `#1step` or none: the Preponed value, the assertion's own sample.
    Preponed,
    /// `#0`: the value of the source signal in the Observed region.
    Zero,
    /// `#N`: the block's own sample cell (written at the clock event).
    Delayed,
}

/// The variable's own skew, else the block's `default input` (14.4).
fn clock_var_skew<'d>(sym: &Symbol<'d>, cb: &Symbol<'d>) -> InputSkew {
    let mut skew = sym.clock_var_input_skew();
    if !skew.has_value() {
        skew = cb.clocking_block_default_input_skew();
    }
    let Some(tc) = skew.delay.and_then(|n| n.as_timing_control()) else {
        return InputSkew::Preponed;
    };
    if tc.kind() != sv_lang::kinds::TimingControlKind::Delay {
        return InputSkew::Preponed;
    }
    let zero = tc
        .children()
        .into_iter()
        .find_map(|n| n.as_expression())
        .and_then(|e| e.constant_value())
        .is_some_and(|cv| match &cv {
            sv_lang::ConstantValue::Real(f) => *f == 0.0,
            other => other.as_integer().and_then(|i| i.as_i64()) == Some(0),
        });
    if zero {
        InputSkew::Zero
    } else {
        InputSkew::Delayed
    }
}

/// Whether `sym` is a clock variable of a block whose event is one of the
/// assertion's `clocks` and whose input skew is not the Preponed sample (`#0`
/// or `#N`; 14.4): its row words are refreshed at the Observed region (SA-004).
fn is_skewed_clock_var<'d>(sym: &Symbol<'d>, clocks: &[SemNode<'d>]) -> bool {
    if sym.kind() != SymbolKind::ClockVar {
        return false;
    }
    let Some(cb) = sym.parent() else {
        return false;
    };
    let Some(event) = cb.clocking_block_event() else {
        return false;
    };
    clocks
        .iter()
        .any(|c| super::build::events_equivalent(*c, event))
        && clock_var_skew(sym, &cb) != InputSkew::Preponed
}

/// An assertion's signal row: each signal and its slot, in row order.
type Row = Vec<(SymbolId, SignalSlot)>;

/// A clock variable read in a multiclocked assertion where only some clocks are
/// its block's event: the row carries its source's Preponed value under `id` and
/// the block's last sample under `sample`; a leaf whose clock is not `event`
/// reads the latter (16.18).
struct MixedClockVar<'d> {
    id: SymbolId,
    sample: SymbolId,
    event: SemNode<'d>,
}

/// [`row_signals`]' result: the row, its free and Observed-refreshed ids, and
/// the mixed-clock clock variables.
type RowParts<'d> = (
    Row,
    BTreeSet<SymbolId>,
    BTreeSet<SymbolId>,
    Vec<MixedClockVar<'d>>,
    BTreeMap<SymbolId, sv_sim_sim::collections::Nest>,
);

/// The block event of clock variable `sym` when some but not all of `clocks`
/// are it (the shape [`clock_var_source`] serves with two row entries).
fn mixed_clock_var<'d>(sym: &Symbol<'d>, clocks: &[SemNode<'d>]) -> Option<SemNode<'d>> {
    if sym.kind() != SymbolKind::ClockVar {
        return None;
    }
    let event = sym.parent()?.clocking_block_event()?;
    let same = clocks
        .iter()
        .filter(|c| super::build::events_equivalent(**c, event))
        .count();
    (same > 0 && same < clocks.len()).then_some(event)
}

/// The module signals `exprs` name, in a deterministic order, with their slots.
/// `clocks` are the clocking events of the assertion (see [`clock_var_source`]).
fn row_signals<'d>(
    plan: &ProcessLoweringPlan<'d>,
    exprs: &[Expression<'d>],
    extra: &[Symbol<'d>],
    clocks: &[SemNode<'d>],
    watcher_ids: &[SymbolId],
) -> Result<RowParts<'d>, LoweringError> {
    let mut mixed: Vec<MixedClockVar<'d>> = Vec::new();
    let mut free = BTreeSet::new();
    let mut observed = BTreeSet::new();
    let mut colls = BTreeMap::new();
    let mut found: Vec<Symbol<'d>> = extra.to_vec();
    for e in exprs {
        collect_named_value_symbols(e.as_sem_node(), &mut found);
        let mut stack = vec![e.as_sem_node()];
        while let Some(n) = stack.pop() {
            if let Some(x) = n.as_expression() {
                found.extend(vif_candidates(&x));
            }
            stack.extend(sv_sim_sim::process::cfg::live_children(&n));
        }
    }
    let mut by_id: BTreeMap<SymbolId, SignalSlot> = BTreeMap::new();
    for sym in found {
        let id = sym.uid();
        let Some(info) = plan.signals.get(&id) else {
            continue;
        };
        if sv_sim_sim::netlist::free_var_kind(&sym)
            == Some(sv_sim_sim::netlist::FreeVarKind::Active)
        {
            free.insert(id.clone());
        }
        match info.class {
            // A wide signal takes several row words ([`row_words`]).
            SignalSlotClass::Inline | SignalSlotClass::Wide => {}
            // Every element takes a row word per 64 bits ([`MAX_MEMORY_ROW_WORDS`]).
            SignalSlotClass::Memory { num_rows, .. } => {
                if row_words(info) > MAX_MEMORY_ROW_WORDS {
                    return Err(unsupported(
                        plan,
                        &format!(
                            "the memory `{}` in a concurrent assertion has {num_rows} elements \
                             of {} bits: every element is sampled at every step (16.5.1), so \
                             only memories of at most {MAX_MEMORY_ROW_WORDS} 64-bit row words \
                             are executable",
                            sym.name(),
                            info.width
                        ),
                    ));
                }
            }
        }
        // The clock variable's row entry is its source signal's slot (shadowed
        // under the clock variable's id), so a leaf reading `cb.a` evaluates the
        // Preponed value; the widths agree because the clock variable has the
        // type of the signal it samples.
        if is_skewed_clock_var(&sym, clocks) {
            observed.insert(id.clone());
        }
        if sym
            .declared_type()
            .is_some_and(|t| sv_sim_sim::state::storage::is_collection(&t))
        {
            let nest = sym
                .declared_type()
                .and_then(|t| super::build::collection_nest(&t))
                .ok_or_else(|| {
                    unsupported(
                        plan,
                        &format!(
                            "the collection `{}` read by a concurrent assertion has class-handle \
                             elements that its sampled snapshot cannot copy by value",
                            sym.name()
                        ),
                    )
                })?;
            colls.insert(id.clone(), nest);
        }
        let slot = match clock_var_source(plan, &sym, clocks)? {
            Some(src) if src.width == info.width && src.signed == info.signed => src,
            _ => *info,
        };
        if let Some(event) = mixed_clock_var(&sym, clocks) {
            let sample = block_sample_id(&id);
            by_id.insert(sample.clone(), *info);
            mixed.push(MixedClockVar {
                id: id.clone(),
                sample,
                event,
            });
        }
        by_id.insert(id, slot);
    }
    // The end-point watcher cells of the sequences used as clocks (16.5.2).
    for id in watcher_ids {
        if let Some(info) = plan.signals.get(id) {
            by_id.insert(id.clone(), *info);
        }
    }
    Ok((by_id.into_iter().collect(), free, observed, mixed, colls))
}

/// Whether the clocking event `ev` is a sequence instance (`@seq`, LRM 16.5.2).
fn is_sequence_clock(ev: &ClockEvent<'_>) -> bool {
    ev.signal.kind() == ExpressionKind::AssertionInstance
}

/// The id of the watcher cell of the sequence clock `ev` (16.5.2): stamped by
/// the sequence's watcher engine at each end point, it is the clock's
/// "signal". Not available to a hosted (procedural) assertion, whose
/// watchers are the enclosing block's.
fn sequence_clock_id(
    plan: &ProcessLoweringPlan<'_>,
    ev: &ClockEvent<'_>,
) -> Result<SymbolId, LoweringError> {
    let id = sv_sim_sim::sva::endpoint::watcher_id(&plan.fn_sym.uid(), &ev.signal);
    if plan.hosted_assertion.is_some_and(|h| h.instance.is_some())
        || !plan.signals.contains_key(&id)
    {
        return Err(unsupported(
            plan,
            "a sequence instance as the clocking event (`@seq`, LRM 16.5.2) of a procedural \
             concurrent assertion of a checker (the watcher belongs to the procedure that \
             writes the clock)",
        ));
    }
    Ok(id)
}

/// [`AssertionSpec::current_words`] of a row; with `observed` ids,
/// [`AssertionSpec::observed_words`].
fn active_free_words(
    row: &[(SymbolId, SignalSlot)],
    free: &BTreeSet<SymbolId>,
) -> Vec<(SymbolId, usize, usize)> {
    active_free_words_of(row, free.iter())
}

fn active_free_words_of<'a>(
    row: &[(SymbolId, SignalSlot)],
    free: impl Iterator<Item = &'a SymbolId>,
) -> Vec<(SymbolId, usize, usize)> {
    let free: BTreeSet<&SymbolId> = free.collect();
    let mut out = Vec::new();
    let mut base = 0;
    for (id, info) in row {
        if free.contains(id) {
            out.push((id.clone(), base, row_words(info)));
        }
        base += row_words(info);
    }
    out
}

/// Per leaf, the local-variable declarations of the automaton whose edges use
/// it: the top automaton's, or an end-point instance's (whose frame extends the
/// enclosing one with slots of its own, `ir::EndPoint::automaton`).
fn leaf_owner_decls(ir: &PropertyIr, n_leaves: usize) -> Vec<Option<Vec<LocalVarDecl>>> {
    let mut out: Vec<Option<Vec<LocalVarDecl>>> = vec![None; n_leaves];
    let mut stack = vec![&ir.automaton];
    while let Some(a) = stack.pop() {
        stack.extend(a.end_points.iter().map(|ep| &ep.automaton));
        let mut own = |l: LeafId| {
            if let Some(slot) = out.get_mut(l.0 as usize)
                && slot.is_none()
            {
                *slot = Some(a.local_vars.clone());
            }
        };
        for edge in a.states.iter().flat_map(|s| &s.edges) {
            if let Some(g) = edge.guard {
                own(g);
            }
            match &edge.label {
                Transition::Abort { leaf, .. } => own(*leaf),
                Transition::LocalVarWrite { value, .. } => own(*value),
                Transition::SubroutineCall { args, .. } => {
                    for arg in args {
                        if let CallArg::Value(l) = arg {
                            own(*l);
                        }
                    }
                }
                Transition::EndPoint { .. }
                | Transition::Delay { .. }
                | Transition::Epsilon
                | Transition::Match { .. }
                | Transition::LocalVarCopy { .. }
                | Transition::FirstMatchBegin { .. }
                | Transition::FirstMatchEnd { .. }
                | Transition::LocalVarStep { .. }
                | Transition::ClockSync { .. } => {}
            }
        }
    }
    out
}

/// The most row words (one per 64 bits of an element) of a memory an assertion
/// samples. The row of every step holds all of them (an element read is
/// `mem[idx]` with a sampled index, so any element may be needed) and the engine
/// keeps a window of rows, so the cap keeps a row small (16 MiB).
const MAX_MEMORY_ROW_WORDS: usize = 1 << 20;

/// The most elements of a memory whose shadow array is filled by unrolled stores;
/// a larger memory is filled by a loop.
const UNROLLED_MEMORY_ROWS: u32 = 16;

/// The row words signal `info` takes: one per 64 bits of a wide signal (the
/// value's bits in the low half of each `u128`, the unknown plane's in the
/// high half), one for a narrow signal (its packed 4-state value), one per
/// 64 bits of every element of a memory ([`MAX_MEMORY_ROW_WORDS`] at most).
fn row_words(info: &SignalSlot) -> usize {
    match info.class {
        SignalSlotClass::Wide => info.width.div_ceil(64) as usize,
        SignalSlotClass::Memory { num_rows, .. } => num_rows as usize * elem_words(info),
        SignalSlotClass::Inline => 1,
    }
}

/// The row words one element of a memory takes: one per 64 bits of the element
/// (laid out like a wide signal's words), at least one.
fn elem_words(info: &SignalSlot) -> usize {
    info.width.div_ceil(64).max(1) as usize
}

/// The system functions a function called from an assertion expression may use:
/// the ones whose value depends on their arguments alone (constant, bit and
/// array queries, the math functions and the conversions, 20.5 to 20.8). A
/// system task or any other system function (`$display`, `$random`, `$time`,
/// `$fopen`, ...) has a side effect or reads state of its own.
const PURE_SYSTEM_FUNCTIONS: &[&str] = &[
    "clog2",
    "bits",
    "signed",
    "unsigned",
    "countones",
    "countbits",
    "onehot",
    "onehot0",
    "isunknown",
    "ln",
    "log10",
    "exp",
    "sqrt",
    "pow",
    "floor",
    "ceil",
    "sin",
    "cos",
    "tan",
    "asin",
    "acos",
    "atan",
    "atan2",
    "hypot",
    "sinh",
    "cosh",
    "tanh",
    "asinh",
    "acosh",
    "atanh",
    "itor",
    "rtoi",
    "realtobits",
    "bitstoreal",
    "shortrealtobits",
    "bitstoshortreal",
    "low",
    "high",
    "left",
    "right",
    "size",
    "increment",
    "dimensions",
    "unpacked_dimensions",
];

/// Why a call to the user function `callee` cannot run on an assertion's sampled
/// row, `None` when it can. The arguments of an assertion's expressions are
/// sampled values (16.5.1), and the function sees nothing else: the call is
/// executable exactly when the function's value is a function of its arguments
/// alone, which is what 16.6 asks of it ("functions shall be automatic (or
/// preserve no state information) and have no side effects"; the leaf validator
/// has already refused the static ones and the output/inout/ref formals). So the
/// function (and every function it calls) must
/// - be a plain function with a body (not a DPI import, a class method or a call
///   through a virtual interface),
/// - take its arguments by value, as packed or real values,
/// - read and keep no module state (no module signal or memory, no `static`
///   variable of its own), and
/// - call no system subroutine but the pure ones ([`PURE_SYSTEM_FUNCTIONS`]).
fn impure_call_reason<'d>(call: Expression<'d>) -> Option<String> {
    if sv_sim_sim::netlist::vif::call_targets(&call).is_some() || call.call_this_class().is_some() {
        return Some("it is a method call".into());
    }
    let callee = call.call_subroutine()?;
    let mut seen: BTreeSet<SymbolId> = BTreeSet::new();
    let mut work = vec![callee];
    while let Some(sub) = work.pop() {
        if !seen.insert(sub.uid()) {
            continue;
        }
        let name = sub.name();
        if sub
            .subroutine_flags()
            .contains(sv_lang::MethodFlags::DPI_IMPORT)
        {
            return Some(format!("`{name}` is a DPI import"));
        }
        if sub.parent().is_some_and(|p| {
            matches!(
                p.kind(),
                SymbolKind::ClassType | SymbolKind::GenericClassDef
            )
        }) {
            return Some(format!("`{name}` is a class method"));
        }
        let Some(body) = sv_sim_sim::process::cfg::proc_body(&sub) else {
            return Some(format!("`{name}` has no body"));
        };
        let value_type = |t: Option<sv_lang::Type<'d>>| {
            t.is_some_and(|t| (t.is_integral() || t.is_floating()) && !t.is_void())
        };
        if !sub
            .subroutine_return_type()
            .is_some_and(|t| t.is_void() || t.is_integral() || t.is_floating())
        {
            return Some(format!(
                "`{name}` returns a type other than a packed or real value"
            ));
        }
        for formal in sub.subroutine_arguments() {
            if crate::func::is_by_reference(&formal) && !crate::func::is_const_ref(&formal) {
                return Some(format!(
                    "its formal `{}` is passed by reference (`ref`/`output`/`inout`)",
                    formal.name()
                ));
            }
            if !value_type(formal.value_type()) {
                return Some(format!(
                    "its formal `{}` is not a packed or real value",
                    formal.name()
                ));
            }
        }
        let mut stack = vec![body.as_sem_node()];
        while let Some(n) = stack.pop() {
            if let Some(x) = n.as_expression()
                && x.kind() == ExpressionKind::Call
            {
                if x.is_system_call() == Some(true) {
                    let sys = x.system_subroutine().map(|s| s.name()).unwrap_or_default();
                    if !PURE_SYSTEM_FUNCTIONS.contains(&sys.trim_start_matches('$')) {
                        return Some(format!(
                            "`{name}` calls `{sys}`, which is not a pure function of its \
                             arguments"
                        ));
                    }
                } else {
                    work.extend(crate::func::user_callees(&x));
                }
            }
            // A constant `if` runs one arm (12.4): the dead one (`else $error(...)`
            // behind a parameter test) is never lowered, so it is not walked.
            if let Some(s) = n.as_statement()
                && let Some(taken) = sv_sim_sim::process::cfg::constant_if_arm(&s)
            {
                let live = if taken {
                    s.then_branch()
                } else {
                    s.else_branch()
                };
                stack.extend(live.map(|l| l.as_sem_node()));
                continue;
            }
            stack.extend(sv_sim_sim::process::cfg::live_children(&n));
        }
    }
    let abi = crate::func::subroutine_abi(&callee);
    // A static function's formal is rewritten from the (sampled) actual by every
    // call: it preserves no state (16.6).
    if let Some(sig) = abi
        .signals
        .iter()
        .find(|s| s.kind() != SymbolKind::FormalArgument)
    {
        return Some(format!(
            "it reads or keeps the module-level or `static` variable `{}`, whose live value is \
             not the sampled one",
            sig.name()
        ));
    }
    if abi.needs_handle {
        return Some("it reads a module memory".into());
    }
    None
}

/// Rejects the expressions whose value would not come from the sampled row.
fn check_expression<'d>(
    plan: &ProcessLoweringPlan<'d>,
    e: Expression<'d>,
) -> Result<(), LoweringError> {
    let mut stack = vec![e.as_sem_node()];
    while let Some(n) = stack.pop() {
        if let Some(x) = n.as_expression()
            && x.kind() == ExpressionKind::Call
            && x.is_system_call() == Some(false)
            && let Some(why) = impure_call_reason(x)
        {
            return Err(unsupported(
                plan,
                &format!(
                    "a call to a user function in an assertion expression is not executable: \
                     {why}; the call would not read the sampled values (16.5.1)"
                ),
            ));
        }
        stack.extend(sv_sim_sim::process::cfg::live_children(&n));
    }
    Ok(())
}

/// One sampled value function call (16.9.3) in an assertion's expressions: the
/// engine hands each leaf a position's row followed by the rows of the previous
/// ticks, and the call reads its signals from them.
#[derive(Clone, Debug)]
struct HistSite {
    /// The call's source position, [`sv_sim_sim::sva::sampled::site_loc`].
    loc: String,
    /// The signals the call's argument reads.
    args: Vec<SymbolId>,
    /// How many previous ticks the call reads
    /// ([`sv_sim_sim::sva::sampled::SampledOp::depth`]).
    depth: u32,
    /// The clock the call samples at: the clock its leaf is evaluated in
    /// (16.9.3); its history is that clock's block of the position row.
    clock: u32,
    /// A global clocking future function (16.9.4): it reads the next tick's
    /// row, which follows the history in the position row.
    future: bool,
}

/// The sampled value function calls in `e`, outermost only (a nested one is
/// refused by [`strict_signals_in`] when its site is checked).
fn sampled_calls_in<'d>(
    plan: &ProcessLoweringPlan<'d>,
    e: Expression<'d>,
) -> Result<Vec<SampledCall<'d>>, LoweringError> {
    let mut out = Vec::new();
    let mut stack = vec![e.as_sem_node()];
    while let Some(n) = stack.pop() {
        if let Some(x) = n.as_expression()
            && let Some(call) = decode(x).map_err(|m| unsupported(plan, &m.0))?
        {
            out.push(call);
            continue;
        }
        stack.extend(sv_sim_sim::process::cfg::live_children(&n));
    }
    Ok(out)
}

/// The signal `e` names, when it is nothing but a name.
fn bare_signal(e: Expression<'_>) -> Option<SymbolId> {
    if e.kind() == ExpressionKind::NamedValue {
        e.referenced_symbol().map(|s| s.uid())
    } else {
        None
    }
}

/// A clock of its own that a sampled value function samples at without being
/// the assertion's: an explicit clocking event (16.9.3), the global clock
/// (16.9.4), or one of the assertion's clocks gated by a `$past` gating
/// expression. The engine keeps its history next to the assertion clocks'
/// (`EngineConfig::hist_clocks`); its ticks make no position.
#[derive(Clone)]
struct HistClock<'d> {
    /// The terms, the clock ticking when any term's event occurs (9.4.2).
    terms: Vec<ClockEvent<'d>>,
    /// The gating expression (16.9.3 `expression2`): the clock ticks only
    /// where it is true, sampled with the terms' `iff` conditions.
    gate: Option<Expression<'d>>,
}

/// What [`hist_sites`] found.
struct HistPlan<'d> {
    /// The calls, in leaf order.
    sites: Vec<HistSite>,
    /// The clocks past the assertion's own, indexed `n_clocks + j`.
    extra: Vec<HistClock<'d>>,
    /// The clock the global clocking future functions wait on (16.9.4): an
    /// assertion clock or an extra one. Meaningful only when some site is
    /// `future`.
    future_clock: u32,
    /// The leaves the engine evaluates on the live state that hold a sampled
    /// value function (`disable iff`, asynchronous `accept_on`/`reject_on`,
    /// 16.12): they get a `_lv` function.
    live_calls: Vec<LeafId>,
    /// A clocking event's `iff` calls one: the tick functions read history rows.
    tick_history: bool,
}

/// Whether two clocking events are the same signal events: bare signals, same
/// edges, no `iff`. (A conservative test: two clocks it calls different merely
/// get separate histories.)
fn same_terms(a: &[ClockEvent<'_>], b: &[ClockEvent<'_>]) -> bool {
    a.len() == b.len()
        && a.iter().zip(b).all(|(x, y)| {
            x.edge == y.edge
                && x.iff.is_none()
                && y.iff.is_none()
                && bare_signal(x.signal).is_some()
                && bare_signal(x.signal) == bare_signal(y.signal)
        })
}

/// The index of the clock sampling at `terms` gated by `gate`: an assertion
/// clock or an already listed extra one when it is the same, else a new extra
/// one.
fn clock_index<'d>(
    own: &[Vec<ClockEvent<'d>>],
    extra: &mut Vec<HistClock<'d>>,
    terms: Vec<ClockEvent<'d>>,
    gate: Option<Expression<'d>>,
) -> u32 {
    if gate.is_none() {
        if let Some(c) = own.iter().position(|o| same_terms(o, &terms)) {
            return c as u32;
        }
        if let Some(j) = extra
            .iter()
            .position(|x| x.gate.is_none() && same_terms(&x.terms, &terms))
        {
            return (own.len() + j) as u32;
        }
    }
    extra.push(HistClock { terms, gate });
    (own.len() + extra.len() - 1) as u32
}

/// The sampled value function calls of the assertion's leaves, each checked to be
/// one the engine can evaluate from its position rows. A call reads its signals'
/// sampled values at this tick and at the previous ticks of the clock it samples
/// at (16.9.3, 16.5.1): the clock of the leaf it is in (in a multiclock
/// assertion the leaf's domain), its explicit clocking event, or the global
/// clock (16.9.4). A clock that is not one of the assertion's gets a history of
/// its own ([`HistClock`]); the global clock's next tick serves the future
/// functions. What is left as a named error:
///
/// * a call with no clock of its own in a property-level condition of a
///   multiclock assertion: its clock is not a sequence domain;
/// * an explicit clocking event that is not one signal event (`@(a or b)`,
///   refused by the decoder);
/// * a call in the clocking event itself (16.9.3: the clock of a sampled value
///   function cannot depend on itself).
fn hist_sites<'d>(
    plan: &ProcessLoweringPlan<'d>,
    ir: &PropertyIr,
    roles: &[LeafRole],
    leaves: &LeafTable<'d>,
    clock_events: &[Vec<ClockEvent<'d>>],
) -> Result<HistPlan<'d>, LoweringError> {
    let live = live_leaves(ir);
    let doms = leaf_domains(ir);
    let mut found: Vec<(SampledCall<'d>, Option<u32>)> = Vec::new();
    let mut live_calls: Vec<LeafId> = Vec::new();
    for (i, role) in roles.iter().enumerate() {
        if *role == LeafRole::Unused {
            continue;
        }
        let calls = sampled_calls_in(plan, leaves.get(LeafId(i as u32)))?;
        // Every live-state leaf gets the `_lv` form (a plain `disable iff` too), so
        // the engine reads the signals themselves rather than snapshotting the
        // whole row per fire.
        if live.contains(&LeafId(i as u32)) {
            live_calls.push(LeafId(i as u32));
        }
        let dom = doms.get(&LeafId(i as u32)).copied();
        found.extend(calls.into_iter().map(|c| (c, dom)));
    }
    let mut tick_history = false;
    for ev in clock_events.iter().flatten() {
        if !is_sequence_clock(ev) && !sampled_calls_in(plan, ev.signal)?.is_empty() {
            // The edge of a value that itself changes at another clock's ticks has no
            // meaning the engine could evaluate between two steps.
            return Err(unsupported(
                plan,
                "a sampled value function in the signal of an assertion's clocking event (not \
                 its `iff` condition) is not executable: the event's value would change at the \
                 called function's own clock ticks (16.9.3)",
            ));
        }
        let in_event = match ev.iff {
            Some(c) => sampled_calls_in(plan, c)?,
            None => Vec::new(),
        };
        if in_event.iter().any(|c| c.clock.is_none() && !c.global) {
            // 16.9.3: "if called in a disable condition or a clock expression in an
            // assertion, sequence, or property, it shall be explicitly clocked"; with no
            // clock to infer, the call would sample at the very event it is part of.
            return Err(unsupported(
                plan,
                "a sampled value function in the clocking event of an assertion without an \
                 explicit clocking event is illegal (16.9.3: in a clock expression it shall be \
                 explicitly clocked; the inferred clock would be the event itself)",
            ));
        }
        if !in_event.is_empty() {
            // Well-formed (its own explicit clock gives it a history). The `iff` is
            // judged on the Preponed values of the step, so the engine hands the tick
            // function the step's position row (`EngineConfig::tick_history`): the
            // function reads strictly earlier ticks of its own clock.
            tick_history = true;
            found.extend(in_event.into_iter().map(|c| (c, None)));
        }
    }
    let mut out = HistPlan {
        sites: Vec::with_capacity(found.len()),
        extra: Vec::new(),
        future_clock: 0,
        live_calls,
        tick_history,
    };
    if found.is_empty() {
        return Ok(out);
    }
    if clock_events.is_empty() {
        return Err(unsupported(
            plan,
            "a sampled value function in an assertion with no clocking event",
        ));
    }
    let mut global_terms: Option<Vec<ClockEvent<'d>>> = None;
    for (call, dom) in found {
        // 16.9.4: `$rose_gclk(v)` is `$rose(v, @$global_clock)`.
        let explicit = if call.global {
            if global_terms.is_none() {
                global_terms = Some(clock_terms_of(plan, global_clock_event(plan)?)?);
            }
            global_terms.clone()
        } else {
            call.clock.map(|ev| vec![ev])
        };
        let clock = match explicit {
            Some(terms) => clock_index(clock_events, &mut out.extra, terms, call.gate),
            None => {
                // The clock the call's leaf is evaluated in: the assertion's only
                // one, or in a multiclock assertion the domain of the leaf
                // (16.9.3).
                let dom = if clock_events.len() == 1 {
                    0
                } else {
                    dom.ok_or_else(|| {
                        unsupported(
                            plan,
                            "a sampled value function with no clocking event of its own in a \
                             multiclock assertion, outside any sequence operand (a \
                             property-level condition), is not executable yet: its clock is \
                             not a sequence domain",
                        )
                    })?
                };
                match call.gate {
                    None => dom,
                    gate => clock_index(
                        clock_events,
                        &mut out.extra,
                        clock_events[dom as usize].clone(),
                        gate,
                    ),
                }
            }
        };
        if call.op.is_future() {
            out.future_clock = clock;
        }
        let args = strict_site_signals_in(call.arg)
            .map_err(|m| unsupported(plan, &m.0))?
            .into_iter()
            .collect();
        out.sites.push(HistSite {
            loc: sv_sim_sim::sva::sampled::site_loc(&call.call),
            args,
            depth: call.op.depth(call.ticks),
            clock,
            future: call.op.is_future(),
        });
    }
    Ok(out)
}

/// The clock domain each automaton leaf is evaluated in: from each automaton's
/// (and end-point instance's) entry clock, a `ClockSync` edge switches domains.
/// A leaf reached in several domains keeps the first found.
fn leaf_domains(ir: &PropertyIr) -> std::collections::HashMap<LeafId, u32> {
    let mut out = std::collections::HashMap::new();
    // The property's sequences start in their own clocks (an implication's
    // consequent after a clock change, 16.13.2).
    let mut roots: Vec<(ThreadStateId, ClockId)> = Vec::new();
    for p in &ir.props {
        match p {
            Prop::Seq { seq, .. } => roots.push((seq.entry, seq.clock)),
            Prop::Implication { ante, .. } => roots.push((ante.entry, ante.clock)),
            _ => {}
        }
    }
    let mut autos = vec![&ir.automaton];
    let mut top = true;
    while let Some(a) = autos.pop() {
        autos.extend(a.end_points.iter().map(|ep| &ep.automaton));
        let mut seen = BTreeSet::new();
        let mut queue = vec![(a.start, a.entry_clock)];
        if std::mem::take(&mut top) {
            queue.extend(roots.iter().copied());
        }
        while let Some((state, dom)) = queue.pop() {
            if !seen.insert((state.0, dom.0)) {
                continue;
            }
            for edge in &a.states[state.0 as usize].edges {
                // A clock change's guard is sampled at the new clock's tick.
                let at = match &edge.label {
                    Transition::ClockSync { to, .. } => *to,
                    _ => dom,
                };
                if let Some(g) = edge.guard {
                    out.entry(g).or_insert(at.0);
                }
                let next = match &edge.label {
                    Transition::ClockSync { to, .. } => *to,
                    Transition::LocalVarWrite { value, .. } => {
                        out.entry(*value).or_insert(dom.0);
                        dom
                    }
                    Transition::Abort { leaf, .. } => {
                        out.entry(*leaf).or_insert(dom.0);
                        dom
                    }
                    _ => dom,
                };
                queue.push((edge.target, next));
            }
        }
    }
    out
}

/// The event of the global clocking in effect for `plan`'s instance (LRM
/// 14.14's hierarchical lookup).
fn global_clock_event<'d>(
    plan: &ProcessLoweringPlan<'d>,
) -> Result<TimingControl<'d>, LoweringError> {
    let body = sv_sim_sim::netlist::enclosing_instance_body(&plan.fn_sym)
        .ok_or_else(|| unsupported(plan, "`$global_clock` outside any instance body"))?;
    let found = crate::classes::with_design_trees(|trees| {
        sv_sim_sim::sva::global_clock::global_clocking_of(&body, trees)
    })
    .map_err(|e| unsupported(plan, &e.0))?;
    let global = found.ok_or_else(|| {
        unsupported(
            plan,
            "`$global_clock` with no global clocking declaration in scope (LRM 14.14: the \
             lookup climbs the instance hierarchy to the top and an absent declaration is an \
             error)",
        )
    })?;
    // A global clocking of an enclosing instance (`levels_up > 0`) has its event
    // signals registered as this instance's foreign references (bin `run.rs`).
    global
        .block
        .clocking_block_event()
        .and_then(|n| n.as_timing_control())
        .ok_or_else(|| unsupported(plan, "the global clocking declaration has no event"))
}

/// The clocking event of the clocking block `tc` names (`@(cb)`), `None` for
/// any other event control.
fn clocking_block_named_event<'d>(tc: TimingControl<'d>) -> Option<TimingControl<'d>> {
    if tc.kind() != TimingControlKind::SignalEvent || tc.edge() != sv_lang::EdgeKind::None {
        return None;
    }
    let x = tc.children().first()?.as_expression()?;
    let sym = x.referenced_symbol()?;
    (sym.kind() == SymbolKind::ClockingBlock)
        .then(|| sym.clocking_block_event())
        .flatten()
        .and_then(|n| n.as_timing_control())
}

/// The terms of the clocking event `tc`: the one signal event, or the entries
/// of an event list (`@(posedge a or negedge b)`, 9.4.2), flattened. Any other
/// control is a named error.
fn clock_terms_of<'d>(
    plan: &ProcessLoweringPlan<'d>,
    tc: TimingControl<'d>,
) -> Result<Vec<ClockEvent<'d>>, LoweringError> {
    // `@$global_clock` (14.14, e.g. a checker's `default clocking
    // @$global_clock`): the event of the global clocking in effect.
    if sv_sim_sim::sva::sampled::is_global_clock_event(tc) {
        return clock_terms_of(plan, global_clock_event(plan)?);
    }
    // `@(cb)` / `@cb`, a clocking block named as the event (9.4.2, 14.3): the
    // block's own clocking event.
    if let Some(cev) = clocking_block_named_event(tc) {
        return clock_terms_of(plan, cev);
    }
    if tc.kind() != TimingControlKind::EventList {
        return Ok(vec![
            assertion_clock_event_of(tc).map_err(|e| unsupported(plan, &e.0))?,
        ]);
    }
    let mut terms = Vec::new();
    for sub in tc
        .children()
        .into_iter()
        .filter_map(|n| n.as_timing_control())
    {
        terms.extend(clock_terms_of(plan, sub)?);
    }
    if terms.is_empty() {
        return Err(unsupported(plan, "a clocking event list with no entries"));
    }
    Ok(terms)
}

/// Whether `e` contains a call of `$inferred_disable` (17.4).
fn mentions_inferred_disable(e: Expression<'_>) -> bool {
    mentions_inferred_disable_in(e.as_sem_node())
}

/// [`mentions_inferred_disable`] over any node (a procedure's body statement).
pub(crate) fn mentions_inferred_disable_in(root: SemNode<'_>) -> bool {
    let mut stack = vec![root];
    while let Some(n) = stack.pop() {
        if let Some(x) = n.as_expression()
            && x.call_subroutine_name().as_deref() == Some("$inferred_disable")
        {
            return true;
        }
        stack.extend(sv_sim_sim::process::cfg::live_children(&n));
    }
    false
}

/// The scope a checker's `$inferred_clock` and `$inferred_disable` (17.4,
/// 16.14.7) are resolved in: the scope that instantiates the checker, not the
/// checker's own declaration. For an assertion of a static instance (its blocks
/// are members of the instance's body, whose parent is the instance) that is the
/// instance's parent scope; for a procedural instance (17.3, hosted by the
/// procedure that reaches it) and for an assertion that is no checker's, the
/// block itself.
fn instantiation_scope<'d>(plan: &ProcessLoweringPlan<'d>) -> Symbol<'d> {
    let hosted_instance = plan.hosted_assertion.is_some_and(|h| h.instance.is_some());
    if !hosted_instance && let Some(scope) = checker_instantiation_scope(&plan.fn_sym) {
        return scope;
    }
    plan.fn_sym
}

/// The formal bindings of the checker instance whose body holds `sym` (17.2,
/// 17.3), for a `##[1:hi]` / `[*hi]` bound that names a checker formal; `None`
/// when `sym` is no checker's.
fn checker_frame_of<'d>(
    sym: &Symbol<'d>,
    trees: &[SyntaxTree],
) -> Option<super::ranges::FormalFrame> {
    let mut up = sym.parent();
    while let Some(s) = up {
        if s.kind() == SymbolKind::CheckerInstanceBody {
            let inst = s.checker_instance_body_parent_instance()?;
            let tree = trees.iter().find(|t| s.syntax(t).is_some())?;
            let decl = super::trees::key(s.syntax(tree)?);
            return Some(super::ranges::checker_frame(&inst, decl, trees));
        }
        if s.kind() == SymbolKind::InstanceBody {
            return None;
        }
        up = s.parent();
    }
    None
}

/// The scope that instantiates the static checker whose body holds `sym`
/// (directly, or through generate blocks of the body: 17.9's
/// `generate if (...) begin : cover_b`); `None` for a symbol that is no static
/// checker instance's.
pub(crate) fn checker_instantiation_scope<'d>(sym: &Symbol<'d>) -> Option<Symbol<'d>> {
    let mut up = sym.parent();
    while let Some(s) = up {
        if s.kind() == SymbolKind::CheckerInstanceBody {
            return s
                .checker_instance_body_parent_instance()
                .and_then(|inst| inst.parent());
        }
        if s.kind() == SymbolKind::InstanceBody {
            return None;
        }
        up = s.parent();
    }
    None
}

/// What `$inferred_disable` (17.4) stands for in the checker procedure `proc_sym`,
/// from its source's `trees`: `None` when the procedure is no static checker's or
/// never mentions it; else the `default disable iff` signal of the instantiating
/// scope and whether it is negated, the inner `None` being the `1'b0` of a scope
/// with no default (16.15 rule c).
pub fn procedure_inferred_disable<'d>(
    proc_sym: &Symbol<'d>,
    trees: &[SyntaxTree],
) -> Result<Option<Option<(Symbol<'d>, bool)>>, LoweringError> {
    let Some(context) = checker_instantiation_scope(proc_sym) else {
        return Ok(None);
    };
    let Some(body) = sv_sim_sim::process::cfg::proc_body(proc_sym) else {
        return Ok(None);
    };
    if !mentions_inferred_disable_in(body.as_sem_node()) {
        return Ok(None);
    }
    checker_inferred_disable(proc_sym, trees, &context)
}

/// [`procedure_inferred_disable`] for any symbol of a static checker's body (a
/// procedure, or a function it declares), with no check for a mention.
fn checker_inferred_disable<'d>(
    sym: &Symbol<'d>,
    trees: &[SyntaxTree],
    context: &Symbol<'d>,
) -> Result<Option<Option<(Symbol<'d>, bool)>>, LoweringError> {
    let tree = trees
        .iter()
        .find(|t| sym.syntax(t).is_some())
        .or_else(|| trees.first())
        .ok_or_else(|| {
            LoweringError::unsupported_at("no syntax tree for a checker procedure", sym)
        })?;
    Ok(Some(
        resolve_default_disable(context, tree)?
            .map(|d| d.single(context))
            .transpose()?,
    ))
}

/// The signals named by the `default disable iff` that applies to assertions
/// written in instance body `body` (LRM 16.15), for the caller to give the
/// instance a slot for each. A declaration in an ENCLOSING module declaration
/// (a nested module inherits it) names signals of the enclosing instance, which
/// the assertion row can only read through a foreign slot. An unsupported form
/// is not an error here: lowering the assertion reports it by name.
pub fn default_disable_signals<'d>(body: &Symbol<'d>, tree: &SyntaxTree) -> Vec<Symbol<'d>> {
    match resolve_default_disable(body, tree) {
        Ok(Some(d)) => [Some(d.signal), d.second.map(|(s, _)| s)]
            .into_iter()
            .flatten()
            .collect(),
        _ => Vec::new(),
    }
}

/// What `$inferred_disable` stands for in the code of `sym`, a symbol of a static
/// checker's body (a function it declares included), from the design syntax held
/// by `classes::DesignSyntaxScope`. `Ok(None)` for any other symbol. This is also
/// the `sv_sim_sim::sva::sampled::InferredDisableResolver`.
pub(crate) fn resolve_checker_inferred_disable<'d>(
    sym: &Symbol<'d>,
) -> Result<Option<Option<(Symbol<'d>, bool)>>, String> {
    let Some(context) = checker_instantiation_scope(sym) else {
        return Ok(None);
    };
    crate::classes::with_design_trees(|trees| checker_inferred_disable(sym, trees, &context))
        .map_err(|e| e.to_string())
}

/// The signal `$inferred_disable` reads in the code being emitted, if it is one.
pub(crate) fn inferred_disable_signal() -> Option<SymbolId> {
    INFERRED_DISABLE.with(|c| c.borrow().clone().flatten().map(|(id, _)| id))
}

thread_local! {
    /// The `default disable iff` of the instantiation context of the assertion
    /// whose functions are being emitted, as (signal, negated): what its
    /// `$inferred_disable` value calls read (17.4); the inner `None` is 1'b0.
    /// The outer `None` is "no assertion being emitted".
    static INFERRED_DISABLE: std::cell::RefCell<Option<Option<(SymbolId, bool)>>> =
        const { std::cell::RefCell::new(None) };
}

/// Installs an assertion's `$inferred_disable` for the duration of its emission and
/// restores the previous one.
pub(crate) struct InferredDisableGuard(Option<Option<(SymbolId, bool)>>);

impl InferredDisableGuard {
    fn enter(disable: Option<(SymbolId, bool)>) -> Self {
        Self(INFERRED_DISABLE.with(|c| c.borrow_mut().replace(disable)))
    }

    /// Installs the `$inferred_disable` of a checker procedure's plan
    /// (`ProcessLoweringPlan::inferred_disable`); a plan with none leaves the
    /// current state alone.
    pub(crate) fn enter_plan(state: Option<Option<(SymbolId, bool)>>) -> Self {
        match state {
            Some(disable) => Self::enter(disable),
            None => Self(INFERRED_DISABLE.with(|c| c.borrow().clone())),
        }
    }
}

impl Drop for InferredDisableGuard {
    fn drop(&mut self) {
        INFERRED_DISABLE.with(|c| *c.borrow_mut() = self.0.take());
    }
}

/// `$inferred_disable` (17.4) as a value inside an assertion expression: the
/// `default disable iff` expression of the checker's instantiation context, or
/// `1'b0` when it has none. `None` for any other call.
pub(crate) fn lower_inferred_disable<'ctx>(
    cx: &LowerCtx<'ctx, '_, '_>,
    known: sv_lang::KnownSystemName,
) -> Option<Result<LoweredValue<'ctx>, LoweringError>> {
    if known != sv_lang::KnownSystemName::InferredDisable {
        return None;
    }
    let mut state = INFERRED_DISABLE.with(|c| c.borrow().clone());
    // A function a checker declares (called from a procedure, 17.7.1) is lowered
    // on its own, outside any procedure's plan: it reads its instance's.
    if state.is_none()
        && cx.fn_sym.kind() == SymbolKind::Subroutine
        && let Ok(Some(found)) = resolve_checker_inferred_disable(&cx.fn_sym)
    {
        state = Some(found.map(|(sym, negate)| (sym.uid(), negate)));
    }
    let ctx = cx.ctx;
    let ob = OpBuilder { ctx, b: &cx.b };
    let out = match state {
        None => Err(LoweringError::unsupported_at(
            "`$inferred_disable` (LRM 17.4) outside a static checker instance's concurrent \
             assertions, procedures and functions",
            &cx.fn_sym,
        )),
        Some(_) if cx.repr != ValueRepr::FourState => Err(LoweringError::unsupported_at(
            "`$inferred_disable` (LRM 17.4) in a two-state lowering",
            &cx.fn_sym,
        )),
        Some(None) => {
            let zero = ctx.bool_type().const_zero();
            Ok(LoweredValue::Packed(ob.pack(zero, zero, 1, cx.repr, false)))
        }
        Some(Some((signal, negate))) => match cx.locals.get(&signal).copied() {
            None => Err(LoweringError::unsupported_at(
                "the `default disable iff` signal `$inferred_disable` stands for (LRM 17.4) is \
                 not a module signal an assertion can read",
                &cx.fn_sym,
            )),
            Some((slot, width, signed)) => {
                let ty = ob.i_n(width * 2);
                let raw = cx.b.build_load(ty, slot, "id_ld").unwrap().into_int_value();
                let pv = PackedValue {
                    llvm: raw,
                    width,
                    repr: cx.repr,
                    signed,
                };
                // The value of the expression as a condition: a 1-bit, X-preserving
                // truth value.
                Ok(LoweredValue::Packed(if negate {
                    ob.lnot4(pv)
                } else {
                    ob.redor4(pv)
                }))
            }
        },
    };
    Some(out)
}

/// Whether `e` contains a reference to the target of a compound assignment
/// (`v += e`: the item reads the old value of `v`).
fn reads_lvalue_reference(e: Expression<'_>) -> bool {
    let mut stack = vec![e.as_sem_node()];
    while let Some(n) = stack.pop() {
        if let Some(x) = n.as_expression()
            && x.kind() == ExpressionKind::LValueReference
        {
            return true;
        }
        stack.extend(sv_sim_sim::process::cfg::live_children(&n));
    }
    false
}

/// Builds the property of `stmt`, the static assertion of `plan`.
fn build_of<'d>(
    plan: &ProcessLoweringPlan<'d>,
    stmt: Statement<'d>,
    kind: AssertKind,
    body: &Symbol<'d>,
    trees: &[SyntaxTree],
    inferred_clock: Option<SemNode<'d>>,
) -> Result<(PropertyIr, LeafTable<'d>), LoweringError> {
    let tree = trees
        .iter()
        .find(|t| plan.fn_sym.syntax(t).is_some())
        .or_else(|| trees.first())
        .ok_or_else(|| unsupported(plan, "no syntax tree for an assertion"))?;
    let root = stmt
        .as_sem_node()
        .children()
        .into_iter()
        .find_map(|n| n.as_assertion_expr())
        .ok_or_else(|| unsupported(plan, "a concurrent assertion with no property"))?;
    let (root, root_clock, root_inferred) = if root.kind() == AssertionExprKind::Clocking {
        let mut kids = root.children();
        let mut inner = kids
            .get(1)
            .and_then(|k| k.as_assertion_expr())
            .ok_or_else(|| unsupported(plan, "a clocked property with no body"))?;
        // 16.13.3: juxtaposed clocking events (`@(d) @(c) x`) nullify the first:
        // the property is clocked by the innermost one, as `@(c) x`.
        while inner.kind() == AssertionExprKind::Clocking {
            kids = inner.children();
            inner = kids
                .get(1)
                .and_then(|k| k.as_assertion_expr())
                .ok_or_else(|| unsupported(plan, "a clocked property with no body"))?;
        }
        let event = kids.first().copied();
        if event.is_some_and(is_inferred_clock_event) {
            // 17.4: `@clock` with `clock` defaulted to `$inferred_clock`: the clock
            // of the instantiation context, which the caller worked out
            // (`inferred_clock`), never a clock the assertion wrote.
            (inner, inferred_clock, true)
        } else {
            (inner, event, false)
        }
    } else {
        // 16.14.6: the clock a procedural assertion has none of its own is the
        // enclosing block's; then the default clocking (14.12).
        let clock = match inferred_clock {
            Some(c) => Some(c),
            None => match default_clocking_event(&plan.fn_sym, tree)? {
                // 17.4: a checker's `default clocking @clock;` whose `clock` kept
                // its `$inferred_clock` default is the default clocking of the scope
                // instantiating the checker (14.12), never the call itself.
                Some(ev) if is_inferred_clock_event(ev) => {
                    default_clocking_event(&instantiation_scope(plan), tree)?
                }
                other => other,
            },
        };
        (root, clock, true)
    };
    build_property_as(
        root,
        root_clock,
        super::trees::Trees::new(trees),
        body,
        kind == AssertKind::CoverSequence,
        root_inferred,
        checker_frame_of(&plan.fn_sym, trees),
    )
}

/// Compiles every static concurrent assertion of `plans` into `module`.
pub(crate) fn emit_assertions<'ctx, 'd>(
    ctx: &'ctx Context,
    module: &Module<'ctx>,
    fns: &AccessorFns<'ctx>,
    plans: &[ProcessLoweringPlan<'d>],
    design: &'d Design,
) -> Result<Vec<AssertionSpec>, LoweringError> {
    let mut specs = Vec::new();
    let mut trees: Option<Vec<SyntaxTree>> = None;
    let mut resolver = crate::sampled::ClockResolver::new(design);
    let mut watched: BTreeSet<SymbolId> = BTreeSet::new();
    for (plan_index, plan) in plans.iter().enumerate() {
        // The plan's assertion statement, and the sequence instances its
        // procedure reads the end point of (`sv_sim_sim::sva::endpoint`).
        let mut jobs: Vec<Job<'d>> = Vec::new();
        if let Some(h) = plan.hosted_assertion {
            jobs.push(Job::Stmt(h.stmt, h.procedural));
            // 16.5.2: a static assertion clocked by a sequence watches it (a
            // procedural one's watchers are the enclosing block's own plan's).
            if !h.procedural && h.instance.is_none() {
                for (k, w) in sv_sim_sim::sva::endpoint::block_watchers(&plan.fn_sym)
                    .into_iter()
                    .enumerate()
                {
                    if watched.insert(w.id()) {
                        jobs.push(Job::Watch(w.inst, w.id(), k));
                    }
                }
            }
        } else if plan.fn_sym.kind() == SymbolKind::ProceduralBlock {
            if plan.fn_sym.procedural_block_procedure_kind() == ProceduralBlockKind::Always
                && let Some(full_body) = sv_sim_sim::process::cfg::proc_body(&plan.fn_sym)
                && let Some(stmt) = static_assertion_statement(full_body)
            {
                jobs.push(Job::Stmt(stmt, false));
            }
            for (k, w) in sv_sim_sim::sva::endpoint::block_watchers(&plan.fn_sym)
                .into_iter()
                .enumerate()
            {
                // Two plans of one block share its watchers.
                if watched.insert(w.id()) {
                    jobs.push(Job::Watch(w.inst, w.id(), k));
                }
            }
        }
        for job in jobs {
            let (stmt, procedural, watch) = match job {
                Job::Stmt(s, p) => (Some(s), p, None),
                Job::Watch(inst, id, k) => (None, false, Some((inst, id, k))),
            };
            let name = match &watch {
                None => format!("{}_a", plan.fn_name),
                Some((_, _, k)) => format!("{}_w{k}", plan.fn_name),
            };
            if module.get_function(&format!("{name}_snap")).is_some() {
                continue;
            }
            let kind = match stmt {
                Some(stmt) => assert_kind(plan, stmt)?,
                // A watcher reports every end point (16.9.11) as a match.
                None => AssertKind::CoverSequence,
            };
            let trees = trees.get_or_insert_with(|| design.syntax_trees());
            let body = sv_sim_sim::netlist::enclosing_instance_body(&plan.fn_sym)
                .ok_or_else(|| unsupported(plan, "a procedural block outside any instance body"))?;
            // The sampled value functions of THIS assertion's property are evaluated
            // here, over the engine's position rows (`hist_sites`); the ones in an
            // action block are lowered like any other in a procedural block, from
            // the block's own history cells, by the host plan
            // (`sv_sim_sim::sva::sampled::sites_of_block` leaves the property out).
            // 16.14.6: a procedural assertion with no clock of its own infers the
            // block's (else the default clocking applies, 14.12).
            let root_event = stmt.and_then(|stmt| {
                stmt.as_sem_node()
                    .children()
                    .into_iter()
                    .find_map(|n| n.as_assertion_expr())
                    .filter(|r| r.kind() == AssertionExprKind::Clocking)
                    .and_then(|r| r.children().first().copied())
            });
            // `@clock` with `clock` defaulted to `$inferred_clock` is not a clock the
            // assertion wrote: it is the one of the checker's instantiation (17.4).
            let has_own_clock = root_event.is_some_and(|ev| !is_inferred_clock_event(ev));
            let tree = trees
                .iter()
                .find(|t| plan.fn_sym.syntax(t).is_some())
                .or_else(|| trees.first())
                .ok_or_else(|| unsupported(plan, "no syntax tree for an assertion"))?;
            let context = instantiation_scope(plan);
            let inferred_clock = if watch.is_some() {
                // A watched instance with no clock of its own runs on the reading
                // procedure's inferred clock (16.14.6), else the default clocking.
                match resolver.inferred_node(&plan.fn_sym).ok().flatten() {
                    Some(c) => Some(c),
                    None => default_clocking_event(&context, tree)?,
                }
            } else if root_event.is_some_and(is_inferred_clock_event) {
                // 17.4 / 16.14.7: the clock inferred in the instantiation context: the
                // enclosing procedure's (16.14.6) for a procedural instance, else the
                // default clocking of the scope instantiating a static one.
                let from_procedure = if procedural {
                    resolver.inferred_node(&plan.fn_sym)?
                } else {
                    None
                };
                let clock = match from_procedure {
                    Some(c) => Some(c),
                    None => default_clocking_event(&context, tree)?,
                };
                if clock.is_none() {
                    return Err(unsupported(
                        plan,
                        "`$inferred_clock` (LRM 17.4, 16.14.7): the checker is instantiated where no \
                     clock is inferred: it is not in a procedure with an inferred clock \
                     (16.14.6) and no default clocking applies (14.12)",
                    ));
                }
                clock
            } else if procedural && !has_own_clock {
                resolver.inferred_node(&plan.fn_sym)?
            } else {
                None
            };
            let (mut ir, leaves) = match (stmt, &watch) {
                (Some(stmt), _) => build_of(plan, stmt, kind, &body, trees, inferred_clock)?,
                (None, Some((inst, _, _))) => super::build::property::build_sequence_watcher(
                    *inst,
                    inferred_clock,
                    super::trees::Trees::new(trees),
                    &body,
                )?,
                (None, None) => {
                    return Err(unsupported(
                        plan,
                        "internal error: an assertion job with nothing to build",
                    ));
                }
            };
            // 17.4: `$inferred_disable` is the `default disable iff` of the
            // instantiation context, as a `disable iff` operand (`ir.disable` is then
            // empty) or as a value in an expression.
            let uses_inferred_disable_value =
                (0..leaves.len()).any(|i| mentions_inferred_disable(leaves.get(LeafId(i as u32))));
            let context_disable = if leaves.disable_inferred() || uses_inferred_disable_value {
                let d = resolve_default_disable(&context, tree)?;
                if let Some(d) = d {
                    // Only one signal fits `$inferred_disable` (17.4).
                    d.single(&context)?;
                }
                d
            } else {
                None
            };
            // 16.15 rule (b): an assertion with no `disable iff` of its own (or one
            // that is `$inferred_disable`, 16.14.7) takes the `default disable iff`
            // in scope, an extra leaf that reads the signal it names.
            let default_disable = if ir.disable.is_none() {
                if leaves.disable_inferred() {
                    context_disable
                } else {
                    resolve_checker_default_disable(&plan.fn_sym, &context, tree)?
                }
            } else {
                None
            };
            let _inferred_disable_guard = InferredDisableGuard::enter(
                context_disable.as_ref().map(|d| (d.signal.uid(), d.negate)),
            );
            // The values an instance captures live in local-variable slots, assigned
            // when the attempt starts (`PropEnv::initial_frame`).
            let captured: Vec<(CaptureItem<'d>, LocalVarId)> = match stmt {
                Some(stmt) => capture_items(&plan.signals, stmt, &plan.fn_sym)?,
                None => Vec::new(),
            }
            .into_iter()
            .map(|item| {
                let var = ir.automaton.new_local_var(item.width, item.signed);
                (item, var)
            })
            .collect();
            let items: Vec<CaptureItem<'d>> = captured.iter().map(|(i, _)| i.clone()).collect();
            // 16.11: the attached calls are dispatched by this assertion's kernel.
            *plan.assertion_calls.borrow_mut() = leaves.calls().to_vec();
            let n_leaves = leaves.len();
            let mut roles = leaf_roles(plan, &ir, n_leaves)?;
            let mut disable_mixed = false;
            let mut leaf_reads = Vec::with_capacity(n_leaves);
            let mut leaf_writes = Vec::with_capacity(n_leaves);
            for i in 0..n_leaves {
                let l = leaves.locals_of(LeafId(i as u32));
                let mut reads: Vec<LocalVarId> = l.reads.iter().map(|(_, v)| *v).collect();
                // An end-point application inside the expression reads the flag the
                // `EndPoint` edge before the leaf stored (16.9.11).
                reads.extend(l.end_flags.iter().copied());
                for k in items_used_by(&items, leaves.get(LeafId(i as u32))) {
                    if ir.disable == Some(LeafId(i as u32)) {
                        // 16.14.6.1: an automatic variable's value is captured when the
                        // assertion is queued, so a condition of captured values alone
                        // is a constant of the attempt, which the engine judges per
                        // attempt. A condition that also reads a signal needs the live
                        // value of the signal AND the attempt's captured one: the engine
                        // evaluates it per distinct captured tuple (`disable_mixed`).
                        if first_non_captured_read(&items, leaves.get(LeafId(i as u32))).is_some() {
                            disable_mixed = true;
                        }
                    }
                    reads.push(captured[k].1);
                }
                match l.lvalue {
                    // `v += e`: the old value of `v` is read, so `v` must be assigned.
                    Some(v) if reads_lvalue_reference(leaves.get(LeafId(i as u32))) => {
                        reads.push(v);
                        leaf_writes.push(None);
                    }
                    // `v = e`: nothing of `v` is read.
                    other => leaf_writes.push(other),
                }
                leaf_reads.push(reads);
            }
            for (i, role) in roles.iter().enumerate() {
                if *role != LeafRole::Unused {
                    check_expression(plan, leaves.get(LeafId(i as u32)))?;
                }
            }
            if default_disable.is_some() {
                // The default disable condition is one more (Bool) leaf, past the
                // builder's: it reads no local variable.
                ir.disable = Some(LeafId(n_leaves as u32));
                leaf_reads.push(Vec::new());
                leaf_writes.push(None);
            }
            // The clocks.
            let n_clocks = leaves.clock_count();
            // One entry per clock: its terms (`@(posedge a or posedge b)` is one clock
            // that ticks when either term's event occurs, 9.4.2).
            let mut clock_events: Vec<Vec<ClockEvent<'d>>> = Vec::with_capacity(n_clocks);
            for c in 0..n_clocks {
                let node = leaves.clock_event(ClockId(c as u32)).ok_or_else(|| {
                unsupported(
                    plan,
                    "an assertion with no clocking event: it has none of its own and the module \
                     has no `default clocking` (16.14.6, 14.12)",
                )
            })?;
                let tc = node.as_timing_control().ok_or_else(|| {
                    unsupported(plan, "a clocking event that is not an event control")
                })?;
                let terms = clock_terms_of(plan, tc)?;
                for ev in &terms {
                    if is_sequence_clock(ev) {
                        sequence_clock_id(plan, ev)?;
                    } else {
                        check_expression(plan, ev.signal)?;
                    }
                    if let Some(i) = ev.iff {
                        check_expression(plan, i)?;
                    }
                }
                clock_events.push(terms);
            }
            let HistPlan {
                sites: hist,
                extra: hist_extra,
                future_clock,
                live_calls,
                tick_history,
            } = hist_sites(plan, &ir, &roles, &leaves, &clock_events)?;
            // The `default disable iff` leaf, past the builder's, is live too.
            let mut live_calls = live_calls;
            if default_disable.is_some() {
                live_calls.push(LeafId(n_leaves as u32));
            }
            let history_depth = hist.iter().map(|s| s.depth as usize).max().unwrap_or(0);
            // The row.
            let mut exprs: Vec<Expression<'d>> = Vec::new();
            for (i, role) in roles.iter().enumerate() {
                if *role != LeafRole::Unused {
                    exprs.push(leaves.get(LeafId(i as u32)));
                }
            }
            let mut watcher_ids: Vec<SymbolId> = Vec::new();
            for ev in clock_events.iter().flatten() {
                if is_sequence_clock(ev) {
                    // 16.5.2: the sequence's watcher cell is the clock's row entry.
                    watcher_ids.push(sequence_clock_id(plan, ev)?);
                } else {
                    exprs.push(ev.signal);
                }
                exprs.extend(ev.iff);
            }
            // The clocks the sampled value functions sample at on their own.
            for clock in &hist_extra {
                for ev in &clock.terms {
                    if is_sequence_clock(ev) {
                        return Err(unsupported(
                            plan,
                            "a sequence instance (`@seq`, LRM 16.5.2) as the clocking event of a \
                             sampled value function",
                        ));
                    }
                    check_expression(plan, ev.signal)?;
                    exprs.push(ev.signal);
                    if let Some(i) = ev.iff {
                        check_expression(plan, i)?;
                        exprs.push(i);
                    }
                }
                if let Some(g) = clock.gate {
                    check_expression(plan, g)?;
                    exprs.push(g);
                }
            }
            let extra: Vec<Symbol<'d>> = default_disable
                .iter()
                .chain(context_disable.iter())
                .flat_map(|d| [Some(d.signal), d.second.map(|(s, _)| s)])
                .flatten()
                .collect();
            let clock_nodes: Vec<SemNode<'d>> = (0..n_clocks)
                .filter_map(|c| leaves.clock_event(ClockId(c as u32)))
                .collect();
            let (row, free, observed, mixed, colls) =
                row_signals(plan, &exprs, &extra, &clock_nodes, &watcher_ids)?;
            let mut case_pairs: Vec<(LeafId, LeafId)> = Vec::new();
            for p in &ir.props {
                if let Prop::Case { selector, arms, .. } = p {
                    for arm in arms {
                        for l in &arm.labels {
                            if !case_pairs.contains(&(*selector, *l)) {
                                case_pairs.push((*selector, *l));
                            }
                        }
                    }
                }
            }
            let e = Emitter {
                ctx,
                module,
                fns,
                plan,
                row: &row,
                ir: &ir,
                leaves: &leaves,
                captured: &captured,
                hist: &hist,
                total_clocks: n_clocks + hist_extra.len(),
                tick_history,
                leaf_decls: leaf_owner_decls(&ir, n_leaves),
                mixed: &mixed,
                domains: leaf_domains(&ir),
            };
            e.snap(&format!("{name}_snap"))?;
            for (i, role) in roles.iter().enumerate() {
                if *role != LeafRole::Unused {
                    e.leaf(&format!("{name}_l{i}"), LeafId(i as u32), *role, false)?;
                }
            }
            for l in &live_calls {
                if l.0 as usize >= n_leaves {
                    continue;
                }
                e.leaf(&format!("{name}_lv{}", l.0), *l, roles[l.0 as usize], true)?;
            }
            if let Some(d) = &default_disable {
                e.default_disable_leaf(&format!("{name}_l{n_leaves}"), d, false)?;
                e.default_disable_leaf(&format!("{name}_lv{n_leaves}"), d, true)?;
                roles.push(LeafRole::Bool);
            }
            for (c, terms) in clock_events.iter().enumerate() {
                e.tick(&format!("{name}_t{c}"), terms, None)?;
            }
            for (j, clock) in hist_extra.iter().enumerate() {
                e.tick(
                    &format!("{name}_t{}", n_clocks + j),
                    &clock.terms,
                    clock.gate,
                )?;
            }
            for (k, (s, l)) in case_pairs.iter().enumerate() {
                e.case_pair(&format!("{name}_c{k}"), *s, *l)?;
            }
            let label = plan.fn_sym.name().to_string();
            specs.push(AssertionSpec {
                plan_index,
                name,
                kind,
                ir,
                n_clocks,
                leaf_reads,
                leaf_writes,
                roles,
                row_len: row.iter().map(|(_, info)| row_words(info)).sum(),
                case_pairs,
                label,
                activated: procedural,
                disable_mixed,
                tick_history,
                // One entry per captured WORD: a wide value takes the consecutive
                // slots of its local variable (`CaptureItem::words`).
                captured: captured
                    .iter()
                    .flat_map(|(item, v)| (0..item.words() as u32).map(|k| LocalVarId(v.0 + k)))
                    .collect(),
                history_depth,
                site: stmt.and_then(|stmt| crate::assert_site::describe(&plan.fn_sym, stmt)),
                current_words: active_free_words(&row, &free),
                observed_words: active_free_words(&row, &observed)
                    .into_iter()
                    .map(|(_, base, n)| (base, n))
                    .collect(),
                coll_words: active_free_words_of(&row, colls.keys())
                    .into_iter()
                    .map(|(_, base, _)| base)
                    .collect(),
                coll_nests: active_free_words_of(&row, colls.keys())
                    .into_iter()
                    .map(|(id, _, _)| colls[&id].clone())
                    .collect(),
                spawn_calls: Vec::new(),
                src_offset: stmt.map(|s| s.source_range().start.offset),
                leaf_src: (0..n_leaves)
                    .map(|i| {
                        let r = leaves.get(LeafId(i as u32)).source_range();
                        (r.start.buffer, r.start.offset, r.end.offset)
                    })
                    .collect(),
                future: hist.iter().any(|s| s.future),
                hist_clocks: hist_extra.len(),
                future_clock,
                live_calls: live_calls.iter().map(|l| l.0).collect(),
                end_cell: match &watch {
                    None => None,
                    Some((_, id, _)) => Some(
                        plan.signals
                            .get(id)
                            .ok_or_else(|| {
                                unsupported(plan, "internal error: a watched sequence with no cell")
                            })?
                            .slot,
                    ),
                },
            });
        }
    }
    Ok(specs)
}

/// One engine `emit_assertions` compiles for a plan: its assertion statement
/// (procedural or not), or a watcher of a sequence instance its procedure reads
/// the end point of (the instance, its cell id, its index in the block).
enum Job<'d> {
    Stmt(Statement<'d>, bool),
    Watch(Expression<'d>, SymbolId, usize),
}

struct Emitter<'a, 'ctx, 'd> {
    ctx: &'ctx Context,
    module: &'a Module<'ctx>,
    fns: &'a AccessorFns<'ctx>,
    plan: &'a ProcessLoweringPlan<'d>,
    row: &'a [(SymbolId, SignalSlot)],
    ir: &'a PropertyIr,
    leaves: &'a LeafTable<'d>,
    /// The captured values of a procedural assertion, with their slots.
    captured: &'a [(CaptureItem<'d>, LocalVarId)],
    /// The sampled value function calls of the property.
    hist: &'a [HistSite],
    /// The clocks a position row carries a history for: the assertion's own and
    /// the sampled value functions' ([`HistClock`]).
    total_clocks: usize,
    /// The tick functions get the position row (`AssertionSpec::tick_history`).
    tick_history: bool,
    /// Per leaf, the local-variable declarations of the automaton it belongs
    /// to: an end-point instance's frame has slots of its own past the
    /// enclosing automaton's (`leaf_owner_decls`).
    leaf_decls: Vec<Option<Vec<LocalVarDecl>>>,
    /// The clock variables read at clocks that are not all their block's event.
    mixed: &'a [MixedClockVar<'d>],
    /// The clock domain each leaf is evaluated in ([`leaf_domains`]).
    domains: std::collections::HashMap<LeafId, u32>,
}

impl<'a, 'ctx, 'd> Emitter<'a, 'ctx, 'd> {
    fn ob<'b>(&self, cx: &'b LowerCtx<'ctx, '_, '_>) -> OpBuilder<'b, 'ctx> {
        OpBuilder {
            ctx: self.ctx,
            b: &cx.b,
        }
    }

    /// A function `name` with `params`, its entry block positioned, and the
    /// lowering context for its body.
    fn begin(
        &self,
        name: &str,
        ret: inkwell::types::IntType<'ctx>,
        n_ptr_params: usize,
    ) -> (
        FunctionValue<'ctx>,
        LowerCtx<'ctx, 'd, 'a>,
        PointerValue<'ctx>,
    ) {
        let ptr_ty = self.ctx.ptr_type(AddressSpace::default());
        let params: Vec<_> = (0..n_ptr_params).map(|_| ptr_ty.into()).collect();
        let f = self
            .module
            .add_function(name, ret.fn_type(&params, false), None);
        f.get_nth_param(0).unwrap().set_name("handle");
        let entry = self.ctx.append_basic_block(f, "entry");
        let b = self.ctx.create_builder();
        b.position_at_end(entry);
        let handle = f.get_nth_param(0).unwrap().into_pointer_value();
        // A memory of the row is read from its sampled copy, a local array
        // ([`Self::shadow_memory`]), not through the accessor's live elements.
        let mut mem_signals = mem_signals_of(&self.plan.signals);
        for (id, _) in self.row {
            mem_signals.remove(id);
        }
        let cx = LowerCtx {
            ctx: self.ctx,
            b,
            repr: ValueRepr::FourState,
            locals: HashMap::new(),
            fn_sym: self.plan.fn_sym,
            module: self.module,
            mem_signals,
            mem_accessor: Some(MemAccessorCtx {
                handle,
                fns: self.fns,
            }),
            lvalue_ref: Default::default(),
            deferred_start: Default::default(),
            unbounded: Default::default(),
            coll_temp: Default::default(),
            iter: Default::default(),
            loop_exits: Default::default(),
            block_exits: Default::default(),
            write_through: None,
            cells: Default::default(),
            copy_out: Default::default(),
            ctor_this: Default::default(),
            decl_scale: Default::default(),
            inline_this: Default::default(),
            end_flags: Default::default(),
            specify_dest: Default::default(),
            elem_refs: Default::default(),
        };
        (f, cx, handle)
    }

    fn verify(&self, f: FunctionValue<'ctx>, what: &str) -> Result<(), LoweringError> {
        if f.verify(true) {
            Ok(())
        } else {
            Err(unsupported(
                self.plan,
                &format!("the {what} of a concurrent assertion failed LLVM verify"),
            ))
        }
    }

    /// The `j`th `u128` of the row `ptr`.
    fn row_entry(
        &self,
        cx: &LowerCtx<'ctx, '_, '_>,
        ptr: PointerValue<'ctx>,
        j: usize,
    ) -> IntValue<'ctx> {
        let idx = self.ctx.i64_type().const_int(j as u64, false);
        self.row_entry_at(cx, ptr, idx)
    }

    /// The `u128` of the row `ptr` at the run-time index `idx` (an `i64`).
    fn row_entry_at(
        &self,
        cx: &LowerCtx<'ctx, '_, '_>,
        ptr: PointerValue<'ctx>,
        idx: IntValue<'ctx>,
    ) -> IntValue<'ctx> {
        let i128_ty = self.ctx.i128_type();
        // SAFETY: `idx < row_len`, the length of every row the runtime passes.
        let p = unsafe {
            cx.b.build_in_bounds_gep(i128_ty, ptr, &[idx], "row_ptr")
                .unwrap()
        };
        cx.b.build_load(i128_ty, p, "row_raw")
            .unwrap()
            .into_int_value()
    }

    /// The first row word of the `j`th row signal.
    fn offset(&self, j: usize) -> usize {
        self.row[..j].iter().map(|(_, info)| row_words(info)).sum()
    }

    /// The number of words of one row.
    fn row_total(&self) -> usize {
        self.row.iter().map(|(_, info)| row_words(info)).sum()
    }

    /// Shadows signal `id` from its words at `base` of the row `ptr`: one word
    /// for a narrow signal; for a wide one, word `k` holds bits `64k..64k+63`
    /// (value in the low half, unknown plane in the high half).
    fn shadow_from_row(
        &self,
        cx: &mut LowerCtx<'ctx, '_, '_>,
        id: &SymbolId,
        info: &SignalSlot,
        ptr: PointerValue<'ctx>,
        base: usize,
    ) {
        if let SignalSlotClass::Memory { num_rows, .. } = info.class {
            let nw = elem_words(info);
            let i64t = self.ctx.i64_type();
            self.shadow_memory(cx, id, info, num_rows, &|cx, k| {
                // The element's first word: `base + k * nw`.
                let at =
                    cx.b.build_int_mul(k, i64t.const_int(nw as u64, false), "elem_at")
                        .unwrap();
                let at =
                    cx.b.build_int_add(at, i64t.const_int(base as u64, false), "elem_word")
                        .unwrap();
                if nw == 1 {
                    let raw = self.row_entry_at(cx, ptr, at);
                    build_fixed_to_packed(cx, raw, info.width)
                } else {
                    self.packed_from_row(cx, ptr, at, info.width)
                }
            });
            return;
        }
        let n = row_words(info);
        if n == 1 {
            let raw = self.row_entry(cx, ptr, base);
            self.shadow(cx, id, info, raw);
            return;
        }
        let w = info.width;
        let at = self.ctx.i64_type().const_int(base as u64, false);
        let packed = self.packed_from_row(cx, ptr, at, w);
        let slot = crate::types::entry_alloca_in(&cx.b, packed.get_type(), "sva_shadow");
        cx.b.build_store(slot, packed).unwrap();
        cx.locals.insert(id.clone(), (slot, w, info.signed));
    }

    /// The packed 4-state value (`2w` bits, value low, unknown plane high) of a
    /// `w`-bit value whose row words start at `base` of the row `ptr`: word `k`
    /// holds bits `64k..64k+63` (value in the low half, unknown plane in the
    /// high half).
    fn packed_from_row(
        &self,
        cx: &LowerCtx<'ctx, '_, '_>,
        ptr: PointerValue<'ctx>,
        base: IntValue<'ctx>,
        w: u32,
    ) -> IntValue<'ctx> {
        let n = w.div_ceil(64) as usize;
        let ob = self.ob(cx);
        let wt = ob.i_n(w);
        let i64t = self.ctx.i64_type();
        let i128t = self.ctx.i128_type();
        let mut val = wt.const_zero();
        let mut unk = wt.const_zero();
        for k in 0..n {
            let at =
                cx.b.build_int_add(base, i64t.const_int(k as u64, false), "w_at")
                    .unwrap();
            let word = self.row_entry_at(cx, ptr, at);
            let v = cx.b.build_int_truncate(word, i64t, "w_val").unwrap();
            let hi =
                cx.b.build_right_shift(word, i128t.const_int(64, false), false, "w_hi")
                    .unwrap();
            let u = cx.b.build_int_truncate(hi, i64t, "w_unk").unwrap();
            let sh = wt.const_int(64 * k as u64, false);
            let vz = cx.b.build_int_z_extend(v, wt, "w_vz").unwrap();
            let uz = cx.b.build_int_z_extend(u, wt, "w_uz").unwrap();
            let vs = cx.b.build_left_shift(vz, sh, "w_vs").unwrap();
            let us = cx.b.build_left_shift(uz, sh, "w_us").unwrap();
            val = cx.b.build_or(val, vs, "w_v").unwrap();
            unk = cx.b.build_or(unk, us, "w_u").unwrap();
        }
        let pt = ob.i_n(2 * w);
        let vz = cx.b.build_int_z_extend(val, pt, "w_pv").unwrap();
        let uz = cx.b.build_int_z_extend(unk, pt, "w_pu").unwrap();
        let us =
            cx.b.build_left_shift(uz, pt.const_int(u64::from(w), false), "w_pus")
                .unwrap();
        cx.b.build_or(vz, us, "w_packed").unwrap()
    }

    /// Primes every row signal's shadow from the row `ptr`.
    fn prime_row(&self, cx: &mut LowerCtx<'ctx, '_, '_>, ptr: PointerValue<'ctx>) {
        for (j, (id, info)) in self.row.iter().enumerate() {
            let base = self.offset(j);
            self.shadow_from_row(cx, id, info, ptr, base);
        }
    }

    /// Primes the hidden cells the sampled value function calls of the property
    /// read, from the position row `ptr` (`(1 + history_depth) * row_len`
    /// entries): the P cell of a signal is its sampled value at this tick (the
    /// row's own part), `S_k` its value `k + 1` ticks back
    /// ([`sv_sim_sim::sva::sampled::use_views`]).
    fn prime_history(&self, cx: &mut LowerCtx<'ctx, '_, '_>, ptr: PointerValue<'ctx>) {
        let len = self.row_total();
        let owner = self.plan.fn_sym.uid();
        let mut done: BTreeSet<SymbolId> = BTreeSet::new();
        // The row is the position's own, then `depth` rows per clock.
        let depth = self
            .hist
            .iter()
            .map(|s| s.depth as usize)
            .max()
            .unwrap_or(0);
        for site in self.hist {
            for sig in &site.args {
                // A signal outside the row (an automatic variable, ...) has no
                // history; lowering the call then fails loudly (`with_views`).
                let Some(j) = self.row.iter().position(|(id, _)| id == sig) else {
                    continue;
                };
                let info = &self.row[j].1;
                let base = self.offset(j);
                if done.insert(p_id(sig)) {
                    self.shadow_from_row(cx, &p_id(sig), info, ptr, base);
                }
                for k in 0..site.depth {
                    let id = s_id(&owner, &site.loc, sig, k);
                    if done.insert(id.clone()) {
                        let at = (1 + site.clock as usize * depth + k as usize) * len + base;
                        self.shadow_from_row(cx, &id, info, ptr, at);
                    }
                }
                // The next tick's row follows every clock's history.
                if site.future && done.insert(n_id(sig)) {
                    let at = (1 + self.total_clocks * depth) * len + base;
                    self.shadow_from_row(cx, &n_id(sig), info, ptr, at);
                }
            }
        }
    }

    /// Runs `body(cx, k)` for every memory row `k` in `0..num_rows` (`k` an
    /// `i64`): unrolled for a small memory, as a loop for a large one, so the
    /// code size does not grow with the memory.
    fn for_each_row(
        &self,
        cx: &LowerCtx<'ctx, '_, '_>,
        num_rows: u32,
        body: &dyn Fn(&LowerCtx<'ctx, '_, '_>, IntValue<'ctx>),
    ) {
        let i64t = self.ctx.i64_type();
        if num_rows <= UNROLLED_MEMORY_ROWS {
            for k in 0..u64::from(num_rows) {
                body(cx, i64t.const_int(k, false));
            }
            return;
        }
        let pre = cx.b.get_insert_block().unwrap();
        let f = pre.get_parent().unwrap();
        let head = self.ctx.append_basic_block(f, "mem_loop");
        let exit = self.ctx.append_basic_block(f, "mem_done");
        cx.b.build_unconditional_branch(head).unwrap();
        cx.b.position_at_end(head);
        let k = cx.b.build_phi(i64t, "mem_k").unwrap();
        k.add_incoming(&[(&i64t.const_zero(), pre)]);
        let kv = k.as_basic_value().into_int_value();
        body(cx, kv);
        let latch = cx.b.get_insert_block().unwrap();
        let next =
            cx.b.build_int_add(kv, i64t.const_int(1, false), "mem_next")
                .unwrap();
        k.add_incoming(&[(&next, latch)]);
        let more =
            cx.b.build_int_compare(
                inkwell::IntPredicate::ULT,
                next,
                i64t.const_int(u64::from(num_rows), false),
                "mem_more",
            )
            .unwrap();
        cx.b.build_conditional_branch(more, head, exit).unwrap();
        cx.b.position_at_end(exit);
    }

    /// Binds memory `id` to a local array of `num_rows` packed 4-state elements
    /// in storage order, element `k` being `elem(cx, k)` (`k` an `i64`): the
    /// array form an unpacked-array element select reads from a local
    /// ([`crate::arrays::Backing::Local`]).
    fn shadow_memory(
        &self,
        cx: &mut LowerCtx<'ctx, '_, '_>,
        id: &SymbolId,
        info: &SignalSlot,
        num_rows: u32,
        elem: &dyn Fn(&LowerCtx<'ctx, '_, '_>, IntValue<'ctx>) -> IntValue<'ctx>,
    ) {
        let row_ty = self.ob(cx).i_n(2 * info.width);
        let arr_ty = row_ty.array_type(num_rows);
        let arr = crate::types::entry_alloca_in(&cx.b, arr_ty, "sva_shadow_mem");
        let i32t = self.ctx.i32_type();
        let fill = |cx: &LowerCtx<'ctx, '_, '_>, k: IntValue<'ctx>| {
            let v = elem(cx, k);
            // SAFETY: `k < num_rows`, the array's length.
            let p = unsafe {
                cx.b.build_in_bounds_gep(arr_ty, arr, &[i32t.const_zero(), k], "mem_row")
                    .unwrap()
            };
            cx.b.build_store(p, v).unwrap();
        };
        self.for_each_row(cx, num_rows, &fill);
        cx.locals.insert(id.clone(), (arr, info.width, info.signed));
    }

    /// Primes every row signal's shadow from the live state.
    fn prime_live(
        &self,
        cx: &mut LowerCtx<'ctx, '_, '_>,
        handle: PointerValue<'ctx>,
        keep: Option<&BTreeSet<SymbolId>>,
    ) {
        for (id, info) in self.row {
            if keep.is_some_and(|k| !k.contains(id)) {
                continue;
            }
            if let SignalSlotClass::Memory { num_rows, .. } = info.class {
                self.shadow_memory(cx, id, info, num_rows, &|cx, k| {
                    crate::accessor::build_get_mem_word(
                        cx, self.fns, handle, info.slot, k, info.width,
                    )
                });
                continue;
            }
            if row_words(info) > 1 {
                let packed =
                    crate::accessor::build_get_wide(cx, self.fns, handle, info.slot, info.width);
                let slot = crate::types::entry_alloca_in(&cx.b, packed.get_type(), "sva_shadow");
                cx.b.build_store(slot, packed).unwrap();
                cx.locals
                    .insert(id.clone(), (slot, info.width, info.signed));
                continue;
            }
            let raw = build_get_scalar_raw(cx, self.fns, handle, info.slot);
            self.shadow(cx, id, info, raw);
        }
    }

    fn shadow(
        &self,
        cx: &mut LowerCtx<'ctx, '_, '_>,
        id: &SymbolId,
        info: &SignalSlot,
        raw: IntValue<'ctx>,
    ) {
        let packed = build_fixed_to_packed(cx, raw, info.width);
        let ptr = crate::types::entry_alloca_in(&cx.b, packed.get_type(), "sva_shadow");
        cx.b.build_store(ptr, packed).unwrap();
        cx.locals.insert(id.clone(), (ptr, info.width, info.signed));
    }

    /// Primes the end-point applications inside `leaf`'s expression (`a &&
    /// s.triggered`): each reads the 0/1 flag its `EndPoint` edge stored in
    /// `frame` (16.9.11), paired with the applications in pre-order
    /// ([`super::build::collect_end_points`], the builder's order) and looked up
    /// by the instance's source position ([`LowerCtx::end_flags`]).
    fn prime_end_flags(
        &self,
        cx: &mut LowerCtx<'ctx, '_, '_>,
        frame: PointerValue<'ctx>,
        leaf: LeafId,
        expr: Expression<'d>,
    ) {
        let flags = &self.leaves.locals_of(leaf).end_flags;
        if flags.is_empty() {
            return;
        }
        let mut calls = Vec::new();
        super::build::collect_end_points(expr, &mut calls);
        let i64_ty = self.ctx.i64_type();
        for ((_, inst), var) in calls.iter().zip(flags) {
            let idx = self.ctx.i32_type().const_int(u64::from(var.0), false);
            // SAFETY: the runtime passes a frame with a slot per local variable.
            let p = unsafe {
                cx.b.build_in_bounds_gep(i64_ty, frame, &[idx], "flag_ptr")
                    .unwrap()
            };
            let v = cx.b.build_load(i64_ty, p, "flag").unwrap().into_int_value();
            let bit =
                cx.b.build_int_compare(
                    inkwell::IntPredicate::NE,
                    v,
                    i64_ty.const_zero(),
                    "flag_bit",
                )
                .unwrap();
            let slot = crate::types::entry_alloca_in(&cx.b, self.ctx.bool_type(), "end_flag");
            cx.b.build_store(slot, bit).unwrap();
            cx.end_flags
                .borrow_mut()
                .insert(inst.source_range().start.offset, slot);
        }
    }

    /// Primes the sequence local variables `leaf` reads from `frame`.
    fn prime_locals(
        &self,
        cx: &mut LowerCtx<'ctx, '_, '_>,
        frame: PointerValue<'ctx>,
        leaf: LeafId,
    ) -> Result<(), LoweringError> {
        let l = self.leaves.locals_of(leaf);
        let i64_ty = self.ctx.i64_type();
        let load = |cx: &LowerCtx<'ctx, '_, '_>, var: LocalVarId| -> IntValue<'ctx> {
            let idx = self.ctx.i32_type().const_int(u64::from(var.0), false);
            // SAFETY: the runtime passes a frame with a slot per local variable.
            let p = unsafe {
                cx.b.build_in_bounds_gep(i64_ty, frame, &[idx], "frame_ptr")
                    .unwrap()
            };
            cx.b.build_load(i64_ty, p, "frame_val")
                .unwrap()
                .into_int_value()
        };
        let shadow = |cx: &mut LowerCtx<'ctx, '_, '_>,
                      var: LocalVarId|
         -> Result<(PointerValue<'ctx>, u32, bool), LoweringError> {
            let decl = self
                .leaf_decls
                .get(leaf.0 as usize)
                .and_then(|d| d.as_ref())
                .and_then(|d| d.get(var.0 as usize))
                .unwrap_or_else(|| self.ir.automaton.local_var(var));
            if decl.width == 0 {
                return Err(unsupported(
                    self.plan,
                    "a sequence local variable of no bits",
                ));
            }
            if decl.is_wide() {
                // A wide variable: its value limbs, then its unknown-plane limbs
                // (`sv_sim_sim::sva::wide`), are assembled into the packed
                // `[unk | val]` form an ordinary four-state value has.
                let n = decl.limbs() as u32;
                let ob = self.ob(cx);
                let plane_ty = ob.i_n(decl.width);
                // The limbs go through a stack buffer read back as one integer, so
                // assembling a plane is `n` stores, not `n` shift/or pairs of the
                // full width.
                let assemble = |cx: &LowerCtx<'ctx, '_, '_>, first: u32| -> IntValue<'ctx> {
                    let full = ob.i_n(64 * n);
                    let buf = crate::types::entry_alloca_in(&cx.b, i64_ty.array_type(n), "lv_buf");
                    for k in 0..n {
                        let limb = load(cx, LocalVarId(var.0 + first + k));
                        let idx = self.ctx.i32_type().const_int(u64::from(k), false);
                        // SAFETY: `k < n`, the buffer's length.
                        let p = unsafe {
                            cx.b.build_in_bounds_gep(i64_ty, buf, &[idx], "lv_slot")
                                .unwrap()
                        };
                        cx.b.build_store(p, limb).unwrap();
                    }
                    let whole = cx.b.build_load(full, buf, "lv_whole").unwrap();
                    inkwell::values::BasicValue::as_instruction_value(&whole)
                        .unwrap()
                        .set_alignment(8)
                        .unwrap();
                    let whole = whole.into_int_value();
                    if decl.width < 64 * n {
                        cx.b.build_int_truncate(whole, plane_ty, "lv_plane")
                            .unwrap()
                    } else {
                        whole
                    }
                };
                let val = assemble(cx, 0);
                let unk = assemble(cx, n);
                let packed = ob.pack(val, unk, decl.width, ValueRepr::FourState, decl.signed);
                let ptr = crate::types::entry_alloca_in(&cx.b, ob.i_n(decl.width * 2), "sva_local");
                cx.b.build_store(ptr, packed.llvm).unwrap();
                return Ok((ptr, decl.width, decl.signed));
            }
            let raw = load(cx, var);
            let ob = self.ob(cx);
            let val = if decl.width < 64 {
                cx.b.build_int_truncate(raw, ob.i_n(decl.width), "lv_val")
                    .unwrap()
            } else {
                raw
            };
            let packed_ty = ob.i_n(decl.width * 2);
            let wide =
                cx.b.build_int_z_extend(val, packed_ty, "lv_packed")
                    .unwrap();
            let ptr = crate::types::entry_alloca_in(&cx.b, packed_ty, "sva_local");
            cx.b.build_store(ptr, wide).unwrap();
            Ok((ptr, decl.width, decl.signed))
        };
        for (sym, var) in &l.reads {
            let s = shadow(cx, *var)?;
            // A fixed-size unpacked array local (16.10) holds its flat stored bits; element
            // selects and whole-array reads go through a row buffer cut out of them.
            if let Some(shape) = sym
                .declared_type()
                .as_ref()
                .and_then(crate::arrays::array_shape)
            {
                let (ptr, width, signed) = s;
                let packed =
                    cx.b.build_load(self.ob(cx).i_n(width * 2), ptr, "arr_local_flat")
                        .unwrap()
                        .into_int_value();
                let flat = PackedValue {
                    llvm: packed,
                    width,
                    repr: ValueRepr::FourState,
                    signed,
                };
                let rows = crate::arrays::rows_from_flat(cx, flat, &shape, "sva_local_rows")?;
                cx.locals.insert(
                    sym.uid(),
                    (
                        rows,
                        crate::types::TypeWidth::value_width(&shape.elem),
                        shape.elem.is_signed(),
                    ),
                );
                continue;
            }
            cx.locals.insert(sym.uid(), s);
        }
        // The values a procedural assertion instance captured.
        let items: Vec<CaptureItem<'d>> = self.captured.iter().map(|(i, _)| i.clone()).collect();
        for k in items_used_by(&items, self.leaves.get(leaf)) {
            let (item, var) = &self.captured[k];
            let s = shadow(cx, *var)?;
            cx.locals.insert(item.key.clone(), s);
        }
        if let Some(var) = l.lvalue {
            let (ptr, width, signed) = shadow(cx, var)?;
            let packed_ty = self.ob(cx).i_n(width * 2);
            let v =
                cx.b.build_load(packed_ty, ptr, "lvalue_ref")
                    .unwrap()
                    .into_int_value();
            cx.lvalue_ref.set(Some(LoweredValue::Packed(PackedValue {
                llvm: v,
                width,
                repr: ValueRepr::FourState,
                signed,
            })));
        }
        Ok(())
    }

    fn snap(&self, name: &str) -> Result<(), LoweringError> {
        let ptr_ty = self.ctx.ptr_type(AddressSpace::default());
        let f = self.module.add_function(
            name,
            self.ctx
                .void_type()
                .fn_type(&[ptr_ty.into(), ptr_ty.into()], false),
            None,
        );
        f.get_nth_param(0).unwrap().set_name("handle");
        let entry = self.ctx.append_basic_block(f, "entry");
        let (_, cx, handle) = {
            let b = self.ctx.create_builder();
            b.position_at_end(entry);
            let handle = f.get_nth_param(0).unwrap().into_pointer_value();
            let cx = LowerCtx {
                ctx: self.ctx,
                b,
                repr: ValueRepr::FourState,
                locals: HashMap::new(),
                fn_sym: self.plan.fn_sym,
                module: self.module,
                mem_signals: Default::default(),
                mem_accessor: None,
                lvalue_ref: Default::default(),
                deferred_start: Default::default(),
                unbounded: Default::default(),
                coll_temp: Default::default(),
                iter: Default::default(),
                loop_exits: Default::default(),
                block_exits: Default::default(),
                write_through: None,
                cells: Default::default(),
                copy_out: Default::default(),
                ctor_this: Default::default(),
                decl_scale: Default::default(),
                inline_this: Default::default(),
                end_flags: Default::default(),
                specify_dest: Default::default(),
                elem_refs: Default::default(),
            };
            (f, cx, handle)
        };
        let out = f.get_nth_param(1).unwrap().into_pointer_value();
        let i128_ty = self.ctx.i128_type();
        let i64t = self.ctx.i64_type();
        let store = |idx: IntValue<'ctx>, raw: IntValue<'ctx>| {
            // SAFETY: `out` has `row_len` entries.
            let p = unsafe {
                cx.b.build_in_bounds_gep(i128_ty, out, &[idx], "out_ptr")
                    .unwrap()
            };
            let st = cx.b.build_store(p, raw).unwrap();
            st.set_alignment(8).unwrap();
        };
        for (j, (_, info)) in self.row.iter().enumerate() {
            let base = self.offset(j);
            let n = row_words(info);
            // A wide value (a wide signal or one element of a memory): word `k`
            // is bits `64k..64k+63` of the value (low half) and of the unknown
            // plane (high half). `packed` is the `2w`-bit packed 4-state value.
            let split = |cx: &LowerCtx<'ctx, '_, '_>,
                         packed: IntValue<'ctx>,
                         w: u32,
                         at: IntValue<'ctx>| {
                let pt = packed.get_type();
                let wt = self.ob(cx).i_n(w);
                let val = cx.b.build_int_truncate(packed, wt, "s_val").unwrap();
                let hi = cx
                    .b
                    .build_right_shift(packed, pt.const_int(u64::from(w), false), false, "s_hi")
                    .unwrap();
                let unk = cx.b.build_int_truncate(hi, wt, "s_unk").unwrap();
                for k in 0..w.div_ceil(64) as usize {
                    let sh = wt.const_int(64 * k as u64, false);
                    let v = cx.b.build_right_shift(val, sh, false, "s_vk").unwrap();
                    let u = cx.b.build_right_shift(unk, sh, false, "s_uk").unwrap();
                    let v = if w > 64 {
                        cx.b.build_int_truncate(v, i64t, "s_v64").unwrap()
                    } else {
                        v
                    };
                    let u = if w > 64 {
                        cx.b.build_int_truncate(u, i64t, "s_u64").unwrap()
                    } else {
                        u
                    };
                    let vz = cx.b.build_int_z_extend(v, i128_ty, "s_vz").unwrap();
                    let uz = cx.b.build_int_z_extend(u, i128_ty, "s_uz").unwrap();
                    let us =
                        cx.b.build_left_shift(uz, i128_ty.const_int(64, false), "s_us")
                            .unwrap();
                    let word =
                        cx.b.build_int_add(at, i64t.const_int(k as u64, false), "s_at")
                            .unwrap();
                    store(word, cx.b.build_or(vz, us, "s_word").unwrap());
                }
            };
            if let SignalSlotClass::Memory { num_rows, .. } = info.class {
                // Every element takes its words in turn, like a wide signal.
                let nw = elem_words(info);
                self.for_each_row(&cx, num_rows, &|cx, k| {
                    let packed = crate::accessor::build_get_mem_word(
                        cx, self.fns, handle, info.slot, k, info.width,
                    );
                    let at =
                        cx.b.build_int_mul(k, i64t.const_int(nw as u64, false), "elem_at")
                            .unwrap();
                    let at =
                        cx.b.build_int_add(at, i64t.const_int(base as u64, false), "elem_word")
                            .unwrap();
                    split(cx, packed, info.width, at);
                });
                continue;
            }
            if n == 1 {
                let raw = build_get_scalar_raw(&cx, self.fns, handle, info.slot);
                store(i64t.const_int(base as u64, false), raw);
                continue;
            }
            let w = info.width;
            let packed = crate::accessor::build_get_wide(&cx, self.fns, handle, info.slot, w);
            split(&cx, packed, w, i64t.const_int(base as u64, false));
        }
        cx.b.build_return(None).unwrap();
        self.verify(f, "row snapshot")
    }

    /// The function of `leaf`. `live` makes the `_lv` form (16.12) for a leaf
    /// the engine evaluates on the live state: its signals are read from the
    /// state, the sampled value functions from `row`, a position row.
    fn leaf(
        &self,
        name: &str,
        leaf: LeafId,
        role: LeafRole,
        live: bool,
    ) -> Result<(), LoweringError> {
        match (role, self.leaves.limb_of(leaf)) {
            (LeafRole::Value, Some(sel)) => self.limb_leaf(name, leaf, sel, live),
            _ => self.leaf_fn(name, leaf, role, live, None),
        }
    }

    /// A limb leaf of a wide local variable or call argument ([`LimbSel`]): a
    /// wrapper that calls the group's shared function (lowered once, by the
    /// group's first leaf) into a stack buffer and returns its word. Lowering the
    /// right-hand side once per assignment rather than once per limb keeps code
    /// generation linear in the width.
    fn limb_leaf(
        &self,
        name: &str,
        leaf: LeafId,
        sel: LimbSel,
        live: bool,
    ) -> Result<(), LoweringError> {
        let base = name.rsplit_once("_l").map_or(name, |(b, _)| b);
        let wname = format!("{base}_w{}{}", sel.group, if live { "v" } else { "" });
        let n = sel.width.div_ceil(64);
        let wide = match self.module.get_function(&wname) {
            Some(w) => w,
            None => {
                self.leaf_fn(&wname, leaf, LeafRole::Value, live, Some(sel))?;
                self.module.get_function(&wname).unwrap()
            }
        };
        let (f, cx, handle) = self.begin(name, self.ctx.i64_type(), 3);
        let row = f.get_nth_param(1).unwrap().into_pointer_value();
        let frame = f.get_nth_param(2).unwrap().into_pointer_value();
        let i64_ty = self.ctx.i64_type();
        let buf = crate::types::entry_alloca_in(&cx.b, i64_ty.array_type(2 * n), "limbs");
        cx.b.build_call(
            wide,
            &[handle.into(), row.into(), frame.into(), buf.into()],
            "wide",
        )
        .unwrap();
        let at = if sel.unknown {
            n + sel.index
        } else {
            sel.index
        };
        // SAFETY: `at < 2 * n`, the buffer's length.
        let p = unsafe {
            cx.b.build_in_bounds_gep(
                i64_ty,
                buf,
                &[self.ctx.i32_type().const_int(u64::from(at), false)],
                "limb_ptr",
            )
            .unwrap()
        };
        let w = cx.b.build_load(i64_ty, p, "limb").unwrap();
        cx.b.build_return(Some(&w)).unwrap();
        self.verify(f, "limb leaf")
    }

    /// The function of `leaf`; with `wide` (a limb leaf's [`LimbSel`]) it takes a
    /// fourth parameter, a buffer of `2 * ceil(width / 64)` words that receives
    /// the value fitted to the variable (value limbs, then unknown limbs), and
    /// returns 0.
    fn leaf_fn(
        &self,
        name: &str,
        leaf: LeafId,
        role: LeafRole,
        live: bool,
        wide: Option<LimbSel>,
    ) -> Result<(), LoweringError> {
        let (f, mut cx, handle) =
            self.begin(name, self.ctx.i64_type(), 3 + usize::from(wide.is_some()));
        let row = f.get_nth_param(1).unwrap().into_pointer_value();
        let frame = f.get_nth_param(2).unwrap().into_pointer_value();
        if live {
            // A leaf with no sampled value function reads only its own signals
            // from the state (the rest of the row is not fetched).
            let expr = self.leaves.get(leaf);
            // `$inferred_disable` (17.4) reads the `default disable iff` signal of the
            // instantiation context, which `expr` does not name: fetch the whole row.
            let own: Option<BTreeSet<SymbolId>> = if sampled_calls_in(self.plan, expr)?.is_empty()
                && !mentions_inferred_disable(expr)
            {
                let (r, ..) = row_signals(self.plan, &[expr], &[], &[], &[])?;
                Some(r.into_iter().map(|(id, _)| id).collect())
            } else {
                None
            };
            self.prime_live(&mut cx, handle, own.as_ref());
        } else {
            self.prime_row(&mut cx, row);
        }
        self.prime_history(&mut cx, row);
        self.rebind_mixed_clock_vars(&mut cx, leaf);
        self.prime_locals(&mut cx, frame, leaf)?;
        let expr = self.leaves.get(leaf);
        self.prime_end_flags(&mut cx, frame, leaf, expr);
        let i64_ty = self.ctx.i64_type();
        let out = match role {
            LeafRole::Bool => {
                let bit = if self.leaves.is_negated(leaf) {
                    lower_negated_condition(&cx, expr)?
                } else {
                    lower_condition(&cx, expr)?
                };
                cx.b.build_int_z_extend(bit, i64_ty, "leaf_i64").unwrap()
            }
            LeafRole::Value => {
                // A `real` value (a `realtime` local's new value, 16.10) is kept as its IEEE
                // bits, the local variable's slot being a plain `i64`.
                // A fixed-size unpacked array local's new value is the array's flat stored
                // bits (`arrays::pack_array_value`).
                // A queue / dynamic / associative array local's new value is the collection's
                // 64-bit handle: the row's snapshot (`AssertionSpec::coll_words`).
                let v = if expr.expr_type().is_some_and(|t| {
                    t.is_unpacked_array() && !sv_sim_sim::state::storage::is_collection(&t)
                }) {
                    LoweredValue::Packed(crate::arrays::pack_array_value(&cx, expr)?)
                } else {
                    lower_expr(&cx, expr)?
                };
                let v = match v {
                    LoweredValue::Real(rv) => crate::real::real_to_bits(&cx, rv, 64),
                    // A `string` local's new value is the string's 64-bit id.
                    LoweredValue::Str(s) => {
                        cx.b.build_return(Some(&s.llvm)).unwrap();
                        return self.verify(f, "leaf");
                    }
                    // A class handle local (6.14) holds the object id and one reference to
                    // it, so the object outlives its other references (a frame slot is
                    // never released: a held object that is never freed is harmless, and a
                    // retain of `null` is a no-op).
                    LoweredValue::Packed(pv) if expr.expr_type().is_some_and(|t| t.is_class()) => {
                        crate::classes::retain_handle(&cx, self.ob(&cx).lane_val(pv));
                        pv
                    }
                    other => other.into_packed(
                        "a string or >128-bit value in an assertion",
                        &self.plan.fn_sym,
                    )?,
                };
                match wide {
                    Some(sel) => {
                        let out = f.get_nth_param(3).unwrap().into_pointer_value();
                        self.store_planes(&cx, v, sel, out);
                        self.ctx.i64_type().const_zero()
                    }
                    None => self.to_i64(&cx, v)?,
                }
            }
            LeafRole::Unused => unreachable!("an unused leaf gets no function"),
        };
        cx.b.build_return(Some(&out)).unwrap();
        self.verify(f, "leaf")
    }

    /// A leaf in a clock domain that is not a mixed clock variable's block event
    /// reads the block's last sample, not the source's Preponed value (16.18).
    fn rebind_mixed_clock_vars(&self, cx: &mut LowerCtx<'ctx, '_, '_>, leaf: LeafId) {
        let Some(dom) = self.domains.get(&leaf) else {
            return;
        };
        let Some(clock) = self.leaves.clock_event(ClockId(*dom)) else {
            return;
        };
        for m in self.mixed {
            if !super::build::events_equivalent(clock, m.event)
                && let Some(cell) = cx.locals.get(&m.sample).copied()
            {
                cx.locals.insert(m.id.clone(), cell);
            }
        }
    }

    /// The leaf of a `default disable iff` (T31): the signal it names, true
    /// where the (possibly negated) condition is KNOWN true.
    fn default_disable_leaf(
        &self,
        name: &str,
        d: &DefaultDisable<'d>,
        live: bool,
    ) -> Result<(), LoweringError> {
        let (f, mut cx, handle) = self.begin(name, self.ctx.i64_type(), 3);
        let row = f.get_nth_param(1).unwrap().into_pointer_value();
        if live {
            // The `_lv` form reads just the one or two signals the condition names.
            let keep: BTreeSet<SymbolId> = [Some(d.signal.uid()), d.second.map(|(s, _)| s.uid())]
                .into_iter()
                .flatten()
                .collect();
            self.prime_live(&mut cx, handle, Some(&keep));
        } else {
            self.prime_row(&mut cx, row);
        }
        // One operand: true where the (possibly negated) signal is KNOWN true.
        let operand = |signal: &Symbol<'d>, negate: bool, pred: TermPred| {
            let (slot, width, signed) = cx.locals.get(&signal.uid()).copied().ok_or_else(|| {
                unsupported(
                    self.plan,
                    &format!(
                        "the `default disable iff` signal `{}` is not a module signal an \
                         assertion can read",
                        signal.name()
                    ),
                )
            })?;
            let ty = self.ob(&cx).i_n(width * 2);
            let raw = cx.b.build_load(ty, slot, "dd_ld").unwrap().into_int_value();
            let pv = PackedValue {
                llvm: raw,
                width,
                repr: cx.repr,
                signed,
            };
            let ob = self.ob(&cx);
            // `known & (value-lane test)`: a bit select or `==` is known only
            // where its bits carry no x/z, and `negate` asks for known-false.
            let tested = |val_test: IntValue<'ctx>, unk_zero: IntValue<'ctx>| {
                let t = if negate {
                    cx.b.build_not(val_test, "dd_not").unwrap()
                } else {
                    val_test
                };
                cx.b.build_and(unk_zero, t, "dd_known").unwrap()
            };
            Ok::<_, LoweringError>(match pred {
                TermPred::Whole if negate => is_definitely_false(self.ctx, &cx.b, pv),
                TermPred::Whole => is_definitely_true(self.ctx, &cx.b, pv),
                TermPred::Bit(pos) => {
                    let ity = ob.i_n(width);
                    let sh = ity.const_int(u64::from(pos), false);
                    let bit_of = |v: IntValue<'ctx>| {
                        let s = cx.b.build_right_shift(v, sh, false, "dd_sh").unwrap();
                        cx.b.build_int_truncate(s, self.ctx.bool_type(), "dd_b")
                            .unwrap()
                    };
                    let unk_zero = cx.b.build_not(bit_of(ob.lane_unk(pv)), "dd_unk0").unwrap();
                    tested(bit_of(ob.lane_val(pv)), unk_zero)
                }
                TermPred::Eq(c) => {
                    let ity = ob.i_n(width);
                    let unk_zero =
                        cx.b.build_int_compare(
                            inkwell::IntPredicate::EQ,
                            ob.lane_unk(pv),
                            ity.const_zero(),
                            "dd_unk0",
                        )
                        .unwrap();
                    let eq =
                        cx.b.build_int_compare(
                            inkwell::IntPredicate::EQ,
                            ob.lane_val(pv),
                            ity.const_int(c, false),
                            "dd_eq",
                        )
                        .unwrap();
                    tested(eq, unk_zero)
                }
            })
        };
        let mut bit = operand(&d.signal, d.negate, d.pred)?;
        if let Some((sig2, neg2)) = &d.second {
            let b2 = operand(sig2, *neg2, d.second_pred)?;
            bit = if d.and {
                cx.b.build_and(bit, b2, "dd_and").unwrap()
            } else {
                cx.b.build_or(bit, b2, "dd_or").unwrap()
            };
        }
        let out =
            cx.b.build_int_z_extend(bit, self.ctx.i64_type(), "dd_i64")
                .unwrap();
        cx.b.build_return(Some(&out)).unwrap();
        self.verify(f, "default disable leaf")
    }

    /// Stores the four-state value `v` fitted to a wide variable ([`LimbSel`]) to
    /// `out`: `v` is extended (by its own signedness, 10.7) or truncated to the
    /// variable's width, then its value plane and its unknown plane are stored as
    /// `ceil(width / 64)` words each, zero above the width.
    fn store_planes(
        &self,
        cx: &LowerCtx<'ctx, '_, '_>,
        v: PackedValue<'ctx>,
        sel: LimbSel,
        out: PointerValue<'ctx>,
    ) {
        let ob = self.ob(cx);
        let fitted = match v.width.cmp(&sel.width) {
            std::cmp::Ordering::Less => ob.extend4(v, sel.width, v.signed),
            std::cmp::Ordering::Equal => v,
            std::cmp::Ordering::Greater => ob.truncate4(v, sel.width),
        };
        let n = sel.width.div_ceil(64);
        let full = ob.i_n(64 * n);
        let i64_ty = self.ctx.i64_type();
        for (plane, first) in [(ob.lane_val(fitted), 0), (ob.lane_unk(fitted), n)] {
            let plane = if sel.width < 64 * n {
                cx.b.build_int_z_extend(plane, full, "plane_ext").unwrap()
            } else {
                plane
            };
            // SAFETY: `first + n <= 2 * n`, the buffer's length.
            let p = unsafe {
                cx.b.build_in_bounds_gep(
                    i64_ty,
                    out,
                    &[self.ctx.i32_type().const_int(u64::from(first), false)],
                    "plane_ptr",
                )
                .unwrap()
            };
            cx.b.build_store(p, plane)
                .unwrap()
                .set_alignment(8)
                .unwrap();
        }
    }

    /// The value lane of `v` as an `i64`: sign-extended when `v` is signed.
    fn to_i64(
        &self,
        cx: &LowerCtx<'ctx, '_, '_>,
        v: PackedValue<'ctx>,
    ) -> Result<IntValue<'ctx>, LoweringError> {
        if v.width > 64 {
            return Err(unsupported(
                self.plan,
                "a value wider than 64 bits as a case selector, a by-value call argument or \
                 another operand the engine keeps as one `i64` in an assertion is not \
                 executable yet",
            ));
        }
        let val = self.ob(cx).lane_val(v);
        let i64_ty = self.ctx.i64_type();
        Ok(if v.width == 64 {
            val
        } else if v.signed {
            cx.b.build_int_s_extend(val, i64_ty, "v_sext").unwrap()
        } else {
            cx.b.build_int_z_extend(val, i64_ty, "v_zext").unwrap()
        })
    }

    /// The value a clocking event term watches, from the state `cx` is primed
    /// with: its signal expression, or, for a sequence clock (16.5.2), the
    /// sequence's watcher cell, which changes at every end point.
    fn clock_value(
        &self,
        cx: &LowerCtx<'ctx, 'd, 'a>,
        ev: &ClockEvent<'d>,
        what: &str,
    ) -> Result<crate::value::PackedValue<'ctx>, LoweringError> {
        if !is_sequence_clock(ev) {
            return lower_expr(cx, ev.signal)?.into_packed(what, &self.plan.fn_sym);
        }
        let id = sequence_clock_id(self.plan, ev)?;
        let &(ptr, width, signed) = cx.locals.get(&id).ok_or_else(|| {
            unsupported(
                self.plan,
                "internal error: a sequence clock's cell is not primed",
            )
        })?;
        let ty = crate::types::int_type(self.ctx, width * 2);
        let v =
            cx.b.build_load(ty, ptr, "seq_clock")
                .unwrap()
                .into_int_value();
        Ok(crate::value::PackedValue {
            llvm: v,
            width,
            repr: cx.repr,
            signed,
        })
    }

    /// The clock's tick test: the OR of its terms' events, each computed from the
    /// previous row (the term's Preponed values) and the live state.
    /// `gate` is a `$past` gating expression (16.9.3), sampled in the previous
    /// row like an `iff`; the clock ticks only where it is true.
    fn tick(
        &self,
        name: &str,
        terms: &[ClockEvent<'d>],
        gate: Option<Expression<'d>>,
    ) -> Result<(), LoweringError> {
        let (f, mut cx, handle) = self.begin(name, self.ctx.i8_type(), 2);
        let prev_row = f.get_nth_param(1).unwrap().into_pointer_value();
        let what = "a clocking event on a real, string or >128-bit value";
        // Every term's previous value and `iff` come from the previous row, so
        // all are lowered before the live state replaces it.
        self.prime_row(&mut cx, prev_row);
        if self.tick_history {
            self.prime_history(&mut cx, prev_row);
        }
        let gate = match gate {
            Some(g) => Some(lower_condition(&cx, g)?),
            None => None,
        };
        let mut prevs = Vec::with_capacity(terms.len());
        for ev in terms {
            let prev = self.clock_value(&cx, ev, what)?;
            let iff = match ev.iff {
                Some(c) => Some(lower_condition(&cx, c)?),
                None => None,
            };
            prevs.push((prev, iff));
        }
        self.prime_live(&mut cx, handle, None);
        let mut tick = self.ctx.bool_type().const_zero();
        for (ev, (prev, iff)) in terms.iter().zip(prevs) {
            let cur = self.clock_value(&cx, ev, what)?;
            let mut term = edge_occurred(&cx, ev.edge, prev, cur);
            if let Some(c) = iff {
                term = cx.b.build_and(term, c, "tick_iff").unwrap();
            }
            tick = cx.b.build_or(tick, term, "tick_or").unwrap();
        }
        if let Some(g) = gate {
            tick = cx.b.build_and(tick, g, "tick_gate").unwrap();
        }
        let ext =
            cx.b.build_int_z_extend(tick, self.ctx.i8_type(), "tick_i8")
                .unwrap();
        cx.b.build_return(Some(&ext)).unwrap();
        self.verify(f, "clock tick test")
    }

    fn case_pair(&self, name: &str, sel: LeafId, lab: LeafId) -> Result<(), LoweringError> {
        let (f, mut cx, _handle) = self.begin(name, self.ctx.i8_type(), 3);
        let row = f.get_nth_param(1).unwrap().into_pointer_value();
        let frame = f.get_nth_param(2).unwrap().into_pointer_value();
        self.prime_row(&mut cx, row);
        self.prime_history(&mut cx, row);
        self.prime_locals(&mut cx, frame, sel)?;
        self.prime_locals(&mut cx, frame, lab)?;
        let what = "a real, string or >128-bit case item in an assertion";
        let a = lower_expr(&cx, self.leaves.get(sel))?.into_packed(what, &self.plan.fn_sym)?;
        let b = lower_expr(&cx, self.leaves.get(lab))?.into_packed(what, &self.plan.fn_sym)?;
        let w = a.width.max(b.width);
        let ob = self.ob(&cx);
        let (a, b) = (ob.extend4(a, w, a.signed), ob.extend4(b, w, b.signed));
        let a = ob.pack(ob.lane_val(a), ob.lane_unk(a), w, cx.repr, false);
        let b = ob.pack(ob.lane_val(b), ob.lane_unk(b), w, cx.repr, false);
        let same = same_value(&cx, a, b);
        let ext =
            cx.b.build_int_z_extend(same, self.ctx.i8_type(), "case_i8")
                .unwrap();
        cx.b.build_return(Some(&ext)).unwrap();
        self.verify(f, "case comparison")
    }
}