vj-codegen 0.1.0

//! SV-B (T19-T26): the property builder -- 16.12's property expressions lowered
//! to a [`PropertyIr`], a DAG of [`Prop`] operators over ONE shared sequence
//! automaton (see `sv_sim_sim::sva::property` for the IR and for the reference
//! evaluator that defines what every node means).
//!
//! [`build_property`] is [`super::build_automaton`]'s sibling: it takes the same
//! root (the `Clocking` wrapper stripped by the caller, its event passed as
//! `root_clock`), builds every SEQUENCE operand with the sequence builder of
//! [`super`] into the property's one automaton (an entry state per sequence, a
//! `Match` self-loop on every exit), and every PROPERTY operator as a [`Prop`]
//! node here.
//!
//! # Sequence or property
//!
//! 16.12.1 draws the line: a `sequence_expr` is a Boolean, a `##`/repetition
//! chain, `first_match`, a sequence instance, or `and`/`or`/`intersect`/
//! `throughout`/`within` of sequences; everything else is a property expression.
//! `and`/`or` are the one ambiguity -- `a ##1 b and c ##1 d` is a sequence and
//! `a ##1 b and (c |-> d)` a property -- resolved by looking at the operands:
//! the operator is a sequence operator iff both are sequences (16.12.5, 16.12.4).
//! A sequence in a property position becomes a [`Prop::Seq`] after the
//! nondegeneracy check of 16.12.22(a).
//!
//! # Derived operators
//!
//! The IR keeps the primitives of Annex F.5 and the builder rewrites the rest
//! with the equivalences the LRM states: `implies` (F.3.4.3) is `not p1 or p2`,
//! `iff` is `(p1 implies p2) and (p2 implies p1)`, `until_with` is
//! `p until (p and q)`, and the followed-by operators are the duals of
//! implication, `r #-# p = not (r |-> not p)` and `r #=# p = not (r |=> not p)`
//! (16.12.9). The strong/weak forms of `nexttime`, `always`, `eventually` and
//! `until` share one evaluation rule (the verdict is judged at the strong or the
//! weak tail, F.5.3.2) and keep their flag for the legality checks.
//!
//! # Property instances and local variables
//!
//! A named property instance is expanded in place like a named sequence
//! ([`super::enter_instance`]), with the formals bound for the folding of
//! `##`/`[...]` bounds. A property's local variables and `local input` formals
//! share the sequence automaton's slot table; their initialisation is a
//! [`Prop::Let`] around the body. Only `|->`, `|=>`, `#-#` and `#=#` carry the
//! antecedent's local variables to the consequent (16.12.19, F.5.4): every other
//! operator hands each operand the variables that flowed into the operator and
//! lets nothing out.
//!
//! # Recursive properties (16.12.17, F.7)
//!
//! A recursive instance is not expanded again: it becomes a [`Prop::Call`] of the
//! [`PropDecl`] of the expansion it recurses into. Two expansions of one
//! declaration are the same body iff every NON-local formal is bound to the same
//! expression (a property, sequence or untyped formal is substituted into the
//! body, so the body is a function of those actuals); only the `local input`
//! formals vary at run time, and a call rebinds exactly those slots. An instance
//! is recursive iff its declaration reaches the declaration it is written in in the
//! dependency digraph of F.7 (an edge `p -> q` for every instance of `q` written in
//! `p`'s declaration, discovered as the expansion proceeds); it then calls the
//! innermost enclosing expansion with the same non-local actuals, and an
//! instance whose actuals are a new binding (`alt(y, x)` inside `alt(x, y)`) is
//! expanded once as a new variant, which closes after finitely many bindings
//! because restriction 4 allows only a forwarded formal or an expression over no
//! formal. The four restrictions of the subclause are enforced here:
//!
//! 1. `not` (and `implies`, `iff`, `#-#`, `#=#`, which are defined through it) and
//!    the strong operators cannot be applied to an operand that contains a call;
//! 2. `disable iff` cannot be in a recursive declaration;
//! 3. every call is after a positive guaranteed advance in time since the
//!    expansion it calls began (`Pb::adv`, which is the weight of F.7's edges
//!    summed along the path, so the check is the positive-cycle-sum rule);
//! 4. a non-local actual of a recursive instance is a formal of the enclosing
//!    declaration or mentions none.
use std::collections::{BTreeMap, BTreeSet, BinaryHeap};
use std::ops::Range;

use sv_lang::kinds::{AssertionExprKind, ExpressionKind};
use sv_lang::nodes::{
    AcceptOnPropertyExprSyntax, IdentifierNameSyntax, SelectorSyntax, StrongWeakPropertyExprSyntax,
    UnaryPropertyExprSyntax, UnarySelectPropertyExprSyntax,
};
use sv_lang::{ArgumentDirection, AssertionExpr, AstNode, Expression, SemNode, Symbol};

use sv_sim_sim::sva::ir::{
    self, AbortMode, ClockId, LeafId, LocalVarId, ThreadStateId, Transition,
};
use sv_sim_sim::sva::property::{
    CaseArm, DeclId, NvRule, Prop, PropDecl, PropId, PropertyIr, SeqRef, SequenceClass, Strength,
    classify_sequence,
};

use super::super::op::{AssertionBinaryOp as B, AssertionUnaryOp as U, Op, peel_property_parens};
use super::super::ranges;
use super::super::trees::{Trees, key};
use super::{
    LeafTable, ScopeVar, Span, actual_syntax, add_match_edges, blank_automaton, build_node,
    collect_end_points, collect_local_reads, enter_instance, formal_reference_origin,
    leave_instance, prune_from,
};
use crate::error::LoweringError;

/// Builds the property rooted at `root` (see the module doc comment for the
/// conventions, and [`super::build_automaton`] for `root_clock`).
///
/// Every failure is a [`LoweringError`] naming the LRM rule or the later task
/// that owns the construct.
pub fn build_property<'d>(
    root: AssertionExpr<'d>,
    root_clock: Option<SemNode<'d>>,
    tree: Trees<'_>,
    scope: &Symbol<'d>,
) -> Result<(PropertyIr, LeafTable<'d>), LoweringError> {
    build_property_as(root, root_clock, tree, scope, false, false, None)
}

/// [`build_property`] for the root of a `cover sequence` statement when
/// `cover_sequence` is set: the root is a sequence expression, not a property,
/// so the 16.12.22 rules on a sequence "used as a property" (nondegenerate, no
/// empty match) do not apply to it (16.14.3: the statement counts the matches of
/// the sequence, whatever they are).
pub fn build_property_as<'d>(
    root: AssertionExpr<'d>,
    root_clock: Option<SemNode<'d>>,
    tree: Trees<'_>,
    scope: &Symbol<'d>,
    cover_sequence: bool,
    root_inferred: bool,
    checker_frame: Option<ranges::FormalFrame>,
) -> Result<(PropertyIr, LeafTable<'d>), LoweringError> {
    let mut leaves = LeafTable::new(root_clock);
    leaves.root_inferred = root_inferred;
    if let Some(f) = checker_frame {
        leaves.env.push(f);
    }
    leaves.future_gclk = crate::sva::gclk::check(root, scope)?;
    let mut pb = Pb {
        a: blank_automaton(),
        leaves,
        props: Vec::new(),
        has_call: Vec::new(),
        nv_rules: Vec::new(),
        decls: Vec::new(),
        frames: Vec::new(),
        edges: BTreeSet::new(),
        sites: BTreeMap::new(),
        adv: 0,
        top: true,
        cover_sequence,
        seq_top: false,
        disable: None,
        tree,
        scope: *scope,
    };
    let root = pb.build_prop(root.as_sem_node())?;
    Ok(pb.finish(root))
}

/// The IR of a watcher of sequence instance `inst` (`sva::endpoint`): the
/// instance as a `cover sequence` root, so its engine reports one match at every
/// nonempty end point (16.9.11). `root_clock` is the clock of the reading
/// procedure (16.14.6) or the default clocking, for an instance with none of its
/// own.
pub fn build_sequence_watcher<'d>(
    inst: sv_lang::Expression<'d>,
    root_clock: Option<SemNode<'d>>,
    tree: Trees<'_>,
    scope: &Symbol<'d>,
) -> Result<(PropertyIr, LeafTable<'d>), LoweringError> {
    let mut leaves = LeafTable::new(root_clock);
    leaves.root_inferred = root_clock.is_some();
    let mut pb = Pb {
        a: blank_automaton(),
        leaves,
        props: Vec::new(),
        has_call: Vec::new(),
        nv_rules: Vec::new(),
        decls: Vec::new(),
        frames: Vec::new(),
        edges: BTreeSet::new(),
        sites: BTreeMap::new(),
        adv: 0,
        top: true,
        cover_sequence: true,
        seq_top: false,
        disable: None,
        tree,
        scope: *scope,
    };
    let root = pb.build_prop(inst.as_sem_node())?;
    Ok(pb.finish(root))
}

/// The identity of a property declaration: the byte range of its body (every
/// instance of one declaration has the same body node).
type DeclKey = (usize, usize);

/// What a formal argument was bound to, up to the identity of the expression:
/// the source range of the actual and, when it mentions formals of the
/// declaration it is written in, which expansion of it (its value differs per
/// expansion). A formal passed on as it is keeps the root of its own actual.
#[derive(Clone, Debug, PartialEq, Eq)]
struct Root {
    text: DeclKey,
    home: Option<usize>,
}

/// An expansion of a named property in progress (see the module doc comment).
struct PFrame {
    name: String,
    key: DeclKey,
    /// Every formal, with its [`Root`]; `None` for a `local input` formal.
    formals: Vec<(String, Option<Root>)>,
    /// The canonical and the physical slot of every local variable of the
    /// expansion (the `local` formals' body copies and the declared locals), by
    /// name.
    locals: Vec<(String, LocalVarId, LocalVarId)>,
    /// Some declared local has an initialiser.
    has_inits: bool,
    /// [`Pb::adv`] where the expansion began.
    entry_adv: u32,
    /// Set when a recursive instance calls this expansion.
    decl: Option<DeclId>,
}

/// Whether the local variable `sym` of an instance with arguments `args` is the
/// body copy of one of its `local` formals (as opposed to a declared local).
fn is_local_formal<'d>(args: &[sv_lang::AssertionInstanceArg<'d>], sym: &Symbol<'d>) -> bool {
    args.iter()
        .any(|g| g.port.assertion_port_is_local_var() && g.port.name() == sym.name())
}

/// One argument of an instance, classified for the recursion checks.
struct Bound {
    /// `None` for a `local input` formal (rebound per call, not part of the
    /// identity of an expansion).
    root: Option<Root>,
    /// The actual is an expression over formals of the declaration it is written
    /// in, other than a bare formal (what restriction 4 forbids in a recursive
    /// instance).
    mixed: bool,
}

/// One actual of an instance as its call site wrote it: all the recursion checks
/// need of the actual's syntax, so that an instance slang gives no arguments
/// (see [`Pb::expand`]) can use those of the same call site met earlier.
#[derive(Clone)]
struct ArgSite {
    name: String,
    /// A `local input` formal: bound per call, no part of the actual's identity.
    local: bool,
    /// The source range of the actual.
    text: DeclKey,
    /// The name, when the actual is one bare identifier.
    bare: Option<String>,
    /// Every identifier in the actual.
    idents: Vec<String>,
}

/// The property under construction.
struct Pb<'d, 't> {
    a: ir::Automaton,
    leaves: LeafTable<'d>,
    props: Vec<Prop>,
    /// Parallel to `props`: whether the node reaches a [`Prop::Call`] through
    /// its operands (16.12.17 restriction 1 asks of an operand of `not` or a
    /// strong operator whether it instantiates a recursive property).
    has_call: Vec<bool>,
    /// The nodes with their own 16.14.8 nonvacuity rule, by node (see
    /// [`NvRule`]).
    nv_rules: Vec<(PropId, NvRule)>,
    decls: Vec<PropDecl>,
    /// The property expansions in progress, outermost first.
    frames: Vec<PFrame>,
    /// The dependency digraph of F.7 found so far: `p -> q` for an instance of `q`
    /// written in the declaration of `p`.
    edges: BTreeSet<(DeclKey, DeclKey)>,
    /// The actuals of every property instance met, by the source range of the
    /// instance (one call site is written once whatever expansion it is met in).
    sites: BTreeMap<DeclKey, Vec<ArgSite>>,
    /// The ticks every evaluation of the node being built is guaranteed to be
    /// after the start of the property: the sum, along the path from the root, of
    /// what the operators in between advance (`nexttime [n]`, `always [lo:..]`, an
    /// implication's antecedent...). Restriction 3 compares two of its values.
    adv: u32,
    /// The node [`Self::build_prop`] is about to build is the whole of the property
    /// spec (the root, or what the root's own instance chain leads to): the only
    /// place a `disable iff` is legal (16.12). Taken by `build_prop`, which hands it
    /// on to the one operand that is still the whole spec (a `Clocking` wrapper's
    /// body, an instance's body).
    top: bool,
    /// The root is the sequence of a `cover sequence` statement (see
    /// [`build_property_as`]).
    cover_sequence: bool,
    /// The sequence [`Self::seq_prop`] is about to build is the root of a cover
    /// sequence (set by `build_prop` from `top`).
    seq_top: bool,
    /// The `disable iff` condition of the spec, once built (see
    /// [`PropertyIr::disable`]).
    disable: Option<LeafId>,
    tree: Trees<'t>,
    scope: Symbol<'d>,
}

/// Every operand [`PropId`] of `p`, in a fixed order (an exhaustive match: a new
/// [`Prop`] variant must say what its operands are).
fn operands(p: &Prop) -> Vec<PropId> {
    match p {
        Prop::Seq { .. } | Prop::Call { .. } => Vec::new(),
        Prop::Not(x) => vec![*x],
        Prop::And(x, y) | Prop::Or(x, y) => vec![*x, *y],
        Prop::If { then, els, .. } => std::iter::once(*then).chain(els.iter().copied()).collect(),
        Prop::Case { arms, default, .. } => arms
            .iter()
            .map(|arm| arm.body)
            .chain(default.iter().copied())
            .collect(),
        Prop::Implication { cons, .. } => vec![*cons],
        Prop::Nexttime { p, .. } | Prop::Always { p, .. } | Prop::Eventually { p, .. } => {
            vec![*p]
        }
        Prop::Until { p, q, .. } => vec![*p, *q],
        Prop::Abort { p, .. } | Prop::Clocked { p, .. } => vec![*p],
        Prop::Let { body, .. } => vec![*body],
    }
}

/// [`operands`] by mutable reference, for renumbering.
fn operands_mut(p: &mut Prop) -> Vec<&mut PropId> {
    match p {
        Prop::Seq { .. } | Prop::Call { .. } => Vec::new(),
        Prop::Not(x) => vec![x],
        Prop::And(x, y) | Prop::Or(x, y) => vec![x, y],
        Prop::If { then, els, .. } => std::iter::once(then).chain(els.iter_mut()).collect(),
        Prop::Case { arms, default, .. } => arms
            .iter_mut()
            .map(|arm| &mut arm.body)
            .chain(default.iter_mut())
            .collect(),
        Prop::Implication { cons, .. } => vec![cons],
        Prop::Nexttime { p, .. } | Prop::Always { p, .. } | Prop::Eventually { p, .. } => vec![p],
        Prop::Until { p, q, .. } => vec![p, q],
        Prop::Abort { p, .. } | Prop::Clocked { p, .. } => vec![p],
        Prop::Let { body, .. } => vec![body],
    }
}

/// The sequences `p` holds (an antecedent or a sequence property).
fn seqs_mut(p: &mut Prop) -> Option<&mut SeqRef> {
    match p {
        Prop::Seq { seq, .. } => Some(seq),
        Prop::Implication { ante, .. } => Some(ante),
        Prop::Not(_)
        | Prop::And(..)
        | Prop::Or(..)
        | Prop::If { .. }
        | Prop::Case { .. }
        | Prop::Nexttime { .. }
        | Prop::Always { .. }
        | Prop::Eventually { .. }
        | Prop::Until { .. }
        | Prop::Abort { .. }
        | Prop::Let { .. }
        | Prop::Clocked { .. }
        | Prop::Call { .. } => None,
    }
}

/// The `[...]` of a `nexttime`/`always`/`eventually` operator (see
/// [`Pb::unary_bracket`]).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
enum Bracket {
    Absent,
    /// `[n]`.
    Count(u32),
    /// `[m:n]`, `[m:$]` (`None`).
    Range(u32, Option<u32>),
}

/// What 16.12.22 asks of a sequence in a given position.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
enum Position {
    /// Used as a property (a), `strong(...)`/`weak(...)` included: nondegenerate
    /// and with no empty match.
    Property,
    /// The antecedent of `|->`/`#-#` (b): nondegenerate, an empty match is fine.
    OverlappedAntecedent,
    /// The antecedent of `|=>`/`#=#` (c): any match at all, empty-only included.
    NonOverlappedAntecedent,
}

impl<'d, 't> Pb<'d, 't> {
    fn err(&self, msg: &str) -> LoweringError {
        LoweringError::unsupported_at(msg, &self.scope)
    }

    /// Adds `p` to the table and records whether it reaches a recursive call.
    /// [`Self::push`] of a node that has a nonvacuity rule of its own.
    fn push_nv(&mut self, p: Prop, rule: NvRule) -> PropId {
        let id = self.push(p);
        self.nv_rules.push((id, rule));
        id
    }

    fn push(&mut self, p: Prop) -> PropId {
        let calls = matches!(p, Prop::Call { .. })
            || operands(&p).iter().any(|id| self.has_call[id.0 as usize]);
        let id = PropId(self.props.len() as u32);
        self.props.push(p);
        self.has_call.push(calls);
        id
    }

    /// The clocking event written directly on `node` (through parentheses), if
    /// any: `(@(posedge c) s)` has `posedge c`. `$inferred_clock` is not one
    /// (its clock is the instantiation context's, unknown here).
    fn written_event(&self, node: SemNode<'d>) -> Option<SemNode<'d>> {
        // A property instance leads with the clock its declaration's body writes
        // (16.16.1: the leading clocks of an instance are those of its body).
        if let Some(e) = node.as_expression()
            && is_property_instance(e)
        {
            return node
                .children()
                .into_iter()
                .find(|c| c.as_assertion_expr().is_some())
                .and_then(|b| self.written_event(b));
        }
        let x = node.as_assertion_expr()?;
        match (x.kind(), x.children().as_slice()) {
            (AssertionExprKind::Simple, [only]) => self.written_event(*only),
            (AssertionExprKind::Clocking, [event, _])
                if !super::is_inferred_clock_event(*event) =>
            {
                Some(*event)
            }
            _ => None,
        }
    }

    /// Whether `node`'s leading clock is a written one: `node` (or, through the
    /// operators that take their clock from their first operand, `s |=> t`,
    /// `s ##1 t`, `not s`, its first operand) is clocked or an instance whose body is
    /// (16.16.1).
    fn leads_with_written_clock(&self, node: SemNode<'d>) -> bool {
        self.leads_with_clock_in(node, true)
    }

    /// `leads_with_written_clock`; `top` is false below a sequence concatenation,
    /// where a sequence instance's declared clock does not become the assertion's
    /// (16.16 (f): `c4: cover property (s3 ##1 b)` is illegal).
    fn leads_with_clock_in(&self, node: SemNode<'d>, top: bool) -> bool {
        if self.written_event(node).is_some() {
            return true;
        }
        // A sequence instance leads with the clock its body writes.
        if let Some(e) = node.as_expression() {
            return top
                && e.kind() == ExpressionKind::AssertionInstance
                && node
                    .children()
                    .into_iter()
                    .find(|c| c.as_assertion_expr().is_some())
                    .is_some_and(|b| self.leads_with_written_clock(b));
        }
        let Some(x) = node.as_assertion_expr() else {
            return false;
        };
        // A parenthesised or plain wrapper takes its operand's clock.
        if x.kind() == AssertionExprKind::Simple
            && let [only] = x.children().as_slice()
        {
            return self.leads_with_clock_in(*only, top);
        }
        let kind = x.kind();
        // Below a sequence concatenation an instance's declared clock is not the
        // assertion's; below `|=>`/`not`... it is (16.13's mult_p6).
        let inst_ok = !matches!(kind, AssertionExprKind::SequenceConcat);
        let first = |s: &Self| {
            x.children()
                .first()
                .is_some_and(|&c| s.leads_with_clock_in(c, inst_ok))
        };
        // Only these operators take their clock from their first operand;
        // every other expression kind has no leading clock to inherit.
        if matches!(
            kind,
            AssertionExprKind::SequenceConcat | AssertionExprKind::Unary
        ) {
            first(self)
        } else if matches!(kind, AssertionExprKind::Binary) {
            !matches!(Op::of(x, &self.scope), Ok(Op::Binary(B::And | B::Or))) && first(self)
        } else {
            false
        }
    }

    /// Whether a clocking event is written anywhere inside `node`, instance
    /// bodies included.
    fn mentions_written_clock(&self, node: SemNode<'d>) -> bool {
        if let Some(x) = node.as_assertion_expr()
            && x.kind() == AssertionExprKind::Clocking
            && let [event, _] = x.children().as_slice()
            && !super::is_inferred_clock_event(*event)
        {
            return true;
        }
        node.children()
            .into_iter()
            .any(|c| self.mentions_written_clock(c))
    }

    /// Whether a clocking event different from `ctx` is written anywhere inside
    /// the assertion expression `node` (a clock change within a sequence).
    fn changes_clock_inside(&self, node: SemNode<'d>, ctx: SemNode<'d>) -> bool {
        let Some(x) = node.as_assertion_expr() else {
            return false;
        };
        let kids = x.children();
        if let (AssertionExprKind::Clocking, [event, _]) = (x.kind(), kids.as_slice())
            && !super::is_inferred_clock_event(*event)
            && !super::events_equivalent(*event, ctx)
        {
            return true;
        }
        kids.iter().any(|&k| self.changes_clock_inside(k, ctx))
    }

    /// Whether `x` is an `and`/`or` whose operands are clocked differently.
    fn and_or_with_two_leading_clocks(&self, x: AssertionExpr<'d>) -> Result<bool, LoweringError> {
        if !matches!(Op::of(x, &self.scope)?, Op::Binary(B::And | B::Or)) {
            return Ok(false);
        }
        // 16.16.1: with no clock flowing in (no default, no inferred clock), an
        // operand without a written clock leads with `inherited`, which no outer
        // clock supplies, next to one that names its own: no unique leading clock.
        if self.leaves.clock_event(self.leaves.cur).is_none() {
            let kids = x.children();
            if let [l, r] = kids.as_slice()
                && self.written_event(*l).is_some() != self.written_event(*r).is_some()
            {
                return Ok(true);
            }
        }
        Ok(self.operands_clocked_differently(x))
    }

    /// Whether the two operands of the `and`/`or` node `x` each name a clock and
    /// the clocks differ, or one names a clock different from the context's.
    fn operands_clocked_differently(&self, x: AssertionExpr<'d>) -> bool {
        let kids = x.children();
        let [l, r] = kids.as_slice() else {
            return false;
        };
        let ctx = self.leaves.clock_event(self.leaves.cur);
        // An operand that is itself a multiclocked sequence (`w ##1 @(d) x`) makes
        // the `and`/`or` a multiclocked property too (16.13.2: multiclocked
        // sequences are multiclocked properties; 16.13.3's `(w ##1 @(d) x) and
        // (y ##1 z)` is "a property conjunction due to the multiple clocking").
        if let Some(c) = ctx
            && (self.changes_clock_inside(*l, c) || self.changes_clock_inside(*r, c))
        {
            return true;
        }
        match (self.written_event(*l), self.written_event(*r)) {
            (Some(a), Some(b)) => !super::events_equivalent(a, b),
            (Some(a), None) | (None, Some(a)) => {
                ctx.is_some_and(|c| !super::events_equivalent(a, c))
            }
            (None, None) => false,
        }
    }

    /// Whether `node` is a `sequence_expr` (16.12.1) rather than a property
    /// expression.
    fn is_seq(&self, node: SemNode<'d>) -> Result<bool, LoweringError> {
        if let Some(e) = node.as_expression() {
            return Ok(!is_property_instance(e));
        }
        let Some(x) = node.as_assertion_expr() else {
            return Err(self.err(
                "sva property builder: a property operand is neither an Expression nor an \
                 AssertionExpr (unexpected SemNode kind)",
            ));
        };
        match x.kind() {
            AssertionExprKind::Simple => match x.children().as_slice() {
                [only] => self.is_seq(*only),
                _ => Ok(true),
            },
            AssertionExprKind::SequenceConcat
            | AssertionExprKind::SequenceWithMatch
            | AssertionExprKind::FirstMatch => Ok(true),
            AssertionExprKind::Clocking => match x.children().as_slice() {
                [_, body] => self.is_seq(*body),
                _ => Err(self.err("a clocking property expression does not have two children")),
            },
            AssertionExprKind::Binary => match super::super::op::Op::of(x, &self.scope)? {
                super::super::op::Op::Binary(op) => {
                    use super::super::op::AssertionBinaryOp as B;
                    match op {
                        B::Intersect | B::Throughout | B::Within => Ok(true),
                        B::And | B::Or => {
                            // 16.13.2: `(@c0 s0) and (@c1 s1)` with different
                            // clocks is a multiclocked PROPERTY (16.13.1: no
                            // sequence operator but `##1`/`##0` combines
                            // differently clocked sequences).
                            if self.operands_clocked_differently(x) {
                                return Ok(false);
                            }
                            for c in x.children() {
                                if !self.is_seq(c)? {
                                    return Ok(false);
                                }
                            }
                            Ok(true)
                        }
                        B::Iff
                        | B::Until
                        | B::SUntil
                        | B::UntilWith
                        | B::SUntilWith
                        | B::Implies
                        | B::OverlappedImplication
                        | B::NonOverlappedImplication
                        | B::OverlappedFollowedBy
                        | B::NonOverlappedFollowedBy => Ok(false),
                    }
                }
                super::super::op::Op::Unary(_) => {
                    Err(self.err("a Binary assertion expression resolved to a unary operator"))
                }
            },
            AssertionExprKind::Unary
            | AssertionExprKind::StrongWeak
            | AssertionExprKind::Abort
            | AssertionExprKind::Conditional
            | AssertionExprKind::Case
            | AssertionExprKind::DisableIff => Ok(false),
            AssertionExprKind::Invalid => Err(self.err(
                "an assertion expression slang could not bind (an Invalid node): the design has \
                 an error, see `Design::diagnostics()`",
            )),
            other => Err(self.err(&format!(
                "sva property builder: AssertionExprKind::{other:?} is not a kind this builder \
                 knows (the enum is non-exhaustive)"
            ))),
        }
    }

    /// Builds the sequence at `node` into the shared automaton: its entry, whether
    /// it admits the empty match, and its F.5.4 flow.
    fn seq(&mut self, node: SemNode<'d>) -> Result<(SeqRef, super::Flow), LoweringError> {
        let frag = build_node(&mut self.a, &mut self.leaves, node, self.tree, &self.scope)?;
        add_match_edges(&mut self.a, frag.exits);
        let span = frag.clock.unwrap_or(Span::single(self.leaves.cur));
        Ok((
            SeqRef {
                entry: frag.entry,
                admits_empty: frag.empty,
                clock: span.start,
                end_clock: span.end,
            },
            frag.flow,
        ))
    }

    /// 16.12.22: what `seq` may be where it stands.
    fn check_nondegenerate(&self, seq: SeqRef, at: Position) -> Result<(), LoweringError> {
        let class = classify_sequence(&self.a, seq, &|_| false);
        let ok = match (at, class) {
            (Position::Property, SequenceClass::NonEmpty { also_empty: false }) => true,
            (Position::Property, _) => false,
            (Position::OverlappedAntecedent, SequenceClass::NonEmpty { .. }) => true,
            (Position::OverlappedAntecedent, _) => false,
            (Position::NonOverlappedAntecedent, SequenceClass::Never) => false,
            (Position::NonOverlappedAntecedent, _) => true,
        };
        if ok {
            return Ok(());
        }
        let why = match class {
            SequenceClass::Never => "it can never match (it is degenerate)",
            SequenceClass::EmptyOnly => "it admits only the empty match (it is degenerate)",
            SequenceClass::NonEmpty { also_empty } => {
                debug_assert!(also_empty);
                "it admits the empty match"
            }
        };
        let rule = match at {
            Position::Property => {
                "a sequence used as a property must be nondegenerate and admit no empty match \
                 (LRM 16.12.22 (a), 16.12.2)"
            }
            Position::OverlappedAntecedent => {
                "the antecedent of an overlapped implication `|->`/`#-#` must be nondegenerate \
                 (LRM 16.12.22 (b))"
            }
            Position::NonOverlappedAntecedent => {
                "the antecedent of a nonoverlapped implication `|=>`/`#=#` must admit at least \
                 one match (LRM 16.12.22 (c))"
            }
        };
        Err(self.err(&format!("{rule}: {why}")))
    }

    /// A sequence in a property position: `seq`/`strong(seq)`/`weak(seq)`.
    fn seq_prop(
        &mut self,
        node: SemNode<'d>,
        strength: Option<Strength>,
    ) -> Result<PropId, LoweringError> {
        let root_of_cover = std::mem::take(&mut self.seq_top);
        let (seq, _) = self.seq(node)?;
        if !root_of_cover {
            self.check_nondegenerate(seq, Position::Property)?;
        }
        Ok(self.push(Prop::Seq { seq, strength }))
    }

    /// Builds the property expression at `node`.
    fn build_prop(&mut self, node: SemNode<'d>) -> Result<PropId, LoweringError> {
        let top = std::mem::take(&mut self.top);
        self.seq_top = top && self.cover_sequence;
        if let Some(e) = node.as_expression() {
            return if is_property_instance(e) {
                self.top = top;
                let built = self.instance(e);
                self.top = false;
                built
            } else {
                self.seq_prop(node, None)
            };
        }
        let Some(x) = node.as_assertion_expr() else {
            return Err(self.err(
                "sva property builder: a property operand is neither an Expression nor an \
                 AssertionExpr (unexpected SemNode kind)",
            ));
        };
        // 16.16 (f): with no default, inferred or leading clocking event, the
        // maximal property must itself be an instance (or clocked) whose leading
        // clock is determined; a bare operator over a clocked operand
        // (`s3 ##1 b`, `a |-> @(c) b`) inherits a clock nothing supplies.
        if top
            && self.leaves.clock_event(self.leaves.cur).is_none()
            && matches!(
                x.kind(),
                AssertionExprKind::SequenceConcat
                    | AssertionExprKind::Binary
                    | AssertionExprKind::Unary
                    | AssertionExprKind::Conditional
                    | AssertionExprKind::Case
            )
            && self.mentions_written_clock(node)
            && !self.leads_with_written_clock(node)
            && !self.and_or_with_two_leading_clocks(x).unwrap_or(false)
        {
            return Err(self.err(
 "the assertion has no leading clocking event (no default clocking, no inferred clock) and its maximal property is not an instance of a sequence or property with a unique leading clock (LRM 16.16 (f))",
            ));
        }
        match x.kind() {
            AssertionExprKind::Clocking => {
                let ch = crate::sva::op::clocking_children(x, &self.scope)?;
                // A clocked sequence is built as one (its stamps carry the clock).
                if self.is_seq(ch.body.as_sem_node())? {
                    return self.seq_prop(node, None);
                }
                self.build_under_clock(ch.event, ch.body.as_sem_node(), top)
            }
            AssertionExprKind::Simple => {
                if let [only] = x.children().as_slice()
                    && only.as_expression().is_some_and(is_property_instance)
                {
                    self.top = top;
                    return self.build_prop(*only);
                }
                self.seq_prop(node, None)
            }
            AssertionExprKind::SequenceConcat
            | AssertionExprKind::SequenceWithMatch
            | AssertionExprKind::FirstMatch => self.seq_prop(node, None),
            AssertionExprKind::StrongWeak => self.build_strong_weak(x),
            AssertionExprKind::Binary if top && self.and_or_with_two_leading_clocks(x)? => {
                // 16.16.1 (e): the maximal property of an assertion shall have
                // a unique semantic leading clock; `q1 and q2` leads with both.
                Err(self.err(
                    "the maximal property is an `and`/`or` of differently clocked operands (or of one \
                     that names a clock and one that inherits none), \
                     which has no unique semantic leading clock (LRM 16.16.1, 16.13.2: legal \
                     only as a consequent or below an operator that fixes the leading clock)",
                ))
            }
            AssertionExprKind::Binary if self.is_seq(node)? => self.seq_prop(node, None),
            AssertionExprKind::Binary => self.build_binary(x),
            AssertionExprKind::Unary => self.build_unary(x),
            AssertionExprKind::Abort => self.build_abort(x),
            AssertionExprKind::Conditional => self.build_if(x),
            AssertionExprKind::Case => self.build_case(x),
            AssertionExprKind::DisableIff => self.build_disable_iff(x, top),
            AssertionExprKind::Invalid => Err(self.err(
                "an assertion expression slang could not bind (an Invalid node): the design has \
                 an error, see `Design::diagnostics()`",
            )),
            other => Err(self.err(&format!(
                "sva property builder: AssertionExprKind::{other:?} is not a kind this builder \
                 knows (the enum is non-exhaustive)"
            ))),
        }
    }

    /// `body` (a property, not a sequence) built with `event` as the context
    /// clock: the `Clocking` node's `@(event) body`, and the body of a property
    /// declared in a clocking block (16.18), which that block's event clocks.
    /// `top`: this is the outermost node of the assertion's property.
    fn build_under_clock(
        &mut self,
        event: SemNode<'d>,
        body: SemNode<'d>,
        top: bool,
    ) -> Result<PropId, LoweringError> {
        if top {
            self.leaves.rebind_inferred_root(event);
        }
        let id = self.leaves.resolve_clock(event, &self.scope)?;
        if id == self.leaves.cur {
            // The event of the context: nothing changes.
            self.top = top;
            return self.build_prop(body);
        }
        // A sequence carries its clock in its own stamps (`Self::seq`), as the
        // `Clocking` arm's clocked sequence does; only a property is wrapped.
        let is_seq = self.is_seq(body)?;
        let saved = std::mem::replace(&mut self.leaves.cur, id);
        self.top = top;
        let built = self.build_prop(body);
        self.leaves.cur = saved;
        let p = built?;
        if is_seq {
            return Ok(p);
        }
        Ok(self.push(Prop::Clocked { clock: id, p }))
    }

    /// A Boolean leaf of the property (an `if` condition, a `case` selector or
    /// label): evaluated at the tick the operator is evaluated at.
    fn leaf(&mut self, node: SemNode<'d>, what: &str) -> Result<LeafId, LoweringError> {
        let e = node.as_expression().ok_or_else(|| {
            self.err(&format!(
                "the {what} of a property operator is not an expression (unexpected SemNode kind)"
            ))
        })?;
        self.leaves.push_leaf(&mut self.a, e, None, &self.scope)
    }

    /// The operator of a unary property node.
    fn build_unary(&mut self, x: AssertionExpr<'d>) -> Result<PropId, LoweringError> {
        let Op::Unary(op) = Op::of(x, &self.scope)? else {
            return Err(self.err("a Unary assertion expression resolved to a binary operator"));
        };
        let kids = x.children();
        let [operand] = kids.as_slice() else {
            return Err(self.err(&format!(
                "a unary property operator {op:?} does not have exactly one operand"
            )));
        };
        match op {
            // 16.12.3: the operand is built under the entry flow set and nothing
            // flows out of the negation.
            U::Not => {
                let p = self.build_prop(*operand)?;
                self.negate(p, "`not`")
            }
            // 16.12.10: `nexttime [n] p` evaluates `p` at the n-th next tick (weak: it
            // is also true when that tick does not exist; strong: it must exist).
            // `[n]` is one constant, `nexttime p` is `nexttime [1] p`, and
            // `nexttime [0] p` is the alignment operator.
            U::NextTime | U::SNextTime => {
                let strong = op == U::SNextTime;
                let name = if strong { "s_nexttime" } else { "nexttime" };
                let n = match self.unary_bracket(x, name)? {
                    Bracket::Absent => 1,
                    Bracket::Count(n) => n,
                    Bracket::Range(..) => {
                        return Err(self.err(&format!(
                            "`{name} [..]` takes one constant number of clock ticks, not a \
                             range (LRM 16.12.10)"
                        )));
                    }
                };
                let p = self.after(n, |s| s.build_prop(*operand))?;
                if strong {
                    self.forbid_call(p, "`s_nexttime`")?;
                }
                Ok(self.push(Prop::Nexttime { p, n, strong }))
            }
            // 16.12.11: `always [lo:hi] p` holds when `p` holds at every tick of the
            // range; `always p` is the unbounded `[0:$]`. The strong form needs
            // those ticks to exist, so its range is mandatory and bounded.
            U::Always | U::SAlways => {
                let strong = op == U::SAlways;
                let name = if strong { "s_always" } else { "always" };
                let (lo, hi) = match self.unary_bracket(x, name)? {
                    Bracket::Absent if strong => {
                        return Err(
                            self.err("`s_always` needs a bounded range `[m:n]` (LRM 16.12.11)")
                        );
                    }
                    Bracket::Absent => (0, None),
                    Bracket::Range(lo, hi) => (lo, hi),
                    Bracket::Count(_) => {
                        return Err(self.err(&format!(
                            "`{name} [..]` takes a range `[m:n]`, not a single count \
                             (LRM 16.12.11)"
                        )));
                    }
                };
                if strong && hi.is_none() {
                    return Err(self.err(
                        "`s_always [m:$]` is illegal: the range of a strong always shall be \
                         bounded (LRM 16.12.11)",
                    ));
                }
                let p = self.after(lo, |s| s.build_prop(*operand))?;
                if strong {
                    self.forbid_call(p, "`s_always`")?;
                }
                Ok(self.push(Prop::Always { p, lo, hi, strong }))
            }
            // 16.12.13: `s_eventually [lo:hi] p` needs `p` at one tick of the range
            // (`s_eventually p` is `[0:$]`, the range may be unbounded); the weak
            // `eventually [lo:hi] p` is also true when the whole range does not
            // exist, so its range is mandatory and bounded.
            U::Eventually | U::SEventually => {
                let strong = op == U::SEventually;
                let name = if strong { "s_eventually" } else { "eventually" };
                let (lo, hi) = match self.unary_bracket(x, name)? {
                    Bracket::Absent if strong => (0, None),
                    Bracket::Absent => {
                        return Err(self.err(
                            "`eventually` needs a bounded range `[m:n]`; the unbracketed form is \
                             `s_eventually` (LRM 16.12.13)",
                        ));
                    }
                    Bracket::Range(lo, hi) => (lo, hi),
                    Bracket::Count(_) => {
                        return Err(self.err(&format!(
                            "`{name} [..]` takes a range `[m:n]`, not a single count \
                             (LRM 16.12.13)"
                        )));
                    }
                };
                if !strong && hi.is_none() {
                    return Err(self.err(
                        "`eventually [m:$]` is illegal: the range of a weak eventually shall be \
                         bounded (LRM 16.12.13)",
                    ));
                }
                let p = self.after(lo, |s| s.build_prop(*operand))?;
                if strong {
                    self.forbid_call(p, "`s_eventually`")?;
                }
                Ok(self.push(Prop::Eventually { p, lo, hi, strong }))
            }
        }
    }

    /// What the `[...]` written after the keyword of the unary property operator `x`
    /// (`nexttime`, `always`, `eventually` and their `s_` forms, named `name` in
    /// the messages) says.
    ///
    /// slang's semantic node drops the bracket, so it is read from the syntax:
    /// `[n]` is a [`Bracket::Count`], `[m:n]`/`[m:$]` a [`Bracket::Range`] (`m <=
    /// n` checked here, 16.12.11), and no bracket [`Bracket::Absent`]. The
    /// bounds fold with the property's formals in scope, so `nexttime [d] p` and
    /// `always [lo:hi] p` take a property formal.
    fn unary_bracket(&self, x: AssertionExpr<'d>, name: &str) -> Result<Bracket, LoweringError> {
        let syn = self.tree.syntax(&x).ok_or_else(|| {
            self.err(&format!(
                "`{name}`: the property operator has no syntax node in the given tree"
            ))
        })?;
        let syn = peel_property_parens(syn);
        let selector = if let Some(s) = UnarySelectPropertyExprSyntax::cast(syn) {
            s.selector()
        } else if UnaryPropertyExprSyntax::cast(syn).is_some() {
            None
        } else {
            return Err(self.err(&format!(
                "`{name}`: expected a unary property expression syntax node, found {:?}",
                syn.kind()
            )));
        };
        let Some(selector) = selector else {
            return Ok(Bracket::Absent);
        };
        let one = matches!(selector, SelectorSyntax::BitSelect(_));
        let r = ranges::range_of_selector(selector, &self.scope, &self.leaves.env)?;
        if one {
            return Ok(Bracket::Count(r.min));
        }
        if let Some(max) = r.max
            && r.min > max
        {
            return Err(self.err(&format!(
                "`{name} [{}:{max}]`: the minimum of the range is greater than its maximum \
                 (LRM 16.12.11, 16.12.13)",
                r.min
            )));
        }
        Ok(Bracket::Range(r.min, r.max))
    }

    /// The operator of a binary property node (a sequence `and`/`or`/`intersect`/
    /// `throughout`/`within` never gets here, see [`Self::is_seq`]).
    fn build_binary(&mut self, x: AssertionExpr<'d>) -> Result<PropId, LoweringError> {
        let Op::Binary(op) = Op::of(x, &self.scope)? else {
            return Err(self.err("a Binary assertion expression resolved to a unary operator"));
        };
        let kids = x.children();
        let [lhs, rhs] = kids.as_slice() else {
            return Err(self.err(&format!(
                "a binary property operator {op:?} does not have exactly two operands"
            )));
        };
        match op {
            // 16.12.4/16.12.5: each operand starts at the operator's start point
            // with the entry flow set.
            B::Or => {
                let (p, q) = (self.build_prop(*lhs)?, self.build_prop(*rhs)?);
                Ok(self.push(Prop::Or(p, q)))
            }
            B::And => {
                let (p, q) = (self.build_prop(*lhs)?, self.build_prop(*rhs)?);
                Ok(self.push(Prop::And(p, q)))
            }
            B::Intersect | B::Throughout | B::Within => Err(self.err(&format!(
                "the sequence operator {op:?} reached the property builder with a property \
                 operand (16.9.6-16.9.10: its operands are sequences)"
            ))),
            // 16.12.8, F.3.4.3.2: `p implies q` is `not p or q` and `p iff q` is
            // `(p implies q) and (q implies p)`; both operands are built once and
            // shared, each under the entry flow set.
            B::Implies => {
                let (p, q) = (self.build_prop(*lhs)?, self.build_prop(*rhs)?);
                self.implies(p, q, true)
            }
            B::Iff => {
                let (p, q) = (self.build_prop(*lhs)?, self.build_prop(*rhs)?);
                // Rule aa (nonvacuous iff either side is) is what the two plain
                // `or`s give; only a written `implies` has rule z.
                let (pq, qp) = (self.implies(p, q, false)?, self.implies(q, p, false)?);
                Ok(self.push(Prop::And(pq, qp)))
            }
            B::OverlappedImplication => self.implication(*lhs, *rhs, true, false),
            B::NonOverlappedImplication => self.implication(*lhs, *rhs, false, false),
            B::OverlappedFollowedBy => self.implication(*lhs, *rhs, true, true),
            B::NonOverlappedFollowedBy => self.implication(*lhs, *rhs, false, true),
            // 16.12.12, F.3.4.3.8: `p until q` holds `p` at every tick up to (not
            // including) a tick where `q` holds; `until_with` includes it, as `p until
            // (p and q)`; the `s_` forms need that tick to exist. Each operand starts
            // at the operator's start tick with the entry flow set.
            B::Until | B::SUntil => {
                let (p, q) = (self.build_prop(*lhs)?, self.build_prop(*rhs)?);
                if op == B::SUntil {
                    self.forbid_call(p, "`s_until`")?;
                    self.forbid_call(q, "`s_until`")?;
                }
                Ok(self.push(Prop::Until {
                    p,
                    q,
                    strong: op == B::SUntil,
                }))
            }
            B::UntilWith | B::SUntilWith => {
                let (p, q) = (self.build_prop(*lhs)?, self.build_prop(*rhs)?);
                if op == B::SUntilWith {
                    self.forbid_call(p, "`s_until_with`")?;
                    self.forbid_call(q, "`s_until_with`")?;
                }
                let both = self.push(Prop::And(p, q));
                Ok(self.push_nv(
                    Prop::Until {
                        p,
                        q: both,
                        strong: op == B::SUntilWith,
                    },
                    NvRule::UntilWith,
                ))
            }
        }
    }

    /// `p implies q`, as `not p or q` (F.3.4.3.2).
    fn implies(&mut self, p: PropId, q: PropId, written: bool) -> Result<PropId, LoweringError> {
        let not_p = self.negate(p, "`implies`/`iff`")?;
        if written {
            Ok(self.push_nv(Prop::Or(not_p, q), NvRule::Implies))
        } else {
            Ok(self.push(Prop::Or(not_p, q)))
        }
    }

    /// `not p`, after restriction 1 of 16.12.17: the negation of a property
    /// expression that contains a recursive instance is illegal. `what` names the
    /// operator the user wrote, which the derived operators (`implies`, `iff`,
    /// `#-#`, `#=#`) define through `not`.
    fn negate(&mut self, p: PropId, what: &str) -> Result<PropId, LoweringError> {
        self.forbid_call(p, what)?;
        Ok(self.push(Prop::Not(p)))
    }

    /// Restriction 1 of 16.12.17: `what` (`not` or a strong operator) shall not be
    /// applied to a property expression that instantiates a recursive property, or
    /// one from which a recursive property is reachable (`has_call` is both: the
    /// call is inside, however deep the expansion of the wrappers in between).
    fn forbid_call(&self, operand: PropId, what: &str) -> Result<(), LoweringError> {
        if !self.has_call[operand.0 as usize] {
            return Ok(());
        }
        Err(self.err(&format!(
            "{what} is applied to a property expression that instantiates a recursive \
             property, or one from which a recursive property is reachable (LRM 16.12.17 \
             restriction 1)"
        )))
    }

    /// Builds with `ticks` more guaranteed time since the start of the property
    /// (see [`Pb::adv`]).
    fn after<T>(
        &mut self,
        ticks: u32,
        build: impl FnOnce(&mut Self) -> Result<T, LoweringError>,
    ) -> Result<T, LoweringError> {
        let saved = self.adv;
        self.adv = saved.saturating_add(ticks);
        let built = build(self);
        self.adv = saved;
        built
    }

    /// The fewest clock ticks between the start of `seq` and the end of any of its
    /// matches (0 for an empty match): the guaranteed advance of time that an
    /// implication's consequent is after. A shortest path over the automaton
    /// with a cycle delay weighing its minimum and everything else nothing, so
    /// the number is a lower bound whatever the match items and guards do.
    fn min_match_ticks(&self, seq: SeqRef) -> u32 {
        if seq.admits_empty {
            return 0;
        }
        let mut best = vec![u32::MAX; self.a.states.len()];
        let mut heap = BinaryHeap::new();
        best[seq.entry.0 as usize] = 0;
        heap.push(std::cmp::Reverse((0u32, seq.entry.0)));
        while let Some(std::cmp::Reverse((d, s))) = heap.pop() {
            if d > best[s as usize] {
                continue;
            }
            for e in &self.a.state(ThreadStateId(s)).edges {
                let w = match &e.label {
                    Transition::Match { .. } => return d,
                    Transition::Delay { min, .. } => *min,
                    _ => 0,
                };
                let nd = d.saturating_add(w);
                let t = e.target.0 as usize;
                if nd < best[t] {
                    best[t] = nd;
                    heap.push(std::cmp::Reverse((nd, e.target.0)));
                }
            }
        }
        0
    }

    /// `ante |-> cons`, `ante |=> cons` (16.12.7) and, with `followed_by`, `ante #-#
    /// cons`, `ante #=# cons` (16.12.9): the duals, `not (ante |-> not cons)`.
    ///
    /// The one operator family that carries the antecedent's local variables to the
    /// consequent: the antecedent is built under the entry flow set, the consequent
    /// under what the antecedent assigned on every path to its end (16.12.19, F.5.4),
    /// and nothing flows out.
    fn implication(
        &mut self,
        ante: SemNode<'d>,
        cons: SemNode<'d>,
        overlapped: bool,
        followed_by: bool,
    ) -> Result<PropId, LoweringError> {
        if !self.is_seq(ante)? {
            return Err(self.err(
                "the antecedent of an implication or a followed-by is a property, not a \
                 sequence (LRM 16.12.7, 16.12.9)",
            ));
        }
        let x0 = self.leaves.flow_in.clone();
        let (ante, flow) = self.seq(ante)?;
        let position = if overlapped {
            Position::OverlappedAntecedent
        } else {
            Position::NonOverlappedAntecedent
        };
        self.check_nondegenerate(ante, position)?;
        self.leaves.flow_in = flow.flow_out(&x0);
        // The consequent starts at the end of a match of the antecedent (one tick
        // later for the nonoverlapped forms): at least that many ticks on.
        let ticks = self
            .min_match_ticks(ante)
            .saturating_add(u32::from(!overlapped));
        let cons = self.after(ticks, |s| s.build_prop(cons));
        self.leaves.flow_in = x0;
        let mut cons = cons?;
        if followed_by {
            cons = self.negate(cons, "`#-#`/`#=#`")?;
        }
        let imp = self.push(Prop::Implication {
            ante,
            cons,
            overlapped,
        });
        if followed_by {
            // `has_call` of `imp` is that of `cons`, already refused above.
            Ok(self.push(Prop::Not(imp)))
        } else {
            Ok(imp)
        }
    }

    /// `if (cond) then [else els]` (16.12.6).
    fn build_if(&mut self, x: AssertionExpr<'d>) -> Result<PropId, LoweringError> {
        let kids = x.children();
        let (cond, then, els) = match kids.as_slice() {
            [c, t] => (*c, *t, None),
            [c, t, e] => (*c, *t, Some(*e)),
            other => {
                return Err(self.err(&format!(
                    "an if-else property has {} children, expected [condition, then] or \
                     [condition, then, else]",
                    other.len()
                )));
            }
        };
        let cond = self.leaf(cond, "condition")?;
        let then = self.build_prop(then)?;
        let els = els.map(|e| self.build_prop(e)).transpose()?;
        Ok(self.push(Prop::If { cond, then, els }))
    }

    /// `case (sel) label, ...: p; ... [default: p] endcase` (16.12.16).
    fn build_case(&mut self, x: AssertionExpr<'d>) -> Result<PropId, LoweringError> {
        let c = crate::sva::op::case_children(x, self.tree, &self.scope)?;
        let selector = self.leaf(c.selector, "case selector")?;
        let mut arms = Vec::with_capacity(c.items.len());
        for item in &c.items {
            let mut labels = Vec::with_capacity(item.labels.len());
            for l in &item.labels {
                labels.push(self.leaf(*l, "case item label")?);
            }
            let body = self.build_prop(item.body.as_sem_node())?;
            arms.push(CaseArm { labels, body });
        }
        let default = c
            .default
            .map(|d| self.build_prop(d.as_sem_node()))
            .transpose()?;
        Ok(self.push(Prop::Case {
            selector,
            arms,
            default,
        }))
    }

    /// `accept_on`/`reject_on`/`sync_accept_on`/`sync_reject_on (cond) p`
    /// (16.12.14). slang gives all four one node kind, so the keyword is read from
    /// the syntax; the evaluator defines what each mode means (`reject_on(b) p`
    /// is `not accept_on(b) not p`, F.3.4.3.7). The condition is a Boolean read at
    /// the tick the operator is evaluated at (and, for the asynchronous forms,
    /// between ticks); `p` gets the entry flow set and lets nothing out.
    fn build_abort(&mut self, x: AssertionExpr<'d>) -> Result<PropId, LoweringError> {
        let syn = self
            .tree
            .syntax(&x)
            .ok_or_else(|| self.err("an abort property has no syntax node"))?;
        let syn = peel_property_parens(syn);
        let ab = AcceptOnPropertyExprSyntax::cast(syn).ok_or_else(|| {
            self.err(&format!(
                "expected an abort property syntax node, found {:?}",
                syn.kind()
            ))
        })?;
        let keyword = ab.keyword().map(|t| t.text().to_string());
        let mode = match keyword.as_deref() {
            Some("accept_on") => AbortMode::Accept,
            Some("reject_on") => AbortMode::Reject,
            Some("sync_accept_on") => AbortMode::SyncAccept,
            Some("sync_reject_on") => AbortMode::SyncReject,
            other => {
                return Err(self.err(&format!(
                    "an abort property with the keyword {other:?}, expected `accept_on`, \
                     `reject_on`, `sync_accept_on` or `sync_reject_on`"
                )));
            }
        };
        let ch = crate::sva::op::abort_children(x, &self.scope)?;
        let cond = self.abort_condition(ch.condition)?;
        let p = self.build_prop(ch.body.as_sem_node())?;
        Ok(self.push(Prop::Abort { cond, p, mode }))
    }

    /// The abort condition of 16.12.14: a plain Boolean, which "shall not contain
    /// any reference to local variables and the sequence methods triggered and
    /// matched".
    fn abort_condition(&mut self, node: SemNode<'d>) -> Result<LeafId, LoweringError> {
        let e = node.as_expression().ok_or_else(|| {
            self.err(
                "the condition of an abort property is not an expression (unexpected SemNode kind)",
            )
        })?;
        let mut points = Vec::new();
        collect_end_points(e, &mut points);
        if !points.is_empty() {
            return Err(self.err(
                "an abort condition shall not contain the sequence methods `.triggered` or \
                 `.matched` (LRM 16.12.14)",
            ));
        }
        let (mut locals, mut lvalue) = (Vec::new(), false);
        collect_local_reads(node, &mut locals, &mut lvalue);
        if let Some(v) = locals.first() {
            return Err(self.err(&format!(
                "an abort condition shall not reference the local variable `{}` (LRM 16.12.14)",
                v.name()
            )));
        }
        self.leaf(node, "abort condition")
    }

    /// `strong(seq)` / `weak(seq)` (16.12.2): the keyword is only in the syntax.
    fn build_strong_weak(&mut self, x: AssertionExpr<'d>) -> Result<PropId, LoweringError> {
        let syn = self
            .tree
            .syntax(&x)
            .ok_or_else(|| self.err("a strong/weak property has no syntax node"))?;
        let syn = peel_property_parens(syn);
        let sw = StrongWeakPropertyExprSyntax::cast(syn).ok_or_else(|| {
            self.err(&format!(
                "expected a strong/weak property syntax node, found {:?}",
                syn.kind()
            ))
        })?;
        let keyword = sw.keyword().map(|t| t.text().to_string());
        let strength = match keyword.as_deref() {
            Some("strong") => Strength::Strong,
            Some("weak") => Strength::Weak,
            other => {
                return Err(self.err(&format!(
                    "a strong/weak property with the keyword {other:?}, expected `strong` or \
                     `weak`"
                )));
            }
        };
        let kids = x.children();
        let [operand] = kids.as_slice() else {
            return Err(self.err("a strong/weak property does not have exactly one operand"));
        };
        self.seq_prop(*operand, Some(strength))
    }

    /// A named property instance (16.12.1, 16.12.19), or the reference to a
    /// property-typed formal, which slang models as a zero-argument instance
    /// whose body is the actual.
    fn instance(&mut self, inst: Expression<'d>) -> Result<PropId, LoweringError> {
        // As for a sequence formal (see `super::build_instance`): the actual was
        // written at the call site, so it hangs off the call site's chain.
        let origin =
            formal_reference_origin(self.tree.syntax(&inst), &self.leaves.env).map(<[_]>::to_vec);
        let Some(origin) = origin else {
            return self.expand(inst, false);
        };
        let saved = std::mem::replace(&mut self.leaves.chain, origin);
        let built = self.expand(inst, true);
        self.leaves.chain = saved;
        built
    }

    /// The instance `inst` of a named property, or (`formal_ref`) the reference to
    /// a property formal, whose body is the actual and which is never recursive in
    /// itself: the actual is built as written.
    fn expand(&mut self, inst: Expression<'d>, formal_ref: bool) -> Result<PropId, LoweringError> {
        let args = inst.assertion_arguments();
        for g in &args {
            // 16.12.19: the local variable formals of a property are inputs.
            if g.port.assertion_port_is_local_var()
                && !matches!(
                    g.port.assertion_port_direction(),
                    None | Some(ArgumentDirection::In)
                )
            {
                return Err(self.err(&format!(
                    "the `local` formal `{}` of a property must be an `input` (LRM 16.12.19)",
                    g.port.name()
                )));
            }
        }
        let body = inst
            .as_sem_node()
            .children()
            .into_iter()
            .find_map(|c| c.as_assertion_expr());
        if formal_ref {
            let body = body.ok_or_else(|| {
                self.err("the reference to a property formal has no body (the actual)")
            })?;
            return self.expand_body(inst, &args, body, None);
        }

        // The declaration, and what its non-local formals are bound to.
        let name = self.callee_name(inst, &args)?;
        let home = self.home_frame(inst);
        // slang gives the instance it stops unfolding at (one past the first
        // repeat of a recursive declaration) a name but no body and no arguments;
        // it is the same call site as the instance that has a body, whose
        // actuals were written once.
        let call_site = self
            .tree
            .syntax(&inst)
            .map(|n| {
                let r = key(n);
                (r.start, r.end)
            })
            .ok_or_else(|| self.err("a property instance has no syntax node"))?;
        let sites = if body.is_some() {
            let s = self.site_args(&args)?;
            self.sites.insert(call_site, s.clone());
            s
        } else {
            self.sites.get(&call_site).cloned().ok_or_else(|| {
                self.err(&format!(
                    "the instance of `{name}` has no body and no earlier instance of the same \
                     call site to take its actuals from (LRM 16.12.17)"
                ))
            })?
        };
        let bound = self.bind_args(&sites, home);
        let key = match body {
            Some(b) => self.decl_key(b)?,
            None => self
                .frames
                .iter()
                .rev()
                .find(|f| f.name == name)
                .map(|f| f.key)
                .ok_or_else(|| {
                    self.err(&format!(
                        "the instance of `{name}` has no body: slang stops unfolding a \
                         recursive property one level after the first, and no expansion of \
                         `{name}` is in progress to call (LRM 16.12.17)"
                    ))
                })?,
        };
        if let Some(h) = home {
            let here = self.frames[h].key;
            self.edges.insert((here, key));
            // 16.12.17 / F.7: the instance recurses iff its declaration reaches the
            // declaration it is written in (a declaration is its own successor
            // when it instantiates itself).
            if self.reaches(key, here) {
                if let Some(arg) = sites
                    .iter()
                    .zip(&bound)
                    .find_map(|(s, b)| b.mixed.then(|| s.name.clone()))
                {
                    return Err(self.err(&format!(
                        "the actual of the non-local formal `{arg}` in the recursive instance \
                         of `{name}` is an expression over formals of the property it is \
                         written in: it must be one of its formals, a `local` formal's actual, \
                         or mention none (LRM 16.12.17 restriction 4)"
                    )));
                }
                let target = (0..=h).rev().find(|&i| {
                    let f = &self.frames[i];
                    f.key == key
                        && f.formals.len() == bound.len()
                        && f.formals.iter().zip(&bound).all(|((_, r), b)| *r == b.root)
                });
                if let Some(i) = target {
                    // The actuals of a `local` formal are semantic expressions of
                    // the instance, which a body-less one does not have.
                    if body.is_none() && sites.iter().any(|s| s.local) {
                        return Err(self.err(&format!(
                            "the recursive instance of `{name}` is past the point where slang \
                             stops unfolding it, so the actuals of its `local` formals are \
                             unavailable (LRM 16.12.17): the instance recurses only after \
                             the non-local actuals have been permuted or replaced"
                        )));
                    }
                    if body.is_none() && self.frames[i].has_inits {
                        return Err(self.err(&format!(
                            "the recursive instance of `{name}` is past the point where slang \
                             stops unfolding it, so the initialisers of its declared local \
                             variables, with this instance's actuals substituted, are \
                             unavailable (LRM 16.12.17, 16.12.19)"
                        )));
                    }
                    return self.recursive_call(inst, &name, &args, i);
                }
            }
        }
        let Some(body) = body else {
            return Err(self.err(&format!(
                "the instance of `{name}` has no body, and the formal arguments it binds are \
                 no binding of any expansion of `{name}` in progress (LRM 16.12.17: slang \
                 unfolds a recursive property only one level past the first)"
            )));
        };
        self.expand_body(inst, &args, body, Some((name, key, bound)))
    }

    /// Builds the body of an instance (`frame` for a named property, `None` for
    /// the reference to a formal) in place, wrapped in the initialisation of its
    /// local variables.
    fn expand_body(
        &mut self,
        inst: Expression<'d>,
        args: &[sv_lang::AssertionInstanceArg<'d>],
        body: AssertionExpr<'d>,
        frame: Option<(String, DeclKey, Vec<Bound>)>,
    ) -> Result<PropId, LoweringError> {
        // A property declared in a clocking block with no event of its own is
        // clocked by the block's (16.18).
        let block_event = if frame.is_none() || body.kind() == AssertionExprKind::Clocking {
            None
        } else {
            super::enclosing_clocking_event(body, self.tree, &self.scope)?
        };
        let top = self.top;
        let entered = enter_instance(
            &mut self.a,
            &mut self.leaves,
            inst,
            args,
            false,
            self.tree,
            &self.scope,
        )?;
        let pushed = frame.is_some();
        if let Some((name, key, bound)) = frame {
            let has_inits = match &entered.locals {
                Some(l) => l
                    .syms
                    .iter()
                    .any(|s| !is_local_formal(args, s) && s.initializer().is_some()),
                None => false,
            };
            let locals: Vec<(String, LocalVarId)> = match &entered.locals {
                Some(l) => l
                    .syms
                    .iter()
                    .zip(&l.slots)
                    .map(|(s, &slot)| (s.name().to_string(), slot))
                    .collect(),
                None => Vec::new(),
            };
            let locals = locals
                .into_iter()
                .map(|(n, slot)| (n, slot, self.leaves.phys_of(&mut self.a, slot)))
                .collect();
            self.frames.push(PFrame {
                name,
                key,
                formals: args
                    .iter()
                    .zip(bound)
                    .map(|(g, b)| (g.port.name().to_string(), b.root))
                    .collect(),
                locals,
                has_inits,
                entry_adv: self.adv,
                decl: None,
            });
        }
        let built = match block_event {
            Some(event) => self.build_under_clock(event, body.as_sem_node(), top),
            None => self.build_prop(body.as_sem_node()),
        };
        let decl = if pushed {
            self.frames.pop().and_then(|f| f.decl)
        } else {
            None
        };
        let locals = leave_instance(&mut self.leaves, entered);
        let body = built?;
        let Some(l) = locals else {
            if let Some(d) = decl {
                self.decls[d.0 as usize].body = body;
            }
            return Ok(body);
        };
        self.leaves.scope.truncate(l.scope_len);
        if !l.write_back.is_empty() {
            return Err(self.err(
                "a property cannot have a `local` output or inout formal (LRM 16.12.19: the \
                 local variable formals of a property are inputs)",
            ));
        }
        let writes: Vec<_> = l
            .init
            .into_iter()
            .filter_map(|t| match t {
                ir::Transition::LocalVarWrite { var, value } => Some((var, value)),
                _ => None,
            })
            .collect();
        let Some(d) = decl else {
            if writes.is_empty() {
                return Ok(body);
            }
            return Ok(self.wrap_let(writes, body));
        };
        // A recursive call re-enters the body without these writes: it rebinds the
        // formals and initialises the declared locals itself, from the
        // initialisers of the instance it stands for (`recursive_call`). slang
        // substitutes the actuals of this instance into the initialisers above,
        // so they are right for this entry only.
        self.decls[d.0 as usize].body = body;
        if writes.is_empty() {
            return Ok(body);
        }
        Ok(self.wrap_let(writes, body))
    }

    /// The semantic leading clocks of property `p` (16.13.7, 16.16.1): the clocks
    /// its first evaluation can be aligned to. A sequence leads with its own first
    /// clock, an implication with its antecedent's, `and`/`or` with both
    /// operands', a clocked property with its clock, and any other operator with
    /// the context clock it stands in.
    fn lead_clocks(&self, p: PropId, out: &mut BTreeSet<ClockId>) {
        match &self.props[p.0 as usize] {
            Prop::Seq { seq, .. } => {
                out.insert(seq.clock);
            }
            Prop::Implication { ante, .. } => {
                out.insert(ante.clock);
            }
            Prop::And(x, y) | Prop::Or(x, y) => {
                self.lead_clocks(*x, out);
                self.lead_clocks(*y, out);
            }
            Prop::Not(x) => self.lead_clocks(*x, out),
            Prop::Clocked { clock, .. } => {
                out.insert(*clock);
            }
            Prop::Let { body, .. } => self.lead_clocks(*body, out),
            Prop::If { .. }
            | Prop::Case { .. }
            | Prop::Nexttime { .. }
            | Prop::Always { .. }
            | Prop::Eventually { .. }
            | Prop::Until { .. }
            | Prop::Abort { .. }
            | Prop::Call { .. } => {
                out.insert(self.leaves.cur);
            }
        }
    }

    /// The initialisation of an instance's declared local variables around its
    /// body, `Let { writes, body }` -- or, when the body has several semantic
    /// leading clocks, one `Let` per operand of the `and`/`or`s that lead it, each
    /// below the `Clocked` wrapper it stands in, so every leading clock gets a
    /// copy of the locals initialised at ITS first tick and the copies are then
    /// checked independently (16.13.7). Single-clock bodies are wrapped whole, as
    /// before.
    fn wrap_let(&mut self, writes: Vec<(LocalVarId, LeafId)>, body: PropId) -> PropId {
        let mut leads = BTreeSet::new();
        self.lead_clocks(body, &mut leads);
        if leads.len() < 2 {
            return self.push(Prop::Let { writes, body });
        }
        self.let_per_clock(&writes, body)
    }

    /// [`Self::wrap_let`]'s push-down.
    fn let_per_clock(&mut self, writes: &[(LocalVarId, LeafId)], p: PropId) -> PropId {
        match self.props[p.0 as usize].clone() {
            Prop::And(x, y) => {
                let (x, y) = (self.let_per_clock(writes, x), self.let_per_clock(writes, y));
                self.push(Prop::And(x, y))
            }
            Prop::Or(x, y) => {
                let (x, y) = (self.let_per_clock(writes, x), self.let_per_clock(writes, y));
                self.push(Prop::Or(x, y))
            }
            Prop::Clocked { clock, p } => {
                let inner = self.push(Prop::Let {
                    writes: writes.to_vec(),
                    body: p,
                });
                self.push(Prop::Clocked { clock, p: inner })
            }
            _ => self.push(Prop::Let {
                writes: writes.to_vec(),
                body: p,
            }),
        }
    }

    /// The call of the expansion `frames[target]` by the recursive instance
    /// `args` of `name` written in it (or below it), checking restriction 3 of
    /// 16.12.17: time must have advanced since that expansion began.
    fn recursive_call(
        &mut self,
        inst: Expression<'d>,
        name: &str,
        args: &[sv_lang::AssertionInstanceArg<'d>],
        target: usize,
    ) -> Result<PropId, LoweringError> {
        if self.adv == self.frames[target].entry_adv {
            return Err(self.err(&format!(
                "the recursive instance of `{name}` is not after a positive guaranteed advance \
                 in time since the instance it recurses into began: a cycle of the dependency \
                 digraph of `{name}` has total weight 0 (LRM 16.12.17 restriction 3)"
            )));
        }
        let mut call_args = Vec::new();
        for g in args {
            if !g.port.assertion_port_is_local_var() {
                continue;
            }
            let formal = g.port.name();
            let var = self.frames[target]
                .locals
                .iter()
                .find(|(n, _, _)| n == formal)
                .map(|&(_, _, v)| v)
                .ok_or_else(|| {
                    self.err(&format!(
                        "the `local` formal `{formal}` of the recursive instance of `{name}` \
                         has no slot in the expansion it calls"
                    ))
                })?;
            let actual = g.actual.as_expression().ok_or_else(|| {
                self.err(&format!(
                    "the actual of the `local` formal `{formal}` is not an expression"
                ))
            })?;
            call_args.extend(self.leaves.slot_leaves(
                &mut self.a,
                var,
                actual,
                None,
                &self.scope,
            )?);
        }
        // The declared locals of the instance, initialised as the instance's own
        // initialisers say (the actuals already substituted by slang), into the
        // slots of the expansion called. An initialiser reads the instance's
        // earlier declared locals, which are those slots.
        let mut inits = Vec::new();
        if self.frames[target].has_inits {
            let scope_len = self.leaves.scope.len();
            let built = self.recursive_inits(inst, name, args, target, &mut inits);
            self.leaves.scope.truncate(scope_len);
            built?;
        }
        let decl = match self.frames[target].decl {
            Some(d) => d,
            None => {
                let d = DeclId(self.decls.len() as u32);
                self.decls.push(PropDecl {
                    name: name.to_string(),
                    // Set when the expansion the declaration stands for is built.
                    body: PropId(0),
                });
                self.frames[target].decl = Some(d);
                d
            }
        };
        Ok(self.push(Prop::Call {
            decl,
            args: call_args,
            inits,
        }))
    }

    /// The `inits` of a [`Prop::Call`] of the expansion `frames[target]` by `inst`.
    /// Leaves the declared locals of `inst` in `leaves.scope`, bound to the slots
    /// of the expansion called (the caller truncates it).
    fn recursive_inits(
        &mut self,
        inst: Expression<'d>,
        name: &str,
        args: &[sv_lang::AssertionInstanceArg<'d>],
        target: usize,
        inits: &mut Vec<(LocalVarId, LeafId)>,
    ) -> Result<(), LoweringError> {
        for sym in inst.assertion_local_vars() {
            if is_local_formal(args, &sym) {
                continue;
            }
            let (canon, phys) = self.frames[target]
                .locals
                .iter()
                .find(|(n, _, _)| n == sym.name())
                .map(|&(_, c, p)| (c, p))
                .ok_or_else(|| {
                    self.err(&format!(
                        "the declared local `{}` of the recursive instance of `{name}` has no \
                         slot in the expansion it calls",
                        sym.name()
                    ))
                })?;
            self.leaves.scope.push(ScopeVar { sym, slot: canon });
            if let Some(initializer) = sym.initializer() {
                inits.extend(self.leaves.slot_leaves(
                    &mut self.a,
                    phys,
                    initializer,
                    None,
                    &self.scope,
                )?);
            }
        }
        Ok(())
    }

    /// The name of the property `inst` instantiates.
    fn callee_name(
        &self,
        inst: Expression<'d>,
        args: &[sv_lang::AssertionInstanceArg<'d>],
    ) -> Result<String, LoweringError> {
        if let Some(parent) = args.first().and_then(|g| g.port.parent()) {
            return Ok(parent.name().to_string());
        }
        let syn = self
            .tree
            .syntax(&inst)
            .ok_or_else(|| self.err("a property instance has no syntax node"))?;
        let text = syn.text();
        let name = text.split('(').next().unwrap_or_default().trim();
        if name.is_empty() {
            return Err(self.err("a property instance has no name"));
        }
        Ok(name.to_string())
    }

    /// The identity of the declaration whose body is `body`.
    fn decl_key(&self, body: AssertionExpr<'d>) -> Result<DeclKey, LoweringError> {
        let r: Range<usize> = key(self.tree.syntax(&body).ok_or_else(|| {
            self.err(
                "a property declaration has no syntax node in any source file of the \
                 compilation (a declaration slang made up)",
            )
        })?);
        Ok((r.start, r.end))
    }

    /// The expansion in progress whose declaration `inst` is written in: the
    /// innermost one whose body contains the instance's syntax. `None` for an
    /// instance written in the assertion statement (or in an actual that was).
    fn home_frame(&self, inst: Expression<'d>) -> Option<usize> {
        let r = key(self.tree.syntax(&inst)?);
        self.frames
            .iter()
            .rposition(|f| f.key.0 <= r.start && r.end <= f.key.1)
    }

    /// The syntax of every actual of the instance `args` (see [`ArgSite`]).
    fn site_args(
        &self,
        args: &[sv_lang::AssertionInstanceArg<'d>],
    ) -> Result<Vec<ArgSite>, LoweringError> {
        let mut out = Vec::with_capacity(args.len());
        for g in args {
            let name = g.port.name().to_string();
            if g.port.assertion_port_is_local_var() {
                out.push(ArgSite {
                    name,
                    local: true,
                    text: (0, 0),
                    bare: None,
                    idents: Vec::new(),
                });
                continue;
            }
            let syn = actual_syntax(g.actual, self.tree)
                .or_else(|| self.tree.syntax(&g.actual.as_assertion_expr()?))
                // An `event`-typed formal's actual is a clocking event (16.12.18).
                .or_else(|| self.tree.syntax(&g.actual.as_timing_control()?))
                .ok_or_else(|| {
                    self.err(&format!(
                        "the actual of the formal `{name}` has no syntax node"
                    ))
                })?;
            let r = key(syn);
            let ident = |n| {
                IdentifierNameSyntax::cast(n)
                    .and_then(|i| i.identifier())
                    .map(|t| t.value_text().to_string())
            };
            out.push(ArgSite {
                name,
                local: false,
                text: (r.start, r.end),
                bare: ident(syn),
                idents: syn.descendants().filter_map(ident).collect(),
            });
        }
        Ok(out)
    }

    /// Classifies the actuals of an instance written in the expansion
    /// `frames[home]` (see [`Bound`]).
    fn bind_args(&self, sites: &[ArgSite], home: Option<usize>) -> Vec<Bound> {
        let mut out = Vec::with_capacity(sites.len());
        for s in sites {
            if s.local {
                out.push(Bound {
                    root: None,
                    mixed: false,
                });
                continue;
            }
            let text = s.text;
            let Some(h) = home else {
                out.push(Bound {
                    root: Some(Root { text, home: None }),
                    mixed: false,
                });
                continue;
            };
            let formals = &self.frames[h].formals;
            let bare = s
                .bare
                .as_ref()
                .and_then(|id| formals.iter().find(|(n, _)| n == id));
            let bound = match bare {
                // A formal passed on as it is: the same binding as its own.
                Some((_, Some(root))) => Bound {
                    root: Some(root.clone()),
                    mixed: false,
                },
                // A `local` formal passed to a non-local one: a value of this
                // expansion, which restriction 4 forbids in a recursive instance.
                Some((_, None)) => Bound {
                    root: Some(Root {
                        text,
                        home: Some(h),
                    }),
                    mixed: true,
                },
                None => {
                    let mentions = s
                        .idents
                        .iter()
                        .any(|id| formals.iter().any(|(f, _)| f == id));
                    Bound {
                        root: Some(Root {
                            text,
                            home: mentions.then_some(h),
                        }),
                        mixed: mentions,
                    }
                }
            };
            out.push(bound);
        }
        out
    }

    /// Whether `from` reaches `to` in the dependency digraph found so far (a
    /// declaration reaches itself).
    fn reaches(&self, from: DeclKey, to: DeclKey) -> bool {
        let mut seen = BTreeSet::new();
        let mut stack = vec![from];
        while let Some(k) = stack.pop() {
            if k == to {
                return true;
            }
            if !seen.insert(k) {
                continue;
            }
            stack.extend(
                self.edges
                    .range((k, (0, 0))..)
                    .take_while(|(f, _)| *f == k)
                    .map(|&(_, t)| t),
            );
        }
        false
    }

    /// Whether the declaration `key` is on a cycle of the dependency digraph
    /// (16.12.17: recursive, directly or through others).
    fn on_cycle(&self, key: DeclKey) -> bool {
        self.edges
            .range((key, (0, 0))..)
            .take_while(|(f, _)| *f == key)
            .any(|&(_, t)| self.reaches(t, key))
    }

    /// `disable iff (cond) p` (16.12, 16.15): legal only as the whole of the
    /// property spec (`top`), and not in the declaration of a recursive property
    /// (16.12.17 restriction 2). It is not a property operator: the condition is
    /// recorded as [`PropertyIr::disable`] and the node builds to `p` alone, the
    /// engine reading the condition at every time step of an attempt (16.12.1:
    /// "an attempt is disabled if the condition is true at any time ...").
    fn build_disable_iff(
        &mut self,
        x: AssertionExpr<'d>,
        top: bool,
    ) -> Result<PropId, LoweringError> {
        let ch = crate::sva::op::disable_iff_children(x, &self.scope)?;
        // The guarded property first: a recursive instance in it closes the cycle
        // through the declaration this `disable iff` is written in.
        let in_decl = self.tree.syntax(&x).and_then(|n| {
            let r = key(n);
            self.frames
                .iter()
                .rposition(|f| f.key.0 <= r.start && r.end <= f.key.1)
        });
        let body = self.build_prop(ch.body.as_sem_node())?;
        if let Some(h) = in_decl {
            let key = self.frames[h].key;
            if self.on_cycle(key) {
                return Err(self.err(&format!(
                    "`disable iff` in the declaration of the recursive property `{}` (LRM 16.12.17 \
                     restriction 2)",
                    self.frames[h].name
                )));
            }
        }
        if !top {
            return Err(self.err(
                "`disable iff` is legal only as the outermost operator of a property \
                 specification: it cannot be nested in a property expression, in a property \
                 whose instance is itself under a `disable iff`, or be the actual of a \
                 property operand (LRM 16.12, 16.15)",
            ));
        }
        // 16.15: the condition "shall not contain any reference to local
        // variables or the sequence method `matched`".
        let e = ch.condition.as_expression().ok_or_else(|| {
            self.err(
                "the condition of a `disable iff` is not an expression (unexpected SemNode kind)",
            )
        })?;
        // 16.14.7: `$inferred_disable` is the `default disable iff` of the
        // instantiation context (else `1'b0`): exactly what an assertion with no
        // `disable iff` of its own gets, so it records no condition here and the
        // emitter applies the default (rule b/c of 16.15).
        if e.call_subroutine_name().as_deref() == Some("$inferred_disable") {
            self.leaves.disable_inferred = true;
            return Ok(body);
        }
        let mut points = Vec::new();
        collect_end_points(e, &mut points);
        if points.iter().any(|(m, _)| *m == ir::EndMethod::Matched) {
            return Err(self.err(
                "a `disable iff` condition shall not contain the sequence method `.matched` \
                 (LRM 16.15)",
            ));
        }
        let (mut locals, mut lvalue) = (Vec::new(), false);
        collect_local_reads(ch.condition, &mut locals, &mut lvalue);
        if let Some(v) = locals.first() {
            return Err(self.err(&format!(
                "a `disable iff` condition shall not reference the local variable `{}` \
                 (LRM 16.15)",
                v.name()
            )));
        }
        let cond = self.leaf(ch.condition, "disable iff condition")?;
        self.disable = Some(cond);
        Ok(body)
    }

    /// Seals the build: drops the nodes nothing reaches, keeps the sequences'
    /// states in the order the nodes are numbered and prunes the rest.
    fn finish(mut self, root: PropId) -> (PropertyIr, LeafTable<'d>) {
        let mut keep = vec![false; self.props.len()];
        let mut stack = vec![root];
        stack.extend(self.decls.iter().map(|d| d.body));
        while let Some(id) = stack.pop() {
            if std::mem::replace(&mut keep[id.0 as usize], true) {
                continue;
            }
            stack.extend(operands(&self.props[id.0 as usize]));
        }
        let mut new_id = vec![None; self.props.len()];
        let mut props = Vec::new();
        for (i, p) in self.props.drain(..).enumerate() {
            if keep[i] {
                new_id[i] = Some(PropId(props.len() as u32));
                props.push(p);
            }
        }
        let map = |id: PropId| new_id[id.0 as usize].expect("a kept node's operands are kept");
        for p in &mut props {
            for id in operands_mut(p) {
                *id = map(*id);
            }
        }
        for d in &mut self.decls {
            d.body = map(d.body);
        }
        let root = map(root);
        let nv_rules: Vec<(PropId, NvRule)> = self
            .nv_rules
            .iter()
            .filter_map(|(id, rule)| new_id[id.0 as usize].map(|n| (n, *rule)))
            .collect();
        let roots: Vec<ThreadStateId> = props
            .iter_mut()
            .filter_map(|p| seqs_mut(p).map(|s| s.entry))
            .collect();
        let renumber = prune_from(&mut self.a, &roots);
        for p in &mut props {
            if let Some(s) = seqs_mut(p) {
                s.entry = renumber[s.entry.0 as usize].expect("a sequence's entry is a root");
            }
        }
        (
            PropertyIr {
                automaton: self.a,
                props,
                decls: self.decls,
                root,
                disable: self.disable,
                nv_rules,
            },
            self.leaves,
        )
    }
}

/// Whether `e` is an instance of a named property (or a property-typed formal)
/// rather than a Boolean or a sequence instance.
fn is_property_instance(e: Expression<'_>) -> bool {
    e.kind() == ExpressionKind::AssertionInstance
        && e.expr_type().is_some_and(|t| t.is_property_type())
}

#[cfg(test)]
mod tests;