vj-codegen 0.1.0

//! sva T27: `disable iff` (LRM 16.12, 16.15).
//!
//! Three things are pinned: what the builder accepts and rejects (the clause is
//! legal only as the whole property spec, and its condition is a plain Boolean), what
//! an attempt does when the condition is true during it (`Evaluator::attempt`), and
//! which condition an assertion ends up with when it has no clause (16.15's rules
//! a-c, on the LRM's own example modules).
use sv_sim_sim::sva::property::Disposition;

use super::*;
use crate::sva::disable::{DisableSource, resolve_disable};
use sv_lang::SyntaxTree;

// -- builder ---------------------------------------------------------------------

/// What the leaf's condition is, for the Boolean conditions these fixtures use: the
/// name of the signal it reads (so an actual substituted for a formal is the actual,
/// not the formal's spelling), or its source text when it is not a plain name.
fn leaf_text(leaves: &LeafTable<'_>, leaf: LeafId, tree: &SyntaxTree) -> String {
    let e = leaves.get(leaf);
    if let Some(sym) = e.referenced_symbol() {
        return sym.name().to_string();
    }
    e.syntax(tree)
        .expect("a leaf has a syntax node")
        .text()
        .trim()
        .to_string()
}

/// The condition of the `disable iff` the builder recorded for the whole of `prop`
/// (`None`: the property has none).
fn disable_of(decls: &str, prop: &str) -> Option<String> {
    with_property(decls, &ap(prop), false, |r, tree| {
        let (ir, leaves) = r.unwrap_or_else(|e| panic!("`{prop}` failed to build: {e}"));
        ir.disable.map(|d| leaf_text(&leaves, d, tree))
    })
}

/// 16.12: `disable iff (cond) p` as the property spec records `cond` and builds `p`
/// alone -- the clause is not a property operator.
#[test]
fn explicit_clause_is_recorded_and_the_body_is_built_alone() {
    assert_eq!(
        disable_of("", "disable iff (reset) a |=> b").as_deref(),
        Some("reset")
    );
    assert_eq!(disable_of("", "a |=> b"), None);
    // The body is exactly the property without the clause: same verdict on every
    // trace, from every start, under both readings of a bare sequence.
    for body in [
        "a |=> b",
        "a ##1 b",
        "not (a ##1 b)",
        "always (a |-> ##1 b)",
    ] {
        let with = all_verdicts(
            "",
            &format!("disable iff (reset) {body}"),
            &["a", "b", "reset"],
            3,
        );
        // `reset` is a leaf of the clause only: `Evaluator::verdict` is the body.
        let without = all_verdicts("", body, &["a", "b", "reset"], 3);
        assert_eq!(with, without, "`disable iff (reset) {body}`");
    }
}

/// 16.12: the clause may be written in the property a spec instantiates, with the
/// property's formals substituted into the condition.
#[test]
fn clause_in_an_instantiated_property_is_the_specs_clause() {
    let decls = "property p; disable iff (reset) a |=> b; endproperty
                 property q(rst); disable iff (rst) a |=> b; endproperty
                 property w(rst); q(rst); endproperty";
    assert_eq!(disable_of(decls, "p").as_deref(), Some("reset"));
    assert_eq!(disable_of(decls, "q(reset)").as_deref(), Some("reset"));
    assert_eq!(disable_of(decls, "q(x)").as_deref(), Some("x"));
    // An instance that is only the whole body of another declaration is still the
    // whole spec.
    assert_eq!(disable_of(decls, "w(y)").as_deref(), Some("y"));
}

/// 16.12: `disable iff` "cannot be nested": not under another `disable iff`, nor in
/// a property that is an operand of anything.
///
/// slang enforces every one of these forms before the builder sees the design (the
/// parser refuses the clause under a clause or inside an operand; the instance of a
/// property with a clause is refused "here"), so the assertion never reaches
/// `build_property`: what is pinned is that slang's diagnostic is what stops it -- an
/// upgrade that let one through would meet the builder's own rejection of a non-top
/// clause instead of silently ignoring it.
#[test]
fn nested_disable_iff_is_rejected() {
    let decls = "logic y; property inner; disable iff (y) a |=> b; endproperty";
    for (prop, what) in [
        ("disable iff (b) inner", "under a clause"),
        ("not inner", "operand of not"),
        ("inner and a", "operand of and"),
        ("a |-> inner", "consequent"),
        ("always inner", "operand of always"),
        ("if (a) inner", "branch of if"),
        ("reject_on (b) inner", "body of an abort"),
        (
            "disable iff (a) disable iff (b) a |=> b",
            "clause under a clause",
        ),
        ("(disable iff (b) a) or b", "clause in an operand"),
    ] {
        let msg = slang_errors(decls, prop);
        assert!(
            msg.contains("error"),
            "{what} (`{prop}`) was not refused by slang: {msg}"
        );
    }
    // An instance that IS the whole spec is the legal form.
    builds(
        "property inner; disable iff (y) a |=> b; endproperty",
        "inner",
    );
}

/// 16.15: the condition "shall not contain any reference to local variables or the
/// sequence method `matched`". slang diagnoses both (so, as above, the builder's own
/// check is for a tree slang let through).
#[test]
fn condition_may_not_read_a_local_variable_or_matched() {
    let msg = slang_errors(
        "property pl; int v; disable iff (v == 1) (a, v = 1) ##1 b; endproperty",
        "pl",
    );
    assert!(
        msg.contains("local variables cannot be used in disable iff conditions"),
        "{msg}"
    );
    let msg = slang_errors(
        "sequence s; a ##1 b; endsequence",
        "disable iff (s.matched) a |=> b",
    );
    assert!(
        msg.contains("'matched' method cannot be used in disable iff conditions"),
        "{msg}"
    );
}

// -- evaluator -------------------------------------------------------------------

/// What an attempt of `prop` (under `disable iff (reset)`) at `start` comes to on
/// `signals`, with the condition's values strictly between ticks in `between`
/// (index `t`: between tick `t` and `t + 1`).
fn attempt(
    prop: &str,
    signals: &[(&str, &str)],
    between_reset: Option<&str>,
    start: u32,
    strong: bool,
) -> Disposition {
    let table = rows(signals);
    let len = table.values().next().expect("a signal").len() as u32;
    with_property(
        "",
        &ap(&format!("disable iff (reset) {prop}")),
        false,
        |r, _| {
            let (ir, leaves) = r.unwrap_or_else(|e| panic!("`{prop}` failed to build: {e}"));
            let mut env = Sigs::new(&leaves, &table);
            if let Some(b) = between_reset {
                env.between = rows(&[("reset", b)]);
            }
            Evaluator::new(&ir, &env, strong)
                .attempt(len, start)
                .unwrap_or_else(|e| panic!("`{prop}` failed to evaluate: {e}"))
        },
    )
}

/// 16.12: "an attempt is disabled if the condition is true at any time from the
/// start of the attempt to its end, inclusive": a failure the disabling pre-empts
/// is no failure.
#[test]
fn condition_true_during_the_attempt_disables_it() {
    // Strong, so that an attempt that has not seen its `b` yet is undecided (a weak
    // sequence has nothing owed on a `⊤` tail and passes).
    let p = "strong(a ##1 b)";
    let sigs = |reset| [("a", "10"), ("b", "00"), ("reset", reset)];
    // Never true: the failure at tick 1 stands.
    assert_eq!(attempt(p, &sigs("00"), None, 0, false), Disposition::Fails);
    // True at the tick the failure would be reported at (tick 1): disabled.
    assert_eq!(
        attempt(p, &sigs("01"), None, 0, false),
        Disposition::Disabled
    );
    // True when the attempt starts: disabled, however the rest goes.
    assert_eq!(
        attempt(p, &sigs("10"), None, 0, false),
        Disposition::Disabled
    );
    // The attempt that starts at tick 1 never sees tick 0 (and fails: `a` is 0 there).
    assert_eq!(attempt(p, &sigs("10"), None, 1, false), Disposition::Fails);
    // Under `|=>` the same shape: disabled before the consequent's tick.
    let p = "a |-> strong(1 ##1 b)";
    assert_eq!(
        attempt(p, &sigs("01"), None, 0, false),
        Disposition::Disabled
    );
}

/// Annex F.5.3.2 is literal about a prefix whose antecedent needs a letter that has
/// not come yet: `a |=> b` on `[a]` is satisfied by `w ⊥^ω` (the antecedent's
/// `##1 1` is not matched by a `⊥` letter), so the attempt "passes" under a
/// disabling at tick 1, where `a |-> strong(1 ##1 b)` (a consequent that is not
/// vacuous on the tail) is disabled. The simulation engine does not take a pass from a verdict that
/// depended on a letter it has not seen (T29); this evaluator is the Annex F
/// classification itself.
#[test]
fn a_prefix_that_is_vacuous_on_the_tail_passes_under_annex_f() {
    let sigs = [("a", "10"), ("b", "00"), ("reset", "01")];
    assert_eq!(
        attempt("a |=> b", &sigs, None, 0, false),
        Disposition::Passes
    );
    assert_eq!(
        attempt("a |-> strong(1 ##1 b)", &sigs, None, 0, false),
        Disposition::Disabled
    );
}

/// 16.12.1: the condition is evaluated with CURRENT values at every time step, not
/// sampled at ticks: a pulse strictly between two ticks disables the attempt.
#[test]
fn condition_pulse_between_ticks_disables_it() {
    let p = "strong(a ##1 b)";
    let sigs = [("a", "10"), ("b", "00"), ("reset", "00")];
    // Between tick 0 and tick 1: before the failing evaluation, so disabled.
    assert_eq!(
        attempt(p, &sigs, Some("10"), 0, false),
        Disposition::Disabled
    );
    // Between tick 1 and tick 2 (the trace ends at tick 1, so the pulse is after the
    // last letter): the failure was decided before it and stands.
    assert_eq!(attempt(p, &sigs, Some("01"), 0, false), Disposition::Fails);
}

/// F.5.? (neutral satisfaction under a top-level `disable iff`): what was decided on
/// the letters before the disabling is not undone by it.
#[test]
fn decided_attempts_are_unaffected_by_a_later_disabling() {
    // Passes at tick 0 (`a` and `b` at the same tick), then reset: still a pass.
    assert_eq!(
        attempt(
            "a |-> b",
            &[("a", "11"), ("b", "11"), ("reset", "01")],
            None,
            0,
            false
        ),
        Disposition::Passes
    );
    // Fails at tick 1 (`a ##1 b` with b false), reset only at tick 2.
    assert_eq!(
        attempt(
            "strong(a ##1 b)",
            &[("a", "100"), ("b", "000"), ("reset", "001")],
            None,
            0,
            false
        ),
        Disposition::Fails
    );
    // A pending attempt that is disabled is disabled, not passed, and not failed.
    assert_eq!(
        attempt(
            "strong(a ##1 b)",
            &[("a", "10"), ("b", "00"), ("reset", "01")],
            None,
            0,
            false
        ),
        Disposition::Disabled
    );
    // ... and one nobody disables is still pending after its last letter.
    assert_eq!(
        attempt(
            "strong(a ##3 b)",
            &[("a", "10"), ("b", "00"), ("reset", "00")],
            None,
            0,
            false
        ),
        Disposition::Pending
    );
}

/// The three exhaustive properties the definition gives, over every trace of
/// `a`, `b`, `reset` up to four ticks, from every start, under both readings of a
/// bare sequence:
///
/// * a condition that is never true leaves the verdict alone;
/// * a condition true at the start disables;
/// * with the first moment `t > start` it is true at, the result is the verdict on
///   the `t` letters before it (an undecided one is "disabled"), computed here on a
///   trace actually truncated to `t` ticks rather than by the evaluator's own cut.
#[test]
fn attempt_is_the_verdict_on_the_letters_before_the_first_disabling() {
    for prop in [
        "a |=> b",
        "a ##1 b",
        "not (a ##1 b)",
        "a |-> s_eventually b",
        "always (a |-> ##1 b)",
        "(a ##[1:2] b) or c",
    ] {
        let spec = format!("disable iff (reset) {prop}");
        with_property("", &ap(&spec), false, |r, _| {
            let (ir, leaves) = r.unwrap_or_else(|e| panic!("`{prop}` failed to build: {e}"));
            for len in 1..=4usize {
                for table in all_traces(&["a", "b", "c", "reset"], len) {
                    let env = Sigs::new(&leaves, &table);
                    for strong in [false, true] {
                        let ev = Evaluator::new(&ir, &env, strong);
                        for start in 0..len as u32 {
                            let got = ev.attempt(len as u32, start).unwrap();
                            let first = (start as usize..len).find(|&t| table["reset"][t] != 0);
                            let want = match first {
                                None => ev.verdict(len as u32, start).unwrap().into(),
                                Some(t) if t == start as usize => Disposition::Disabled,
                                Some(t) => {
                                    let cut: Rows = table
                                        .iter()
                                        .map(|(n, v)| (n.clone(), v[..t].to_vec()))
                                        .collect();
                                    let env = Sigs::new(&leaves, &cut);
                                    match Evaluator::new(&ir, &env, strong)
                                        .verdict(t as u32, start)
                                        .unwrap()
                                    {
                                        Verdict::Holds => Disposition::Disabled,
                                        decided => decided.into(),
                                    }
                                }
                            };
                            assert_eq!(
                                got, want,
                                "`{spec}` len {len} start {start} strong {strong}: {table:?}"
                            );
                        }
                    }
                }
            }
        });
    }
}

// -- 16.15 resolution ------------------------------------------------------------

/// Which rule gave each concurrent assertion of the design `src` its condition,
/// and the text of the condition, keyed by the assertion's label; every instance
/// body of the design (the top module and the modules instantiated in it) is
/// searched.
fn resolved(src: &str) -> BTreeMap<String, String> {
    let session = Session::new();
    let mut comp = Compilation::new(&session).unwrap();
    comp.add_source(src).unwrap();
    let design = comp.compile().unwrap();
    let diags = design.diagnostics();
    assert!(
        !diags.has_errors(),
        "fixture has compile errors:\n{}\n{src}",
        diags.rendered()
    );
    let analysis = design.analyze(AnalysisFlags::NONE, 1).unwrap();
    let tree = design.syntax_trees().into_iter().next().unwrap();
    let mut bodies = vec![
        design
            .top_instances()
            .next()
            .unwrap()
            .instance_body()
            .unwrap(),
    ];
    let mut out = BTreeMap::new();
    while let Some(body) = bodies.pop() {
        bodies.extend(
            body.members()
                .filter(|m| m.kind() == sv_lang::kinds::SymbolKind::Instance)
                .filter_map(|m| m.instance_body()),
        );
        for proc in analysis.procedures(body) {
            for assertion in analysis.assertions(proc.symbol()) {
                let label = proc
                    .symbol()
                    .syntax(&tree)
                    .and_then(|n| n.first_token())
                    .map(|t| t.text().to_string())
                    .expect("an assertion statement starts with its label");
                let root = assertion.root().as_assertion_expr().unwrap();
                let (root, root_clock) = if root.kind() == AssertionExprKind::Clocking {
                    let kids = root.children();
                    (kids[1].as_assertion_expr().unwrap(), Some(kids[0]))
                } else {
                    (root, None)
                };
                let (ir, leaves) = build_property(root, root_clock, (&tree).into(), &body)
                    .unwrap_or_else(|e| panic!("{label}: {e}"));
                let how = match resolve_disable(ir.disable, &body, &tree)
                    .unwrap_or_else(|e| panic!("{label}: {e}"))
                {
                    DisableSource::Explicit(l) => {
                        format!("explicit {}", leaf_text(&leaves, l, &tree))
                    }
                    DisableSource::Default { scope, decl } => format!(
                        "default {} (declared in {})",
                        decl.expr().syntax().text().trim(),
                        scope.name()
                    ),
                    DisableSource::None => "none".to_string(),
                };
                assert!(
                    out.insert(label.clone(), how).is_none(),
                    "two assertions labelled `{label}`"
                );
            }
        }
    }
    out
}

/// The `examples_with_default` module of 16.15, verbatim (the assertion
/// statements, the property, and the inline comments each assertion's
/// expectation comes from).
const EXAMPLES_WITH_DEFAULT: &str = "
module examples_with_default (input logic a, b, clk, rst, rst1);
   default disable iff rst;
   property p1;
      disable iff (rst1) a |=> b;
   endproperty

   // Disable condition is rst1 - explicitly specified within a1
   a1 : assert property (@(posedge clk) disable iff (rst1) a |=> b);

   // Disable condition is rst1 - explicitly specified within p1
   a2 : assert property (@(posedge clk) p1);

   // Disable condition is rst - no explicit specification, inferred from
   // default disable iff declaration
   a3 : assert property (@(posedge clk) a |=> b);

   // Disable condition is 1'b0. This is the only way to
   // cancel the effect of default disable.
   a4 : assert property (@(posedge clk) disable iff (1'b0) a |=> b);
endmodule
";

/// The `examples_without_default` module of 16.15, verbatim.
const EXAMPLES_WITHOUT_DEFAULT: &str = "
module examples_without_default (input logic a, b, clk, rst);
   property p2;
      disable iff (rst) a |=> b;
   endproperty

   // Disable condition is rst - explicitly specified within a5
   a5 : assert property (@(posedge clk) disable iff (rst) a |=> b);

   // Disable condition is rst - explicitly specified within p2
   a6 : assert property (@ (posedge clk) p2);

   // No disable condition
   a7 : assert property (@ (posedge clk) a |=> b);
endmodule
";

/// 16.15 rules (a)-(c), on `examples_with_default`: an explicit clause (written in
/// the assertion or in its property) wins over the default, the default applies to an
/// assertion with none, and `disable iff (1'b0)` is the way to cancel it.
#[test]
fn examples_with_default() {
    let r = resolved(EXAMPLES_WITH_DEFAULT);
    assert_eq!(r.len(), 4, "{r:?}");
    // a1: "Disable condition is rst1 - explicitly specified within a1".
    assert_eq!(r["a1"], "explicit rst1");
    // a2: "Disable condition is rst1 - explicitly specified within p1".
    assert_eq!(r["a2"], "explicit rst1");
    // a3: "Disable condition is rst - no explicit specification, inferred from
    // default disable iff declaration".
    assert_eq!(r["a3"], "default rst (declared in examples_with_default)");
    // a4: "Disable condition is 1'b0. This is the only way to cancel the effect of
    // default disable."
    assert_eq!(r["a4"], "explicit 1'b0");
}

/// 16.15 rule (c) and rule (a) without any default: "No disable condition" for a7.
#[test]
fn examples_without_default() {
    let r = resolved(EXAMPLES_WITHOUT_DEFAULT);
    assert_eq!(r.len(), 3, "{r:?}");
    // a5, a6: "Disable condition is rst - explicitly specified within a5 / p2".
    assert_eq!(r["a5"], "explicit rst");
    assert_eq!(r["a6"], "explicit rst");
    // a7: "No disable condition".
    assert_eq!(r["a7"], "none");
}

/// 16.15's first `m1`/`m2` example: no default in the nested `m2`, so "the inferred
/// disable condition of both assertions a1 and a2 is rst1" -- the default is
/// declared in `m1`, and that is the scope its names resolve in.
#[test]
fn nested_module_inherits_the_default() {
    let r = resolved(
        "module m1;
            bit clk, rst1, a, b;
            default disable iff rst1;
            a1: assert property (@(posedge clk) a |=> b);
            m2 u2();
            module m2;
               bit rst2;
               a2: assert property (@(posedge clk) a |=> b);
            endmodule
         endmodule",
    );
    assert_eq!(r["a1"], "default rst1 (declared in m1)");
    assert_eq!(r["a2"], "default rst1 (declared in m1)");
}

/// 16.15's second `m1`/`m2` example: "within m2 this default disable condition
/// overrides the default disable condition declared in m1. Therefore ... the
/// inferred disable condition of a1 is rst1, but the inferred disable condition of
/// a2 is rst2."
#[test]
fn nested_module_default_overrides() {
    let r = resolved(
        "module m1;
            bit clk, rst1, a, b;
            default disable iff rst1;
            a1: assert property (@(posedge clk) a |=> b);
            m2 u2();
            module m2;
               bit rst2;
               default disable iff rst2;
               a2: assert property (@(posedge clk) a |=> b);
            endmodule
         endmodule",
    );
    assert_eq!(r["a1"], "default rst1 (declared in m1)");
    assert_eq!(r["a2"], "default rst2 (declared in m2)");
}

/// 16.15: "The scope does not extend into any instances of modules": a module
/// merely instantiated in the one with the default does not get it.
#[test]
fn default_does_not_extend_into_instances() {
    let r = resolved(
        "module leaf (input logic a, b, clk);
            a2: assert property (@(posedge clk) a |=> b);
         endmodule
         module top;
            bit clk, rst1, a, b;
            default disable iff rst1;
            a1: assert property (@(posedge clk) a |=> b);
            leaf u (a, b, clk);
         endmodule",
    );
    assert_eq!(r["a1"], "default rst1 (declared in top)");
    assert_eq!(r["a2"], "none");
}

/// 16.15: "The effect of a default disable iff declaration is independent of the
/// position of the declaration within that scope": declared after the assertion.
#[test]
fn default_is_position_independent() {
    let r = resolved(
        "module m;
            bit clk, rst, a, b;
            a1: assert property (@(posedge clk) a |=> b);
            default disable iff rst;
         endmodule",
    );
    assert_eq!(r["a1"], "default rst (declared in m)");
}

/// 16.15: "More than one default disable iff declaration within the same module ...
/// shall be an error", even if every assertion has its own clause.
#[test]
fn duplicate_defaults_are_an_error_even_when_every_assertion_has_a_clause() {
    let src = "module m;
            bit clk, rst1, rst2, a, b;
            default disable iff rst1;
            default disable iff rst2;
            a1: assert property (@(posedge clk) disable iff (rst1) a |=> b);
         endmodule";
    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();
    let tree = design.syntax_trees().into_iter().next().unwrap();
    let body = design
        .top_instances()
        .next()
        .unwrap()
        .instance_body()
        .unwrap();
    let err = resolve_disable(None, &body, &tree).expect_err("two defaults in one scope");
    assert!(err.to_string().contains("16.15"), "{err}");
    drop(analysis);
}