vj-codegen 0.1.0

//! sva T28: multiclocked sequences and properties (LRM 16.13.1, 16.13.2, 16.13.4,
//! 16.13.7, 16.16.1).
//!
//! The reference evaluator runs these over a global timeline: every signal row has
//! one sample per time step, and each clock is the list of steps it ticks at. The
//! expected verdicts are worked out by hand from the clause each test cites; a
//! comment on the trace says which tick every sample is read at.
//!
//! `clk` is `ClockId(0)` (the assertion's own clock), the others are numbered in
//! the order the builder meets them, which the tests never rely on: a clock is
//! identified by its event text.
use std::collections::BTreeMap;

use super::*;
use sv_lang::SyntaxTree;

/// The module-level declarations the LRM's 16.13.4 examples share.
const MC: &str = "logic clk1, clk2, f;\n\
    sequence s1; a ##1 b; endsequence\n\
    sequence s2; c ##1 d; endsequence\n\
    sequence mult_s;\n\
      @(posedge clk) a ##1 @(posedge clk1) s1 ##1 @(posedge clk2) s2;\n\
    endsequence\n\
    property mult_p1;\n\
      @(posedge clk) a ##1 @(posedge clk1) s1 ##1 @(posedge clk2) s2;\n\
    endproperty\n\
    property mult_p2;\n\
      mult_s;\n\
    endproperty\n\
    property mult_p3;\n\
      @(posedge clk) a ##1 @(posedge clk1) s1 |=> @(posedge clk2) s2;\n\
    endproperty\n\
    property mult_p6;\n\
      mult_s |=> mult_s;\n\
    endproperty\n\
    property mult_p7;\n\
      @(posedge clk) a ##1 b |-> c ##1 @(posedge clk1) d;\n\
    endproperty\n\
    property mult_p8;\n\
      @(posedge clk) a ##1 b |->\n\
      if (c)\n\
         (1 |=> @(posedge clk1) d)\n\
      else\n\
         e ##1 @(posedge clk2) f ;\n\
    endproperty\n";

/// The text of clock `id`'s event with the `@(...)` stripped and the whitespace
/// removed (`posedgeclk1`), which is how the tests name a clock.
fn clock_key(leaves: &LeafTable<'_>, tree: &SyntaxTree, id: u32) -> String {
    let event = leaves
        .clock_event(ClockId(id))
        .unwrap_or_else(|| panic!("clock {id} has no event"));
    let text: String = event
        .as_timing_control()
        .expect("a clock event is a timing control")
        .syntax(tree)
        .expect("a clock event has syntax")
        .text()
        .split_whitespace()
        .collect();
    let text = text.strip_prefix('@').unwrap_or(&text);
    text.strip_prefix('(')
        .and_then(|t| t.strip_suffix(')'))
        .unwrap_or(text)
        .to_string()
}

/// The verdict of the whole assertion `stmt` on `signals` (one sample per global
/// time step) when each clock ticks at the steps `clocks` marks with a `1`: `clocks`
/// maps a clock's event text (`posedgeclk1`) to its row. The attempt starts at step
/// 0, which the fixtures make a tick of the leading clock. `strong` is a `cover
/// property` reading.
fn mc(
    decls: &str,
    stmt: &str,
    signals: &[(&str, &str)],
    clocks: &[(&str, &str)],
    strong: bool,
) -> Verdict {
    let table = rows(signals);
    let len = table.values().next().expect("a signal").len();
    assert!(table.values().all(|r| r.len() == len), "ragged signal rows");
    let by_event: BTreeMap<&str, &str> = clocks.iter().copied().collect();
    with_property(decls, stmt, false, |r, tree| {
        let (ir, leaves) = r.unwrap_or_else(|e| panic!("`{stmt}` failed to build: {e}"));
        let mut rows_by_id: Vec<Vec<bool>> = Vec::new();
        let mut used = 0;
        for id in 0..leaves.clock_count() as u32 {
            let key = clock_key(&leaves, tree, id);
            let row = by_event
                .get(key.as_str())
                .unwrap_or_else(|| panic!("`{stmt}`: no tick row for clock `{key}`"));
            assert_eq!(row.len(), len, "tick row of `{key}`");
            rows_by_id.push(row.chars().map(|c| c == '1').collect());
            used += 1;
        }
        assert_eq!(
            used,
            by_event.len(),
            "a tick row names no clock of `{stmt}`"
        );
        let refs: Vec<&[bool]> = rows_by_id.iter().map(Vec::as_slice).collect();
        let mut env = Sigs::new(&leaves, &table);
        env.timeline = Some(Timeline::from_rows(&refs));
        Evaluator::new(&ir, &env, strong)
            .verdict(len as u32, 0)
            .unwrap_or_else(|e| panic!("`{stmt}` failed to evaluate: {e}"))
    })
}

/// `mc` for an `assert property (...)` of the shared declarations.
fn mca(prop: &str, signals: &[(&str, &str)], clocks: &[(&str, &str)]) -> Verdict {
    mc(
        MC,
        &format!("assert property ({prop});"),
        signals,
        clocks,
        false,
    )
}

/// The `(to, strict)` of every clock-synchronisation edge of `stmt`'s automaton and
/// the number of distinct clocks, for the statements whose shape matters.
fn sync_shape(decls: &str, stmt: &str) -> (usize, Vec<(u32, bool)>) {
    with_property(decls, stmt, false, |r, _| {
        let (ir, leaves) = r.unwrap_or_else(|e| panic!("`{stmt}` failed to build: {e}"));
        let syncs = ir
            .automaton
            .states
            .iter()
            .flat_map(|st| &st.edges)
            .filter_map(|e| match &e.label {
                Transition::ClockSync { to, strict } => Some((to.0, *strict)),
                _ => None,
            })
            .collect();
        (leaves.clock_count(), syncs)
    })
}

/// The error of a design slang accepts and the builder refuses.
fn refused(decls: &str, stmt: &str) -> String {
    with_property(decls, stmt, false, |r, _| match r {
        Ok(_) => panic!("`{stmt}` was expected to be rejected"),
        Err(e) => e.to_string(),
    })
}

fn passes(v: Verdict) -> bool {
    matches!(v, Verdict::Holds | Verdict::HoldsStrongly)
}

// -- 16.13.4 a, b, c: multiclocked sequences as properties -----------------------

/// 16.13.4 (a)-(c): `mult_s`, `mult_p1` (the same sequence written in the property)
/// and `mult_p2` (the property that names the sequence) all say: `a` at a tick of
/// clk; then `s1 = a ##1 b` on clk1 starting at the first clk1 tick STRICTLY after
/// it (`##1` between clocks, 16.13.1); then `s2 = c ##1 d` on clk2 starting at the
/// first clk2 tick strictly after the end of `s1`.
#[test]
fn mult_s_p1_p2_synchronise_each_clock_change_to_the_next_tick() {
    // clk ticks at 0; clk1 at 1, 3, 5; clk2 at 4, 6, 8.
    let clocks = [
        ("posedgeclk", "1000000000"),
        ("posedgeclk1", "0101010000"),
        ("posedgeclk2", "0000101010"),
    ];
    // a at 0 (clk) and at 1 (s1's first letter on clk1), b at clk1's next tick
    // (3), c at clk2's first tick after 3 (4), d at its next tick (6).
    let good = [
        ("a", "1100000000"),
        ("b", "0001000000"),
        ("c", "0000100000"),
        ("d", "0000001000"),
    ];
    // Every prefix of the match, with one sample moved off its tick.
    let bad_b = [
        ("a", "1100000000"),
        ("b", "0010000000"), // b at 2: not a clk1 tick
        ("c", "0000100000"),
        ("d", "0000001000"),
    ];
    let bad_c = [
        ("a", "1100000000"),
        ("b", "0001000000"),
        ("c", "0001000000"), // c at 3, the end of s1: clk2 does not tick there
        ("d", "0000001000"),
    ];
    let bad_d = [
        ("a", "1100000000"),
        ("b", "0001000000"),
        ("c", "0000100000"),
        ("d", "0000000010"), // d at 8 instead of clk2's next tick (6)
    ];
    for prop in ["mult_p1", "mult_p2"] {
        assert_eq!(mca(prop, &good, &clocks), Verdict::HoldsStrongly, "{prop}");
        for (name, trace) in [("b", &bad_b), ("c", &bad_c), ("d", &bad_d)] {
            assert_eq!(
                mca(prop, trace, &clocks),
                Verdict::Fails,
                "{prop} bad {name}"
            );
        }
    }
    // The sequence as an assertion on its own, and under `cover` (strong: a trace
    // that stops before the match is still waiting, not holding).
    let on_its_own = mc(MC, "assert property (mult_s);", &good, &clocks, false);
    assert_eq!(on_its_own, Verdict::HoldsStrongly);
    let cut = [
        ("a", "11000"),
        ("b", "00010"),
        ("c", "00001"),
        ("d", "00000"),
    ];
    let cut_clocks = [
        ("posedgeclk", "10000"),
        ("posedgeclk1", "01010"),
        ("posedgeclk2", "00001"),
    ];
    // The trace ends after c, before d's tick of clk2: the attempt is pending
    // (nothing has failed, nothing has matched), under either reading.
    for strong in [false, true] {
        assert_eq!(
            mc(MC, "assert property (mult_s);", &cut, &cut_clocks, strong),
            Verdict::Holds,
            "strong = {strong}"
        );
    }
    // The same cut trace with the match broken at c: that is a definite failure.
    let cut_bad = [
        ("a", "11000"),
        ("b", "00010"),
        ("c", "00000"),
        ("d", "00000"),
    ];
    assert_eq!(
        mc(
            MC,
            "assert property (mult_s);",
            &cut_bad,
            &cut_clocks,
            false
        ),
        Verdict::Fails
    );
}

/// The automaton of `mult_s` has exactly the structure 16.13.1 gives it: three
/// clocks and two strict synchronisations, one into each later clock, in order.
#[test]
fn mult_s_has_two_strict_clock_syncs() {
    for prop in ["mult_p1", "mult_p2", "mult_s"] {
        let (clocks, syncs) = sync_shape(MC, &format!("assert property ({prop});"));
        assert_eq!(clocks, 3, "{prop}");
        assert_eq!(syncs, [(1, true), (2, true)], "{prop}");
    }
    // `##0` is the overlapping synchronisation.
    let (_, syncs) = sync_shape(
        MC,
        "assert property (@(posedge clk) a ##0 @(posedge clk1) b ##0 @(posedge clk2) c);",
    );
    assert_eq!(syncs, [(1, false), (2, false)]);
}

/// 16.13.1 `##0`: the second subsequence may start at the SAME step as the end of
/// the first, when the second clock ticks there too.
#[test]
fn cross_clock_zero_delay_may_overlap_and_one_delay_may_not() {
    let clocks = [("posedgeclk", "1100"), ("posedgeclk1", "0110")];
    let on_ticks = [("a", "1000"), ("b", "0100")];
    // clk1 ticks at 1 (and 2). `a ##0 @(clk1) b` starts at clk1's first tick at
    // or after 0, which is step 1; `##1` the first strictly after, also 1 here.
    let decls = "logic clk1;";
    let zero = "assert property (@(posedge clk) a ##0 @(posedge clk1) b);";
    let one = "assert property (@(posedge clk) a ##1 @(posedge clk1) b);";
    assert_eq!(
        mc(decls, zero, &on_ticks, &clocks, false),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        mc(decls, one, &on_ticks, &clocks, false),
        Verdict::HoldsStrongly
    );
    // Now clk1 also ticks at the end step 0: `##0` takes that tick, `##1` skips it.
    let clocks = [("posedgeclk", "1100"), ("posedgeclk1", "1110")];
    let at_zero = [("a", "1000"), ("b", "1000")];
    assert_eq!(
        mc(decls, zero, &at_zero, &clocks, false),
        Verdict::HoldsStrongly,
        "##0 reads b at the overlapping clk1 tick"
    );
    assert_eq!(
        mc(decls, one, &at_zero, &clocks, false),
        Verdict::Fails,
        "##1 skips the overlapping tick: b is read at step 1, where it is false"
    );
}

// -- 16.13.4 d, e: multiclock implication --------------------------------------

/// 16.13.4 (d): `@(posedge clk) a ##1 @(posedge clk1) s1 |=> @(posedge clk2) s2`.
/// The antecedent is the multiclocked `a ##1 @(clk1) s1`; the consequent starts at
/// the nearest tick of clk2 STRICTLY after the end of the antecedent (16.13.2) and
/// is `c ##1 d` on clk2.
#[test]
fn mult_p3_checks_the_consequent_on_the_next_clk2_tick_after_the_antecedent() {
    // The antecedent ends at step 3 (clk1's second tick).
    let ante = [("a", "1100000000"), ("b", "0001000000")];
    // clk2 ticks at 4, 6, 8: the consequent starts at 4.
    let clocks = [
        ("posedgeclk", "1000000000"),
        ("posedgeclk1", "0101010000"),
        ("posedgeclk2", "0000101010"),
    ];
    let with = |c: &str, d: &str| -> Vec<(&'static str, String)> {
        let mut v: Vec<(&'static str, String)> =
            ante.iter().map(|(n, r)| (*n, r.to_string())).collect();
        v.push(("c", c.to_string()));
        v.push(("d", d.to_string()));
        v
    };
    let run = |c: &str, d: &str, clocks: &[(&str, &str)]| {
        let owned = with(c, d);
        let sig: Vec<(&str, &str)> = owned.iter().map(|(n, r)| (*n, r.as_str())).collect();
        mca("mult_p3", &sig, clocks)
    };
    assert_eq!(
        run("0000100000", "0000001000", &clocks),
        Verdict::HoldsStrongly
    );
    assert_eq!(run("0000100000", "0000000010", &clocks), Verdict::Fails);
    assert_eq!(run("0000001000", "0000000010", &clocks), Verdict::Fails);
    // A vacuous attempt: the antecedent does not match (b missing).
    let sig = [
        ("a", "1100000000"),
        ("b", "0000000000"),
        ("c", "0000000000"),
        ("d", "0000000000"),
    ];
    assert!(passes(mca("mult_p3", &sig, &clocks)));
    // clk2 ALSO ticks at step 3, where the antecedent ends: `|=>` is strictly
    // later, so the consequent starts at 6 (c at 6, d at 8 holds; c at 3, d at 6,
    // which an overlapped implication would read, fails).
    let clocks = [
        ("posedgeclk", "1000000000"),
        ("posedgeclk1", "0101010000"),
        ("posedgeclk2", "0001001010"),
    ];
    assert_eq!(
        run("0000001000", "0000000010", &clocks),
        Verdict::HoldsStrongly
    );
    assert_eq!(run("0001000000", "0000001000", &clocks), Verdict::Fails);
}

/// 16.13.4 (e): `mult_s |=> mult_s`. The antecedent ends on clk2; the consequent
/// is `mult_s` again, so it starts on clk, at the first clk tick strictly after
/// the antecedent's end, and runs through clk1 and clk2 again.
#[test]
fn mult_p6_restarts_the_whole_chain_on_the_leading_clock() {
    // First pass: a@0 (clk), a@1 b@3 (clk1), c@4 d@6 (clk2): ends at 6.
    // Second pass starts at clk's first tick strictly after 6, which is 12.
    let clocks = [
        ("posedgeclk", "10000010000010000000"),
        ("posedgeclk1", "01010000000001010000"),
        ("posedgeclk2", "00001010000000101010"),
    ];
    // Second pass: a@12 (clk), a@13 b@15 (clk1), c@16 d@18 (clk2).
    let a = "11000000000011000000";
    let b = "00010000000000010000";
    let c = "00001000000000001000";
    let d = "00000010000000000010";
    let good = [("a", a), ("b", b), ("c", c), ("d", d)];
    assert_eq!(mca("mult_p6", &good, &clocks), Verdict::HoldsStrongly);
    // The consequent is checked from step 12, not from the end step 6 (clk ticks
    // at 6 as well: `|=>` skips it). Here the second chain is complete from a
    // at 6 -- a@6, a@13 b@15, c@16 d@18 -- and a is false at 12: a consequent
    // that started at 6 would hold, one that starts at 12 fails.
    let early = [
        ("a", "11000010000001000000"),
        ("b", "00010000000000010000"),
        ("c", "00001000000000001000"),
        ("d", "00000010000000000010"),
    ];
    assert_eq!(mca("mult_p6", &early, &clocks), Verdict::Fails);
    // A consequent that stops short of the end: the trace ends at step 12, a@12
    // holds, and no clk1 tick is left to carry `a ##1 b`. The second `mult_s` is a
    // weak bare sequence and nothing in it has failed, so the verdict is pending
    // (`Holds`), not a pass and not a failure. clk2 ticks at 11 as well, so the
    // `1` of F.3.4's `ante ##1 1` -- the next tick of the antecedent's end clock --
    // is a real sample and the antecedent is not vacuously false at the trace end.
    let short_clocks = [
        ("posedgeclk", "1000001000001"),
        ("posedgeclk1", "0101000000000"),
        ("posedgeclk2", "0000101000100"),
    ];
    let short = [
        ("a", "1100001000001"),
        ("b", "0001000000000"),
        ("c", "0000100000000"),
        ("d", "0000001000000"),
    ];
    assert_eq!(mca("mult_p6", &short, &short_clocks), Verdict::Holds);
    // The same trace with a false at 12: the consequent's first sample is wrong.
    let short_bad = [
        ("a", "1100001000000"),
        ("b", "0001000000000"),
        ("c", "0000100000000"),
        ("d", "0000001000000"),
    ];
    assert_eq!(mca("mult_p6", &short_bad, &short_clocks), Verdict::Fails);
}

// -- 16.13.4 f, g: clock flow ----------------------------------------------------

/// 16.13.4 (f): `@(posedge clk) a ##1 b |-> c ##1 @(posedge clk1) d`. `a`, `b`
/// and `c` are clocked at clk (clock flow, 16.13.3); `|->` starts the consequent
/// at the end of the antecedent; `##1 @(clk1) d` reads `d` at the first clk1 tick
/// strictly after `c`.
#[test]
fn mult_p7_flows_clk_through_the_overlapped_implication() {
    // clk ticks at 0, 2, 4; clk1 at 1, 3, 5. a@0, b@2: the antecedent ends at 2.
    let clocks = [("posedgeclk", "101010"), ("posedgeclk1", "010101")];
    let base = |d: &'static str| [("a", "100000"), ("b", "001000"), ("c", "001000"), ("d", d)];
    // d at 3, the first clk1 tick strictly after 2.
    assert_eq!(
        mca("mult_p7", &base("000100"), &clocks),
        Verdict::HoldsStrongly
    );
    // d only at 5, the second clk1 tick: not the one `##1` selects.
    assert_eq!(mca("mult_p7", &base("000001"), &clocks), Verdict::Fails);
    // d at 2 itself (a clk tick, not a clk1 tick).
    assert_eq!(mca("mult_p7", &base("001000"), &clocks), Verdict::Fails);
    // c false at the end of the antecedent.
    let no_c = [
        ("a", "100000"),
        ("b", "001000"),
        ("c", "000000"),
        ("d", "000100"),
    ];
    assert_eq!(mca("mult_p7", &no_c, &clocks), Verdict::Fails);
    // The antecedent does not match: vacuous.
    let no_b = [
        ("a", "100000"),
        ("b", "000000"),
        ("c", "001000"),
        ("d", "000000"),
    ];
    assert!(passes(mca("mult_p7", &no_b, &clocks)));
    // The structure: one sync into clk1, strict, inside the consequent.
    let (clocks_n, syncs) = sync_shape(MC, "assert property (mult_p7);");
    assert_eq!((clocks_n, syncs), (2, vec![(1, true)]));
}

/// 16.13.4 (g): clock flow through `if`/`else`. `c` selects, at the end of the
/// antecedent (a clk tick): `1 |=> @(clk1) d` reads `d` at the first clk1 tick
/// strictly after it, `e ##1 @(clk2) f` reads `e` there and `f` at the first clk2
/// tick strictly after it.
#[test]
fn mult_p8_selects_between_two_clock_flows() {
    // clk ticks at 0, 2; clk1 at 3, 5; clk2 at 4, 6. a@0, b@2: ends at 2.
    let clocks = [
        ("posedgeclk", "1010000"),
        ("posedgeclk1", "0001010"),
        ("posedgeclk2", "0000101"),
    ];
    let run = |c: &'static str, d: &'static str, e: &'static str, f: &'static str| {
        mca(
            "mult_p8",
            &[
                ("a", "1000000"),
                ("b", "0010000"),
                ("c", c),
                ("d", d),
                ("e", e),
                ("f", f),
            ],
            &clocks,
        )
    };
    // c at 2: the then branch. d at clk1's first tick after 2 (step 3).
    assert_eq!(
        run("0010000", "0001000", "0000000", "0000000"),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        run("0010000", "0000010", "0000000", "0000000"),
        Verdict::Fails,
        "d at clk1's SECOND tick is not read"
    );
    // The else branch is not checked when c is true: e/f hold nothing.
    assert_eq!(
        run("0010000", "0001000", "0000000", "0000000"),
        Verdict::HoldsStrongly
    );
    // c false at 2: the else branch. e at 2, f at clk2's first tick after 2 (4).
    assert_eq!(
        run("0000000", "0000000", "0010000", "0000100"),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        run("0000000", "0000000", "0010000", "0000001"),
        Verdict::Fails,
        "f at clk2's second tick is not read"
    );
    assert_eq!(
        run("0000000", "0001000", "0000000", "0000100"),
        Verdict::Fails,
        "e false at the end of the antecedent"
    );
    // The then branch's d is not what the else branch reads.
    assert_eq!(
        run("0000000", "0001000", "0010000", "0000000"),
        Verdict::Fails
    );
    // Both flows are in one automaton: clk1 and clk2, one sync into clk2.
    let (n, syncs) = sync_shape(MC, "assert property (mult_p8);");
    assert_eq!((n, syncs), (3, vec![(2, true)]));
}

// -- 16.13.7: local variables with several semantic leading clocks --------------

/// The LRM's own `p`/`a1`.
const P_A1: &str = "logic clk1, clk2, f;\n\
    property p;\n\
       logic v = e;\n\
       (@(posedge clk1) (a == v)[*1:$] |-> b)\n\
       and\n\
       (@(posedge clk2) c[*1:$] |-> d == v)\n\
       ;\n\
    endproperty\n";
const A1: &str = "assert property (@(posedge clk) f |=> p);";

/// 16.13.7: the instance of `p` in `a1` has two semantic leading clocks, so `v`
/// is two variables. One is set from `e` at clk1's first tick after the antecedent
/// (t1) and used in `(a == v)[*1:$] |-> b`; the other is set from `e` at clk2's
/// first tick after it (t2) and used in `c[*1:$] |-> d == v`. The two copies hold
/// DIFFERENT values here (e is 1 at t1 and 0 at t2), so a single shared `v` fails.
#[test]
fn each_semantic_leading_clock_gets_its_own_copy_of_the_local_variable() {
    // clk ticks at 0 (f true); clk1 at 1, 3; clk2 at 2, 4. t1 = 1, t2 = 2.
    let clocks = [
        ("posedgeclk", "10000"),
        ("posedgeclk1", "01010"),
        ("posedgeclk2", "00101"),
    ];
    // e = 1 at t1, e = 0 at t2: v(clk1) = 1, v(clk2) = 0.
    // Subproperty 1: a == 1 at step 1 (the antecedent matches there only, since a
    // is 0 at step 3), so b must hold at 1. Subproperty 2: c at step 2, so d == 0
    // must hold at 2.
    let sig = |a: &'static str, b: &'static str, c: &'static str, d: &'static str| {
        [
            ("f", "10000"),
            ("e", "01000"),
            ("a", a),
            ("b", b),
            ("c", c),
            ("d", d),
        ]
        .map(|(n, r)| (n, r))
        .to_vec()
    };
    let run = |s: Vec<(&str, &str)>| mc(P_A1, A1, &s, &clocks, false);
    // Both subproperties hold.
    assert_eq!(
        run(sig("01000", "01000", "00100", "00000")),
        Verdict::HoldsStrongly
    );
    // Copy 2 broken alone: d == v(clk2) = 0 fails when d is 1 at step 2.
    assert_eq!(run(sig("01000", "01000", "00100", "00100")), Verdict::Fails);
    // Copy 1 broken alone: a == v(clk1) matches at step 1, b is false there.
    assert_eq!(run(sig("01000", "00000", "00100", "00000")), Verdict::Fails);
    // Copy 1 not matching (a is 0, v(clk1) = 1): the first subproperty is
    // vacuous, and copy 2 is still checked.
    assert!(passes(run(sig("00000", "00000", "00100", "00000"))));
    assert_eq!(run(sig("00000", "00000", "00100", "00100")), Verdict::Fails);
    // A single shared copy would use e at t1 (1) for `d == v` too: d = 0 would
    // fail. Pinned by the first case above; here the same trace with d = 1, which
    // a shared copy would ACCEPT, fails because copy 2 is e at t2 = 0.
    assert_eq!(run(sig("01000", "01000", "00100", "01100")), Verdict::Fails);
}

/// 16.13.7: each copy is assigned at the earliest tick of ITS clock at or after the
/// beginning of the evaluation attempt, which for `|=>` is strictly after t0 --
/// even when that clock ticks at t0 as well.
#[test]
fn the_declaration_assignment_happens_after_the_antecedent_not_at_it() {
    // Both clk1 and clk2 tick at step 0 (= t0) too. e is 0 at 0 and 1 at 1 and 2.
    // The attempt of p starts strictly after t0: v(clk1) = e at 1 = 1,
    // v(clk2) = e at 2 = 1.
    let clocks = [
        ("posedgeclk", "1000000"),
        ("posedgeclk1", "1101010"),
        ("posedgeclk2", "1010101"),
    ];
    let good = [
        ("f", "1000000"),
        ("e", "0110000"),
        ("a", "0100000"), // a == v(clk1) = 1 at step 1; 0 at step 3 ends it
        ("b", "0100000"),
        ("c", "0010000"),
        ("d", "0010000"), // d == v(clk2) = 1 at step 2
    ];
    assert_eq!(mc(P_A1, A1, &good, &clocks, false), Verdict::HoldsStrongly);
    // Had `v` been assigned at t0 (e = 0), a would have to be 0 to match and b
    // would not be checked; here a matches v = 1 and b is false: it fails.
    let bad_b = [
        ("f", "1000000"),
        ("e", "0110000"),
        ("a", "0100000"),
        ("b", "0000000"),
        ("c", "0010000"),
        ("d", "0010000"),
    ];
    assert_eq!(mc(P_A1, A1, &bad_b, &clocks, false), Verdict::Fails);
    // Likewise for the second copy: d == 0 would pass at t0, d == 1 is required.
    let bad_d = [
        ("f", "1000000"),
        ("e", "0110000"),
        ("a", "0100000"),
        ("b", "0100000"),
        ("c", "0010000"),
        ("d", "0000000"),
    ];
    assert_eq!(mc(P_A1, A1, &bad_d, &clocks, false), Verdict::Fails);
}

/// The two copies are built as two `Let` nodes, one under each leading clock, and
/// a property with ONE leading clock keeps its single `Let` where it was.
#[test]
fn the_local_variable_is_pushed_below_each_leading_clock() {
    // (number of variable-initialising nodes, how many of them are the direct
    // body of a clock node).
    let counts = |decls: &str, stmt: &str| {
        with_property(decls, stmt, false, |r, _| {
            let (ir, _) = r.unwrap_or_else(|e| panic!("`{stmt}` failed to build: {e}"));
            let lets = ir
                .props
                .iter()
                .filter(|p| matches!(p, Prop::Let { .. }))
                .count();
            let under_clock = ir
                .props
                .iter()
                .filter(|p| match p {
                    Prop::Clocked { p, .. } => matches!(ir.prop(*p), Prop::Let { .. }),
                    _ => false,
                })
                .count();
            (lets, under_clock)
        })
    };
    // Two leading clocks: two copies, each directly below its clock.
    assert_eq!(counts(P_A1, A1), (2, 2));
    // One leading clock: one `Let`, where single-clock properties always had it
    // (above the clock node, if there is one).
    let one = "logic clk1, f;\n\
        property q; logic v = e; (@(posedge clk1) (a == v)[*1:$] |-> b); endproperty\n";
    assert_eq!(
        counts(one, "assert property (@(posedge clk) f |=> q);"),
        (1, 0)
    );
}

// -- 16.16.1: semantic leading clocks and legality --------------------------------

const EQ_CLOCKS: &str = "module m;\n\
    wire clk1, clk2;\n\
    logic a, b;\n\
    assign clk2 = clk1;\n\
    a1: assert property (@(clk1) a and @(clk2) b);\n\
    a2: assert property (@(clk1) a and @(clk1) b);\n\
    always @(posedge clk1) begin\n\
       a3: assert property(a and @(posedge clk2) b);\n\
       a4: assert property(a and @(posedge clk1) b);\n\
    end\n\
    endmodule\n";

/// 16.16.1: clocks that have the same VALUE but are not IDENTICAL do not give a
/// unique semantic leading clock. a1 is illegal (clk1 vs clk2, driven by the same
/// net), a2 legal (the same expression twice); a3 is illegal because its inferred
/// clock `@(posedge clk1)` is not identical to `@(posedge clk2)`, a4 legal.
///
/// The LRM prints a3 and a4 as `a and @(posedge clk2)` with no operand after the
/// event, which is not a sequence expression; the intended `a and @(posedge clk2) b`
/// is tested.
///
/// slang implements the rule: an illegal assertion is dropped from the analysis
/// and `NoUniqueClock` is the only trace of it (see `sv_sim_sim::sva::clock`, whose
/// documented a3 gap is a different shape: a default clocking). This test pins what
/// the frontend does today and what this crate does with each survivor: a2 and a4
/// are built, and their two clocks are ONE clock.
#[test]
fn the_same_value_clocks_of_16_16_1_a1_to_a4() {
    let session = Session::new();
    let mut comp = Compilation::new(&session).unwrap();
    comp.add_source(EQ_CLOCKS).unwrap();
    let design = comp.compile().unwrap();
    let m = design
        .top_instances()
        .next()
        .unwrap()
        .instance_body()
        .unwrap();
    let analysis = design.analyze(AnalysisFlags::NONE, 1).unwrap();
    let tree = design.syntax_trees().into_iter().next().unwrap();
    let diags = analysis.diagnostics();
    // a1 and a3 are illegal: exactly two NoUniqueClock errors are reported by the
    // analysis, and neither assertion is among the analysed ones.
    let no_unique = diags
        .items()
        .iter()
        .filter(|d| d.is_error() && d.code_name() == "NoUniqueClock")
        .count();
    assert_eq!(
        no_unique,
        2,
        "a1 and a3 are the illegal assertions slang reports:\n{}",
        diags.rendered()
    );
    let mut built_labels = Vec::new();
    for proc in analysis.procedures(m) {
        for assertion in analysis.assertions(proc.symbol()) {
            let stmt_text = assertion
                .ast_node()
                .as_statement()
                .and_then(|s| s.syntax(&tree))
                .map(|n| n.text().split_whitespace().collect::<String>())
                .unwrap_or_default();
            let root = assertion.root().as_assertion_expr().unwrap();
            // A procedural assertion's inferred clock (`@$inferred_clock`, or none
            // written at all) is the enclosing block's own event, as the emitter
            // resolves it.
            let proc_event = || {
                let mut stack: Vec<_> = sv_sim_sim::process::cfg::proc_body(&proc.symbol())
                    .map(|b| b.as_sem_node())
                    .into_iter()
                    .collect();
                while let Some(n) = stack.pop() {
                    if n.as_timing_control().is_some() {
                        return Some(n);
                    }
                    stack.extend(n.children());
                }
                None
            };
            let (root, root_clock) = if root.kind() == AssertionExprKind::Clocking {
                let kids = root.children();
                let clock = if crate::sva::build::is_inferred_clock_event(kids[0]) {
                    proc_event().unwrap_or(kids[0])
                } else {
                    kids[0]
                };
                (kids[1].as_assertion_expr().unwrap(), Some(clock))
            } else {
                (root, proc_event())
            };
            let (_, leaves) = build_property(root, root_clock, (&tree).into(), &m)
                .unwrap_or_else(|e| panic!("`{stmt_text}` failed to build: {e}"));
            built_labels.push((stmt_text, leaves.clock_count()));
        }
    }
    let count_of = |label: &str| {
        built_labels
            .iter()
            .find(|(t, _)| t.contains(label))
            .unwrap_or_else(|| {
                panic!(
                    "{label} was not analysed: {built_labels:?}\n{}",
                    diags.rendered()
                )
            })
            .1
    };
    assert_eq!(count_of("a2:"), 1, "a2: identical clocks are one clock");
    assert_eq!(count_of("a4:"), 1, "a4: identical clocks are one clock");
    assert!(
        built_labels
            .iter()
            .all(|(t, _)| !t.contains("a1:") && !t.contains("a3:")),
        "a1 and a3 are illegal and are not built: {built_labels:?}"
    );
}

// -- what a clock change cannot take ---------------------------------------------

/// The diagnostics (compile and analysis) slang reports for `decls` + `stmt`.
fn slang_diagnostics(decls: &str, stmt: &str) -> String {
    let src = format!(
        "module m;\n\
         logic clk, a, b, c, d, e;\n\
         {decls}\n\
         always_ff @(posedge clk) begin\n\
           {stmt}\n\
         end\n\
         endmodule\n"
    );
    let session = Session::new();
    let mut comp = Compilation::new(&session).unwrap();
    comp.add_source(&src).unwrap();
    let design = comp.compile().unwrap();
    let analysis = design.analyze(AnalysisFlags::NONE, 1).unwrap();
    format!(
        "{}{}",
        design.diagnostics().rendered(),
        analysis.diagnostics().rendered()
    )
}

/// What slang accepts but one automaton with one clock per thread cannot say:
/// `(u ##1 v)[*2]` (slang accepts it; the sequence is multiclocked) and
/// `first_match` of one. Repeating or selecting among matches of a sequence whose
/// matches end on another clock than they start on needs a tick count per clock
/// that 16.9.2 does not define, so the builder says so by name instead of building
/// an automaton that counts the wrong ticks.
#[test]
fn repeating_a_multiclocked_sequence_is_refused_by_name() {
    let decls = "logic clk1;\n\
        sequence u; @(posedge clk) a ##1 b; endsequence\n\
        sequence v; @(posedge clk1) c ##1 d; endsequence\n";
    for stmt in [
        "assert property ((u ##1 v)[*2]);",
        "assert property ((u ##1 v)[*1:2]);",
        "assert property (first_match(u ##1 v));",
    ] {
        let msg = refused(decls, stmt);
        assert!(
            msg.contains("multiclocked sequence"),
            "`{stmt}` was refused for another reason: {msg}"
        );
    }
}

/// 16.13.1: only `##1` and `##0` join two clocks, and a maximal singly clocked
/// subsequence admits no empty match. slang enforces both (and the rule that the
/// other sequence operators take singly clocked operands) before this crate sees
/// the assertion: the assertion is dropped from the analysis, so the builder's own
/// refusals of the same shapes (`concat_clocked`, `join_clocks`, `single_clock`)
/// are defence in depth that no frontend-accepted design can reach. This test pins
/// that the frontend does refuse each, so a slang upgrade that stops doing so
/// shows up here rather than as a silently built automaton.
#[test]
fn slang_refuses_what_a_clock_change_cannot_take() {
    let decls = "logic clk1;\n\
        sequence u; @(posedge clk) a ##1 b; endsequence\n\
        sequence v; @(posedge clk1) c ##1 d; endsequence\n";
    for stmt in [
        "assert property (u ##2 v);",
        "assert property (u ##[1:2] v);",
        "assert property (u and v);",
        "assert property (u or v);",
        "assert property (u intersect v);",
        "assert property (u within v);",
        "assert property (a throughout v);",
        "assert property (@(posedge clk) a[*0:1] ##1 v);",
        "assert property (@(posedge clk) a ##1 v[*0:1]);",
    ] {
        let msg = slang_diagnostics(decls, stmt);
        assert!(msg.contains("error"), "slang accepted `{stmt}`");
    }
    // The same operators on operands of ONE clock are fine.
    for stmt in [
        "assert property (u and u);",
        "assert property (u intersect u);",
        "assert property (first_match(u ##1 u));",
        "assert property (u[*2]);",
    ] {
        let msg = slang_diagnostics(decls, stmt);
        assert!(!msg.contains("error"), "`{stmt}`: {msg}");
    }
}