vj-sim 0.2.0

//! Task 7 (sva T7, `docs/superpowers/plans/2026-10-03-sva.md`): the
//! clock-flow / clock-resolution query layer -- LRM 1800-2023 16.13.3 (clock
//! flow), 16.16 (clock resolution), 16.16.1 (semantic leading clocks for
//! multiclocked sequences/properties). Per plan §1.1/§1.6 -- the plan's own
//! "single biggest de-risking fact" -- slang has *already* implemented
//! 16.13.3's clock-flow algorithm and 16.16/16.16.1's resolution/uniqueness
//! rules inside `AnalyzedAssertion`
//! (`slang::analysis::AnalyzedAssertion::getClock`/
//! `getSemanticLeadingClock`, vendored C++
//! `source/analysis/AnalyzedAssertion.cpp`). This module is a thin, typed
//! wrapper over that existing analysis -- never a second,
//! independently-reasoned reimplementation of clock-flow/resolution, for
//! the identical reason T6's `inferred_clock` module gives for 16.14.6.
//!
//! ## Deviation from the plan's literal §1.6 text (recorded here as binding)
//!
//! Plan §1.6 describes the query surface as `fn semantic_leading_clocks(&self)
//! -> Vec<TimingControl>` ("empty/plural per 16.16.1's set definition -- a
//! non-unique set is a legality error the CALLER must raise, not this
//! layer's job"). The real `sv-lang` 0.1.9 surface does not match that
//! shape: `AnalyzedAssertion::semantic_leading_clock()` already returns a
//! single `Option<SemNode>` -- it is defined in the vendored C++ as
//! `getClock(getRoot())` (`AnalyzedAssertion.cpp`), which looks up a
//! *single* resolved clock per assertion, not a set. The LRM 16.16.1
//! "set of semantic leading clocks" notion (plural, inductively defined
//! over a bare property/sequence tree independent of any one assert
//! statement) is a concept slang's own `AssertionVisitor` consumes
//! internally while building that single resolved value and while deciding
//! legality -- it is not re-exposed to callers as a set, and no accessor in
//! this `sv-lang` version exposes it as one. So:
//!
//! - [`semantic_leading_clock`] below returns `Option<TimingControl>`, not a
//!   `Vec`.
//! - **The non-unique-clock legality error (16.16 rule (e)/16.16.1) turns
//!   out to behave very differently from the plan's "the caller must raise
//!   it" framing -- verified live, not assumed.** slang raises it ITSELF, as
//!   its own `NoUniqueClock` analysis diagnostic
//!   (`slang::diagnostics::AnalysisDiags::NoUniqueClock`), inside the
//!   `AnalyzedAssertion` constructor -- and
//!   `AnalysisManager::handleAssertion` (`source/analysis/
//!   AnalysisManager.cpp`: `if (!assertion->bad) { ...register it... }`,
//!   with an empty, unwritten `else`) then DISCARDS that `AnalyzedAssertion`
//!   unconditionally, rather than handing it back marked bad. Confirmed
//!   against the LRM's own `examples_with_default` worked module (16.16,
//!   `a5: assert property (q6); // illegal: ... semantic leading clock is
//!   not unique`, reproduced verbatim in this module's tests below): `a5`
//!   never appears in `Analysis::assertions()`'s output at all; the ONLY
//!   observable trace of its illegality is the `NoUniqueClock` entry in
//!   `Analysis::diagnostics()`. There is therefore no `AnalyzedAssertion`
//!   handle left for a caller to call `semantic_leading_clock()` on and get
//!   an error back -- this module's query layer cannot "raise" anything
//!   per-assertion for this case; the only correct way to detect it is
//!   [`has_non_unique_clock_error`] over the whole `Analysis`'s
//!   diagnostics, which this module provides instead of the plan's assumed
//!   per-call error return.
//! - The identical silent-discard shape applies to 16.16 rule (f)'s "no
//!   clock at all" violation (slang's `AssertionNoClock` diagnostic) -- see
//!   [`has_no_clock_error`].
//!
//! ## Confirmed, named gap: LRM 16.16 rule (c)+(e) interaction (`a3`)
//!
//! The LRM's own `examples_with_default` module (16.16) marks
//! `a3: assert property ($fell(c) |=> q2);` illegal -- "multiclocked
//! property with contextually inferred leading clocking event" -- inside
//! `always @(negedge clk) begin ... end`, where `q2` is `property q2;
//! @(posedge clk) q1; endproperty` (its own fixed clock). Per rule (e)'s
//! text, a MULTICLOCKED property used as the maximal property of an
//! assertion statement may inherit only the DEFAULT clocking event as its
//! leading clock, never a contextually inferred one; `$fell(c) |=> q2` is
//! multiclocked (its consequent carries a fixed clock different from its
//! antecedent's) and the clock it would need to inherit here is the always
//! block's CONTEXTUALLY INFERRED `negedge clk` (rule (c)), not the module's
//! `default clocking posedge_clk` -- so the LRM marks this combination
//! illegal.
//!
//! **Verified live
//! ([`tests::a3_examples_with_default_is_accepted_not_rejected_known_gap`]):
//! slang 0.1.9 does NOT reject this.** It resolves `a3`'s semantic leading
//! clock to `negedge clk` and raises no diagnostic at all. The root cause is
//! structural, and the SAME one T6's module doc already names for a
//! different symptom: `AnalyzedProcedure::getInferredClock()` folds the
//! procedural-inferred clock (rule (c)) and the default-clocking fallback
//! (rule (e)'s own "default" source) into ONE `const TimingControl*` value
//! with no tag saying which rule produced it (`AnalyzedProcedure::
//! AnalyzedProcedure`, ~lines 54-66), and that SAME merged value is the only
//! `outerClock` the `AssertionVisitor` building `a3`'s `AnalyzedAssertion`
//! ever sees (`propSpec.visit(visitor, procedure.getInferredClock(),
//! ...)`) -- the visitor's multiclock-inheritance check
//! (`AssertionVisitor::inheritedClock`, `AnalyzedAssertion.cpp`) has no way
//! to tell "this outer clock came from rule (c), not rule (e)'s default" and
//! so cannot apply rule (e)'s default-only restriction. Per plan
//! §1.1/§1.2's explicit decision not to reimplement 16.13.3/16.16's
//! clock-flow/resolution algorithm a second time, and per T6's own
//! precedent (documenting rather than working around an equivalent
//! `sv-lang` 0.1.9 API-shape gap it cannot fix without touching the pinned
//! `sv-lang` dependency), this module does not attempt to re-derive rule
//! (c)/(e)'s distinction from information `sv-lang` 0.1.9 does not expose --
//! `AnalyzedProcedure` has no lower-level accessor that would let it (the
//! same unavailable-surface conclusion T6's own module doc reaches for its
//! "is this really (a)-(c), or the default fallback" question). This is a
//! confirmed, named limitation, not a silently-accepted one: the test named
//! above pins down the CURRENT (non-LRM-compliant for this one rule)
//! behavior so a future `sv-lang` upgrade that exposes clock provenance
//! separately breaks it loudly, rather than this module silently keeping a
//! stale claim.
//!
//! ## No probe-corpus fixture (deviation from the plan's literal "Tests:" text)
//!
//! The plan's own "Tests:" text asks for these worked examples "reproduced
//! as probe-corpus fixtures" run through `vj run`. That path does not
//! exist for this task: concurrent-assertion lowering/simulation is not
//! wired up until T9 onward (the automaton builder) and T29 (the
//! `assert`/`cover`/... statement lowering that would make `vj run`
//! even attempt one), so any `.sv` fixture exercising a clocked assertion
//! today hits the same generic "concurrent assertions are deferred" error
//! every other not-yet-lowered construct does (confirmed by the existing
//! `sva_boolean_leaf_restrictions` probe-corpus fixture, T5, whose
//! `Verdict::KnownGap` owner is explicitly "sva T29", not T5) -- a
//! `vj run`-based fixture here would carry no clock-resolution-specific
//! signal at all. T1 already set this precedent for the same reason (its
//! own `sched::control`-only commit never added the `sva_preponed_sampling`
//! fixture its task text names). This module's frontend-only unit tests
//! below, which compile+analyze the LRM's exact worked modules through a
//! live `sv_lang::Design`/`Analysis` -- the actual object this layer
//! queries -- are the fixtures that matter for this task.

use sv_lang::{AnalyzedAssertion, Diagnostics, SemNode, TimingControl};

use super::super::analysis::AnalysisError;

/// LRM 16.13.3's clock-flow result for `node`, a sub-expression of
/// `assertion.root()` (`slang::analysis::AnalyzedAssertion::getClock`).
/// `Ok(None)` if `node` is itself multiclocked (per the accessor's own doc
/// comment, its own children must be examined individually -- this wrapper
/// draws no finer distinction than the C++ accessor itself makes) or does
/// not belong to `assertion`'s tree at all.
///
/// `Err` only if slang's analysis returns a `SemNode` that is not itself a
/// `TimingControl` -- an API-shape precondition this function depends on,
/// surfaced loudly rather than silently treated as "no clock" if a future
/// `sv-lang` upgrade ever violates it (same posture as T6's
/// `infer_procedural_clock`).
pub fn clock_of<'d>(
    assertion: &AnalyzedAssertion<'d>,
    node: SemNode<'d>,
) -> Result<Option<TimingControl<'d>>, AnalysisError> {
    as_timing_control(assertion.clock(node))
}

/// LRM 16.16.1's semantic leading clock of the whole assertion
/// (`slang::analysis::AnalyzedAssertion::getSemanticLeadingClock`, ==
/// `getClock(getRoot())` per the vendored C++ -- this is that identity made
/// explicit, not a second, independent accessor). See the module doc's
/// "Deviation" section for why this returns a single value rather than a
/// `Vec`, and for why the illegal-multiclock/no-clock cases cannot be
/// detected from this return value at all -- use
/// [`has_non_unique_clock_error`]/[`has_no_clock_error`] over
/// `Analysis::diagnostics()` instead.
pub fn semantic_leading_clock<'d>(
    assertion: &AnalyzedAssertion<'d>,
) -> Result<Option<TimingControl<'d>>, AnalysisError> {
    as_timing_control(assertion.semantic_leading_clock())
}

fn as_timing_control<'d>(
    node: Option<SemNode<'d>>,
) -> Result<Option<TimingControl<'d>>, AnalysisError> {
    match node {
        None => Ok(None),
        Some(n) => n.as_timing_control().map(Some).ok_or_else(|| {
            AnalysisError::Unsupported(format!(
                "AnalyzedAssertion clock query returned a SemNode of kind `{}` that is not a \
                 TimingControl -- sv-lang API shape assumption violated",
                n.kind_name(),
            ))
        }),
    }
}

/// True if `diags` (`Analysis::diagnostics()`) records LRM 16.16 rule
/// (e)/16.16.1's "multiclocked maximal property/sequence has no unique
/// semantic leading clock" violation (slang's own `NoUniqueClock`). See the
/// module doc: the violating assertion itself is silently absent from
/// `Analysis::assertions()`, so this whole-`Analysis` diagnostic scan is the
/// only way to detect it -- there is no per-assertion accessor that could.
pub fn has_non_unique_clock_error(diags: &Diagnostics) -> bool {
    diags
        .items()
        .iter()
        .any(|d| d.is_error() && d.code_name() == "NoUniqueClock")
}

/// True if `diags` records LRM 16.16 rule (f)'s "no explicit, default, or
/// contextually inferred leading clocking event, and the maximal property is
/// not an instance with its own determined leading clocking event"
/// violation (slang's own `AssertionNoClock`). Same "silently dropped, this
/// diagnostic is the only signal" shape as [`has_non_unique_clock_error`].
pub fn has_no_clock_error(diags: &Diagnostics) -> bool {
    diags
        .items()
        .iter()
        .any(|d| d.is_error() && d.code_name() == "AssertionNoClock")
}

#[cfg(test)]
mod tests {
    use super::*;
    use sv_lang::{Analysis, AnalysisFlags, Compilation, EdgeKind, Session, Symbol};

    fn compile(src: &str) -> sv_lang::Design {
        let session = Session::new();
        let mut comp = Compilation::new(&session).expect("session");
        comp.add_source(src).expect("add_source");
        comp.compile().expect("compiles")
    }

    fn top_body<'d>(design: &'d sv_lang::Design) -> Symbol<'d> {
        design
            .top_instances()
            .next()
            .expect("one top instance")
            .instance_body()
            .expect("instance body")
    }

    /// Every `AnalyzedAssertion` reachable from any procedure in `body`,
    /// keyed by its statement's starting byte offset in the source --
    /// `sv-lang` 0.1.9 exposes no statement-label accessor, so this is how
    /// these tests identify *which* LRM-labeled assertion (`a1:`, `c4:`,
    /// ...) a given `AnalyzedAssertion` is (a 16.14.6-style "static
    /// concurrent assertion" is itself modeled by slang as its own
    /// one-statement synthetic procedure -- confirmed live during this
    /// task's own investigation -- so walking `Analysis::procedures` finds
    /// static assertions too, not only ones inside a real `always` block).
    fn assertions_by_offset<'d>(
        analysis: &'d Analysis<'d>,
        body: Symbol<'d>,
    ) -> std::collections::BTreeMap<usize, AnalyzedAssertion<'d>> {
        let mut out = std::collections::BTreeMap::new();
        for proc in analysis.procedures(body) {
            for a in analysis.assertions(proc.symbol()) {
                let off = a
                    .ast_node()
                    .as_statement()
                    .expect("a concurrent assertion statement")
                    .source_range()
                    .start
                    .offset as usize;
                out.insert(off, a);
            }
        }
        out
    }

    /// `(edge, referenced-signal-name)` of `tc`'s own event expression (the
    /// first child, per `TimingControl::children()`'s `SignalEvent` shape --
    /// the same shape T6's tests already rely on).
    fn edge_and_signal(tc: TimingControl<'_>) -> (EdgeKind, Option<String>) {
        let sig = tc
            .children()
            .first()
            .and_then(|c| c.as_expression())
            .and_then(|e| e.referenced_symbol())
            .map(|s| s.name().to_string());
        (tc.edge(), sig)
    }

    /// The LRM's own `examples_with_default` module (16.16), reproduced
    /// verbatim (including its own `a1`..`a6`/`c1`..`c2` labels and
    /// "legal"/"illegal" comments).
    const EXAMPLES_WITH_DEFAULT: &str = "
module examples_with_default (input logic a, b, c, clk);
   property q1;
      $rose(a) |-> ##[1:5] b;
   endproperty
   property q2;
      @(posedge clk) q1;
   endproperty
   default clocking posedge_clk @(posedge clk);
      property q3;
         $fell(c) |=> q1;
         // legal: q1 has no clocking event
      endproperty
      property q4;
         $fell(c) |=> q2;
         // legal: q2 has clocking event identical to that of the clocking block
      endproperty
   endclocking
   property q5;
      @(negedge clk) b[*3] |=> !b;
   endproperty
   always @(negedge clk)
   begin
      a1: assert property ($fell(c) |=> q1);
         // legal: contextually inferred leading clocking event, @(negedge clk)
      a2: assert property (posedge_clk.q4);
         // legal: will be queued (pending) on negedge clk, then (if matured)
         // checked at next posedge clk (see 16.14.6)
      a3: assert property ($fell(c) |=> q2);
         // illegal: multiclocked property with contextually inferred leading
         // clocking event
      a4: assert property (q5);
         // legal: contextually inferred leading clocking event, @(negedge clk)
   end
   property q6;
      q1 and q5;
   endproperty
   a5: assert property (q6);
      // illegal: default leading clocking event, @(posedge clk), but
      // semantic leading clock is not unique
   a6: assert property ($fell(c) |=> q6);
      // legal: default leading clocking event, @(posedge clk), is the
      // unique semantic leading clock
   sequence s2;
      $rose(a) ##[1:5] b;
   endsequence
   c1: cover property (s2);
      // legal: default leading clocking event, @(posedge clk)
   c2: cover property (@(negedge clk) s2);
      // legal: explicit leading clocking event, @(negedge clk)
endmodule
";

    /// The LRM's own `examples_without_default` module (16.16), reproduced
    /// verbatim.
    const EXAMPLES_WITHOUT_DEFAULT: &str = "
module examples_without_default (input logic a, b, c, clk);
   property q1;
      $rose(a) |-> ##[1:5] b;
   endproperty
   property q5;
      @(negedge clk) b[*3] |=> !b;
   endproperty
   property q6;
      q1 and q5;
   endproperty
   a5: assert property (q6);
      // illegal: no leading clocking event
   a6: assert property ($fell(c) |=> q6);
      // illegal: no leading clocking event
   sequence s2;
      $rose(a) ##[1:5] b;
   endsequence
   c1: cover property (s2);
      // illegal: no leading clocking event
   c2: cover property (@(negedge clk) s2);
      // legal: explicit leading clocking event, @(negedge clk)
   sequence s3;
      @(negedge clk) s2;
   endsequence
   c3: cover property (s3);
      // legal: leading clocking event, @(negedge clk), determined from
      // declaration of s3
   c4: cover property (s3 ##1 b);
      // illegal: no default, inferred, or explicit leading clocking event
      // and maximal property is not an instance
endmodule
";

    /// `a1`, `a2`, `a4`: the three LEGAL contextually-inferred-clock cases
    /// in `examples_with_default` each resolve to the expected concrete
    /// clock, via [`semantic_leading_clock`] -- never a reimplementation, a
    /// direct query of `AnalyzedAssertion`.
    #[test]
    fn legal_contextually_inferred_cases_resolve_expected_clock() {
        let design = compile(EXAMPLES_WITH_DEFAULT);
        let body = top_body(&design);
        let analysis = design.analyze(AnalysisFlags::NONE, 1).expect("analysis");
        let by_offset = assertions_by_offset(&analysis, body);

        let a1 = by_offset[&EXAMPLES_WITH_DEFAULT.find("a1:").unwrap()];
        let tc = semantic_leading_clock(&a1)
            .expect("no API-shape error")
            .expect("a1's clock is resolved");
        assert_eq!(edge_and_signal(tc), (EdgeKind::NegEdge, Some("clk".into())));

        // a2: `posedge_clk.q4` -- an explicit reference into the default
        // clocking block, so its clock is the BLOCK's own event regardless
        // of the enclosing `always @(negedge clk)` context.
        let a2 = by_offset[&EXAMPLES_WITH_DEFAULT.find("a2:").unwrap()];
        let tc = semantic_leading_clock(&a2)
            .expect("no API-shape error")
            .expect("a2's clock is resolved");
        assert_eq!(edge_and_signal(tc), (EdgeKind::PosEdge, Some("clk".into())));

        let a4 = by_offset[&EXAMPLES_WITH_DEFAULT.find("a4:").unwrap()];
        let tc = semantic_leading_clock(&a4)
            .expect("no API-shape error")
            .expect("a4's clock is resolved");
        assert_eq!(edge_and_signal(tc), (EdgeKind::NegEdge, Some("clk".into())));
    }

    /// `a6`, `c1`: the two LEGAL default-clocking cases in
    /// `examples_with_default` resolve to the default clocking block's own
    /// event, `@(posedge clk)`.
    #[test]
    fn legal_default_clocking_cases_resolve_default_event() {
        let design = compile(EXAMPLES_WITH_DEFAULT);
        let body = top_body(&design);
        let analysis = design.analyze(AnalysisFlags::NONE, 1).expect("analysis");
        let by_offset = assertions_by_offset(&analysis, body);

        for tag in ["a6:", "c1:"] {
            let a = by_offset[&EXAMPLES_WITH_DEFAULT.find(tag).unwrap()];
            let tc = semantic_leading_clock(&a)
                .expect("no API-shape error")
                .unwrap_or_else(|| panic!("{tag}'s clock is resolved"));
            assert_eq!(
                edge_and_signal(tc),
                (EdgeKind::PosEdge, Some("clk".into())),
                "{tag} resolves to the default clocking event"
            );
        }
    }

    /// `c2`: the LEGAL explicit-leading-clock case in `examples_with_default`
    /// resolves to its own explicit `@(negedge clk)`, overriding the
    /// default.
    #[test]
    fn legal_explicit_clock_overrides_default() {
        let design = compile(EXAMPLES_WITH_DEFAULT);
        let body = top_body(&design);
        let analysis = design.analyze(AnalysisFlags::NONE, 1).expect("analysis");
        let by_offset = assertions_by_offset(&analysis, body);

        let c2 = by_offset[&EXAMPLES_WITH_DEFAULT.find("c2:").unwrap()];
        let tc = semantic_leading_clock(&c2)
            .expect("no API-shape error")
            .expect("c2's clock is resolved");
        assert_eq!(edge_and_signal(tc), (EdgeKind::NegEdge, Some("clk".into())));
    }

    /// `a5`: the LRM's own ILLEGAL "semantic leading clock is not unique"
    /// example. Per the module doc's "Deviation" section: the illegal
    /// assertion is silently absent from `Analysis::assertions()`
    /// altogether, and [`has_non_unique_clock_error`] over
    /// `Analysis::diagnostics()` is the only way to detect it.
    #[test]
    fn a5_non_unique_clock_is_dropped_and_diagnosed() {
        let design = compile(EXAMPLES_WITH_DEFAULT);
        let body = top_body(&design);
        let analysis = design.analyze(AnalysisFlags::NONE, 1).expect("analysis");
        let by_offset = assertions_by_offset(&analysis, body);

        let a5_offset = EXAMPLES_WITH_DEFAULT.find("a5:").unwrap();
        assert!(
            !by_offset.contains_key(&a5_offset),
            "a5 is illegal (non-unique semantic leading clock): slang drops it from \
             Analysis::assertions() entirely rather than returning an AnalyzedAssertion \
             a caller could ask semantic_leading_clock() of"
        );
        assert!(
            has_non_unique_clock_error(&analysis.diagnostics()),
            "a5's illegality must be visible as a NoUniqueClock analysis diagnostic"
        );
        assert!(
            !has_no_clock_error(&analysis.diagnostics()),
            "a5's violation is non-uniqueness, not absence of any clock at all"
        );
    }

    /// Confirmed, named gap (see the module doc's own section): `a3` is
    /// marked illegal by the LRM text ("multiclocked property with
    /// contextually inferred leading clocking event") but slang 0.1.9
    /// accepts it, resolving its semantic leading clock to the always
    /// block's contextually inferred `negedge clk` with no diagnostic at
    /// all. This test pins down that ACTUAL (non-LRM-compliant for this one
    /// rule) behavior -- not the LRM's stated answer -- so a future
    /// `sv-lang` upgrade that starts rejecting it (by exposing clock
    /// provenance so this module's wrapper could, in a later task, apply
    /// rule (e)'s default-only restriction) breaks this test loudly instead
    /// of this module's doc comment silently going stale.
    #[test]
    fn a3_examples_with_default_is_accepted_not_rejected_known_gap() {
        let design = compile(EXAMPLES_WITH_DEFAULT);
        let body = top_body(&design);
        let analysis = design.analyze(AnalysisFlags::NONE, 1).expect("analysis");
        let by_offset = assertions_by_offset(&analysis, body);

        let a3_offset = EXAMPLES_WITH_DEFAULT.find("a3:").unwrap();
        let a3 = *by_offset
            .get(&a3_offset)
            .expect("known gap: slang does not drop a3 the way it drops a5");
        let tc = semantic_leading_clock(&a3)
            .expect("no API-shape error")
            .expect("known gap: slang resolves a3's clock instead of rejecting it");
        assert_eq!(
            edge_and_signal(tc),
            (EdgeKind::NegEdge, Some("clk".into())),
            "known gap: a3 resolves to the contextually inferred clock, not an error"
        );
        // `examples_with_default` also contains a5 (the module's OTHER,
        // genuinely-detected illegal case), which does raise a NoUniqueClock
        // diagnostic -- so this checks that a3 contributes no SECOND one of
        // its own, rather than asserting the diagnostics list is empty.
        let non_unique_clock_errors = analysis
            .diagnostics()
            .items()
            .iter()
            .filter(|d| d.is_error() && d.code_name() == "NoUniqueClock")
            .count();
        assert_eq!(
            non_unique_clock_errors, 1,
            "known gap: slang raises no diagnostic for a3 at all -- the one NoUniqueClock \
             error present is a5's, not a3's (LRM says a3 should also be illegal via rule \
             (c)+(e); see the module doc's gap section for the confirmed root cause)"
        );
    }

    /// `c2`, `c3`: the two LEGAL cases in `examples_without_default`.
    #[test]
    fn examples_without_default_legal_cases_resolve_expected_clock() {
        let design = compile(EXAMPLES_WITHOUT_DEFAULT);
        let body = top_body(&design);
        let analysis = design.analyze(AnalysisFlags::NONE, 1).expect("analysis");
        let by_offset = assertions_by_offset(&analysis, body);

        for tag in ["c2:", "c3:"] {
            let a = by_offset[&EXAMPLES_WITHOUT_DEFAULT.find(tag).unwrap()];
            let tc = semantic_leading_clock(&a)
                .expect("no API-shape error")
                .unwrap_or_else(|| panic!("{tag}'s clock is resolved"));
            assert_eq!(
                edge_and_signal(tc),
                (EdgeKind::NegEdge, Some("clk".into())),
                "{tag} resolves to the explicit/declared @(negedge clk)"
            );
        }
    }

    /// `a5`, `a6`, `c1`, `c4`: the four LRM-stated ILLEGAL "no leading
    /// clocking event" cases in `examples_without_default` (rule (f)) --
    /// each dropped from `Analysis::assertions()` and diagnosed via
    /// [`has_no_clock_error`], never [`has_non_unique_clock_error`] (the
    /// violation here is absence of any clock, not non-uniqueness of
    /// several).
    #[test]
    fn examples_without_default_illegal_cases_are_dropped_and_diagnosed() {
        let design = compile(EXAMPLES_WITHOUT_DEFAULT);
        let body = top_body(&design);
        let analysis = design.analyze(AnalysisFlags::NONE, 1).expect("analysis");
        let by_offset = assertions_by_offset(&analysis, body);
        let diags = analysis.diagnostics();

        for tag in ["a5:", "a6:", "c1:", "c4:"] {
            let offset = EXAMPLES_WITHOUT_DEFAULT.find(tag).unwrap();
            assert!(
                !by_offset.contains_key(&offset),
                "{tag} is illegal (no leading clocking event): must be dropped from \
                 Analysis::assertions()"
            );
        }
        assert!(
            has_no_clock_error(&diags),
            "at least one AssertionNoClock diagnostic must be present"
        );
        assert!(
            !has_non_unique_clock_error(&diags),
            "examples_without_default's violations are all rule (f) (no clock at all), never \
             rule (e) (non-unique)"
        );
        // All four violate the SAME rule (f); `AssertionNoClock` is raised
        // once per offending statement, so there must be (at least) four
        // error-severity entries, not merely one.
        let no_clock_errors = diags
            .items()
            .iter()
            .filter(|d| d.is_error() && d.code_name() == "AssertionNoClock")
            .count();
        assert_eq!(
            no_clock_errors, 4,
            "a5, a6, c1, and c4 each raise their own AssertionNoClock diagnostic"
        );
    }

    /// Sanity: [`semantic_leading_clock`] really is just `clock_of` applied
    /// to the assertion's own `root()` -- the module doc's claim that it is
    /// not a second, independent accessor -- confirmed for a case with no
    /// legality wrinkle at all (`c2` of `examples_without_default`).
    #[test]
    fn semantic_leading_clock_agrees_with_clock_of_root() {
        let design = compile(EXAMPLES_WITHOUT_DEFAULT);
        let body = top_body(&design);
        let analysis = design.analyze(AnalysisFlags::NONE, 1).expect("analysis");
        let by_offset = assertions_by_offset(&analysis, body);

        let c2 = by_offset[&EXAMPLES_WITHOUT_DEFAULT.find("c2:").unwrap()];
        let via_slc = semantic_leading_clock(&c2)
            .expect("no API-shape error")
            .expect("c2 has a resolved clock");
        let via_clock_of = clock_of(&c2, c2.root())
            .expect("no API-shape error")
            .expect("c2 has a resolved clock");
        assert_eq!(edge_and_signal(via_slc), edge_and_signal(via_clock_of));
    }
}