vj-codegen 0.1.0

//! Disable iff resolution (LRM 16.15; sva T27).
//!
//! The disable condition of a concurrent assertion is one of three things:
//!
//! 1. the condition of the `disable iff` the assertion itself carries -- written
//!    in the assertion, or in the property it instantiates -- "and any default
//!    disable iff declaration [is] ignored for this assertion" (rule a);
//! 2. else, if the assertion is "within the scope of a default disable iff
//!    declaration", the expression of that declaration (rule b), whose names
//!    "will be resolved from the scope of the declaration";
//! 3. else none, "equivalent to the inference of a 1'b0 disable condition" (rule c).
//!
//! The explicit clause is found by the property builder (`PropertyIr::disable`);
//! the default is found by [`default_disable_of`], which climbs the LEXICAL scope
//! chain (a nested module declaration inherits the default of the module it is
//! declared in, a module that is merely instantiated there does not), so the two
//! are combined here, in one place, and the rule that wins is part of the result.
//!
//! Nothing outside the tests calls [`resolve_disable`] until T29 lowers concurrent
//! assertion statements (the same state `build` and the other T3-T26 modules were
//! in), hence the `allow` below.
#![allow(dead_code)]
use sv_lang::kinds::{ExpressionKind, SymbolKind};
use sv_lang::nodes::DefaultDisableDeclarationSyntax;
use sv_lang::{AstNode, Expression, Symbol, SyntaxTree};
use sv_sim_sim::sva::ir::LeafId;

use sv_sim_sim::state::default_disable_of;

use crate::error::LoweringError;

/// Where the disable condition of one assertion comes from (16.15).
#[derive(Debug, Clone, Copy)]
pub enum DisableSource<'d, 't> {
    /// Rule (a): the `disable iff` the assertion carries; the leaf is its
    /// condition. A `default disable iff` in scope is ignored.
    Explicit(LeafId),
    /// Rule (b): the assertion has no clause of its own and the scope `scope`
    /// declares the default `decl`. The expression is bound in `scope`, the scope
    /// the default was DECLARED in, never in the assertion's own.
    Default {
        scope: Symbol<'d>,
        decl: DefaultDisableDeclarationSyntax<'t>,
    },
    /// Rule (c): no disable condition (`1'b0`).
    None,
}

/// Applies the three rules of 16.15 to the assertion in `scope`, whose property
/// spec has the `disable iff` condition `explicit` (`None`: it has none).
///
/// A scope with two `default disable iff` declarations is an error whatever the
/// assertion says ("More than one default disable iff declaration within the same
/// module, interface, program declaration, or generate block shall be an error"),
/// so the lookup runs even when rule (a) makes its result irrelevant.
pub fn resolve_disable<'d, 't>(
    explicit: Option<LeafId>,
    scope: &Symbol<'d>,
    tree: &'t SyntaxTree,
) -> Result<DisableSource<'d, 't>, LoweringError> {
    let default = default_disable_of(scope, tree).map_err(|e| {
        LoweringError::unsupported_at(&format!("default disable iff (LRM 16.15): {e:?}"), scope)
    })?;
    Ok(match (explicit, default) {
        (Some(leaf), _) => DisableSource::Explicit(leaf),
        (None, Some((scope, decl))) => DisableSource::Default { scope, decl },
        (None, None) => DisableSource::None,
    })
}

/// What of its signal a `default disable iff` operand tests (LRM 16.15).
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum TermPred {
    /// The whole signal (true where known non-zero).
    Whole,
    /// One bit, `sig[n]`; the payload is its position in the stored value
    /// (bit 0 = least significant), already mapped through the declared range.
    Bit(u32),
    /// `sig == value`: known only where the signal has no x/z bit. `!=` is
    /// this with the operand negated.
    Eq(u64),
}

/// The default disable condition of one assertion, as the executable subset
/// supports it (T31, 16.15 rule b): a signal, read live at every step, taken as
/// is or logically negated. sv-lang 0.1.9 exposes no bound expression for a
/// `default disable iff`, so the declaration's own text is resolved here.
#[derive(Debug, Clone, Copy)]
pub struct DefaultDisable<'d> {
    /// The signal the condition names, resolved from the scope of the
    /// declaration (16.15).
    pub signal: Symbol<'d>,
    /// The condition is `!signal`.
    pub negate: bool,
    /// A second signal joined to the first by `||` (`and == false`) or `&&`
    /// (`and == true`), as in `default disable iff (!rst_ni || flush_i)`; each
    /// operand is true where it is KNOWN true, so the join is exact for 4-state
    /// values (an unknown operand makes neither `||` of it nor `&&` with it true).
    pub second: Option<(Symbol<'d>, bool)>,
    /// How `second` joins `signal`.
    pub and: bool,
    /// What `signal` is tested for.
    pub pred: TermPred,
    /// What `second` is tested for.
    pub second_pred: TermPred,
}

impl<'d> DefaultDisable<'d> {
    /// The plain `(signal, negate)` of a condition that names one signal; a
    /// two-signal condition is refused loudly where only one fits (a checker's
    /// `$inferred_disable`).
    pub fn single(self, scope: &Symbol<'d>) -> Result<(Symbol<'d>, bool), LoweringError> {
        if self.second.is_some() || self.pred != TermPred::Whole {
            return Err(LoweringError::unsupported_at(
                "a `default disable iff` joining two signals, or testing a bit or a comparison, as `$inferred_disable` of a \
                 checker (LRM 17.4) is not executable yet",
                scope,
            ));
        }
        Ok((self.signal, self.negate))
    }
}

/// The actual argument bound to the checker formal `formal` (an `AssertionPort`
/// of a checker instance, LRM 17.2), or `None` when `formal` is no checker's.
fn checker_formal_actual<'d>(formal: &Symbol<'d>) -> Option<Expression<'d>> {
    if formal.kind() != SymbolKind::AssertionPort {
        return None;
    }
    let mut cur = formal.parent();
    let inst = loop {
        let s = cur?;
        if s.kind() == SymbolKind::CheckerInstance {
            break s;
        }
        if s.kind() == SymbolKind::CheckerInstanceBody {
            break s.checker_instance_body_parent_instance()?;
        }
        cur = s.parent();
    };
    let formals = inst.members().filter(|m| {
        matches!(
            m.kind(),
            SymbolKind::AssertionPort | SymbolKind::FormalArgument
        )
    });
    formals
        .zip(inst.checker_instance_connections())
        .find(|(f, _)| f.name() == formal.name())
        .and_then(|(_, conn)| conn.actual())
        .and_then(|a| a.as_expression())
}

/// [`resolve_default_disable`] for an assertion of a checker instance (LRM 17.2,
/// 17.4): the checker's `default disable iff reset;` names its formal `reset`, so
/// the condition is the signal the instance bound to it. The default
/// `$inferred_disable` is the `default disable iff` of `context`, the scope that
/// instantiates the checker; an actual that is a signal name (possibly `!`-negated
/// or parenthesised) is that signal. Anything else is a loud error: the condition
/// would otherwise be silently dropped.
pub fn resolve_checker_default_disable<'d>(
    scope: &Symbol<'d>,
    context: &Symbol<'d>,
    tree: &SyntaxTree,
) -> Result<Option<DefaultDisable<'d>>, LoweringError> {
    let Some(d) = resolve_default_disable(scope, tree)? else {
        return Ok(None);
    };
    let Some(actual) = checker_formal_actual(&d.signal) else {
        return Ok(Some(d));
    };
    d.single(scope)?;
    let mut negate = d.negate;
    let mut e = actual;
    loop {
        if e.call_subroutine_name().as_deref() == Some("$inferred_disable") {
            return resolve_default_disable(context, tree)?
                .map(|c| {
                    let (signal, cneg) = c.single(context)?;
                    Ok(DefaultDisable {
                        signal,
                        negate: cneg != negate,
                        second: None,
                        and: false,
                        pred: TermPred::Whole,
                        second_pred: TermPred::Whole,
                    })
                })
                .transpose();
        }
        if e.kind() == ExpressionKind::NamedValue
            && let Some(signal) = e.referenced_symbol()
        {
            return Ok(Some(DefaultDisable {
                signal,
                negate,
                second: None,
                and: false,
                pred: TermPred::Whole,
                second_pred: TermPred::Whole,
            }));
        }
        if e.kind() == ExpressionKind::UnaryOp
            && e.unary_op() == Some(sv_lang::UnaryOp::LogicalNot)
            && let Some(inner) = e.operand()
        {
            negate = !negate;
            e = inner;
            continue;
        }
        if e.kind() == ExpressionKind::Conversion
            && let Some(inner) = e.operand()
        {
            e = inner;
            continue;
        }
        return Err(LoweringError::unsupported_at(
            &format!(
                "`default disable iff ({})` of a checker (LRM 17.2): its formal is bound to \
                 an expression other than a signal name, `$inferred_disable` or the `!` of \
                 one, which is not executable yet",
                d.signal.name()
            ),
            scope,
        ));
    }
}

/// The `default disable iff` that applies to an assertion written in `scope`
/// (rule b), or `None` (rule c: a `1'b0` condition). An expression other than a
/// possibly parenthesised, possibly `!`-negated signal name is a loud error.
pub fn resolve_default_disable<'d>(
    scope: &Symbol<'d>,
    tree: &SyntaxTree,
) -> Result<Option<DefaultDisable<'d>>, LoweringError> {
    let Some((decl_scope, decl)) = default_disable_of(scope, tree).map_err(|e| {
        LoweringError::unsupported_at(&format!("default disable iff (LRM 16.15): {e:?}"), scope)
    })?
    else {
        return Ok(None);
    };
    let text = decl.expr().syntax().text();
    let whole = strip_outer_parens(text.trim());
    // One `||` or `&&` at the top level joins two operands.
    let (first, join, second) = match split_top_level(whole) {
        Some((a, and, b)) => (a, and, Some(b)),
        None => (whole, false, None),
    };
    let term = |t: &str| resolve_term(t, &text, scope, &decl_scope);
    let (signal, negate, pred) = term(first)?;
    let second = second.map(term).transpose()?;
    Ok(Some(DefaultDisable {
        signal,
        negate,
        second: second.map(|(s, n, _)| (s, n)),
        and: join,
        pred,
        second_pred: second.map_or(TermPred::Whole, |(_, _, p)| p),
    }))
}

/// `s` without any parentheses that enclose all of it.
fn strip_outer_parens(mut s: &str) -> &str {
    while s.starts_with('(') && s.ends_with(')') {
        let mut depth = 0i32;
        let mut closes_at_end = true;
        for (i, c) in s.char_indices() {
            match c {
                '(' => depth += 1,
                ')' => {
                    depth -= 1;
                    if depth == 0 && i + 1 != s.len() {
                        closes_at_end = false;
                        break;
                    }
                }
                _ => {}
            }
        }
        if !closes_at_end {
            break;
        }
        s = s[1..s.len() - 1].trim();
    }
    s
}

/// `a || b` / `a && b` split at the first operator outside any parentheses:
/// `(a, is_and, b)`.
fn split_top_level(s: &str) -> Option<(&str, bool, &str)> {
    let bytes = s.as_bytes();
    let mut depth = 0i32;
    let mut i = 0;
    while i + 1 < bytes.len() {
        match bytes[i] {
            b'(' => depth += 1,
            b')' => depth -= 1,
            b'|' | b'&' if depth == 0 && bytes[i + 1] == bytes[i] => {
                return Some((s[..i].trim(), bytes[i] == b'&', s[i + 2..].trim()));
            }
            _ => {}
        }
        i += 1;
    }
    None
}

/// One operand of a `default disable iff`: a possibly parenthesised signal
/// name under any number of `!` (or `~`, for a one-bit result), resolved from
/// the scope of the declaration. The name may carry a constant bit select
/// (`v[0]`) or be compared with a constant (`mode == 2'd1`, `!=`); such a
/// comparison must be parenthesised under a `!`/`~` (`!mode == 1` is
/// `(!mode) == 1`, LRM 11.3.2 precedence).
fn resolve_term<'d>(
    term: &str,
    text: &str,
    scope: &Symbol<'d>,
    decl_scope: &Symbol<'d>,
) -> Result<(Symbol<'d>, bool, TermPred), LoweringError> {
    let mut rest = term.trim();
    let mut negate = false;
    let mut bitwise = false;
    let mut after_prefix = false;
    loop {
        if let Some(r) = rest.strip_prefix('!') {
            negate = !negate;
            rest = r.trim_start();
            after_prefix = true;
        } else if let Some(r) = rest.strip_prefix('~') {
            negate = !negate;
            bitwise = true;
            rest = r.trim_start();
            after_prefix = true;
        } else if rest.starts_with('(') && rest.ends_with(')') {
            rest = strip_outer_parens(rest);
            after_prefix = false;
            if rest.starts_with('(') && rest.ends_with(')') {
                break;
            }
        } else {
            break;
        }
    }
    let refuse = |why: &str| {
        LoweringError::unsupported_at(
            &format!(
                "`default disable iff ({text})` (LRM 16.15): {why}; only signal names, a \
                 constant bit select or a comparison with a constant, each optionally negated, \
                 joined by one `||` or `&&`, are executable yet"
            ),
            scope,
        )
    };
    let is_name = |s: &str| {
        s.chars()
            .next()
            .is_some_and(|c| c.is_ascii_alphabetic() || c == '_')
            && s.chars()
                .all(|c| c.is_ascii_alphanumeric() || c == '_' || c == '$')
    };
    // `name == lit` / `name != lit` (not `===`, `!==`, `==?`).
    let mut cmp: Option<(&str, bool, &str)> = None;
    if let Some(i) = rest.find("==").or_else(|| rest.find("!=")) {
        let eq = rest.as_bytes()[i] == b'=';
        let after = &rest[i + 2..];
        if after.starts_with(['=', '?']) || (!eq && i > 0 && rest.as_bytes()[i - 1] == b'=') {
            return Err(refuse("a case or wildcard equality"));
        }
        cmp = Some((rest[..i].trim(), eq, after.trim()));
    }
    // `name[n]`.
    let mut select: Option<u32> = None;
    let name = match cmp {
        Some((n, _, _)) => n,
        None => rest,
    };
    let mut name = name;
    if let Some(open) = name.find('[')
        && name.ends_with(']')
    {
        let idx = name[open + 1..name.len() - 1].trim();
        let n: u32 = idx
            .replace('_', "")
            .parse()
            .map_err(|_| refuse("a bit select that is not a decimal constant"))?;
        select = Some(n);
        name = name[..open].trim();
    }
    if !is_name(name) {
        return Err(refuse("an operand that is not a signal name"));
    }
    if cmp.is_some() && after_prefix {
        return Err(refuse(
            "a comparison under a `!`/`~` that is not parenthesised",
        ));
    }
    if cmp.is_some() && select.is_some() {
        return Err(refuse("a comparison of a bit select"));
    }
    let mut cur = Some(*decl_scope);
    while let Some(s) = cur {
        if let Some(signal) = s.find(name) {
            let ty = signal.value_type();
            let width = ty.as_ref().map_or(0, |t| t.bit_width());
            let mut pred = TermPred::Whole;
            if let Some(n) = select {
                let t = ty.ok_or_else(|| refuse(&format!("`{name}` has no value type")))?;
                if !t.canonical().is_packed_array() || width <= 1 {
                    return Err(refuse(&format!("`{name}` is not a packed vector")));
                }
                let range = t.canonical().fixed_range();
                let (lo, hi) = (
                    i64::from(range.left.min(range.right)),
                    i64::from(range.left.max(range.right)),
                );
                if !(lo..=hi).contains(&i64::from(n)) {
                    return Err(refuse(&format!("bit {n} is outside `{name}`")));
                }
                // Stored bit 0 is the right bound's position (LRM 7.4.1).
                pred = TermPred::Bit(i64::from(n).abs_diff(i64::from(range.right)) as u32);
            } else if let Some((_, eq, lit)) = cmp {
                let (value, sized) = parse_literal(lit).ok_or_else(|| {
                    refuse("a comparison constant that is not a decimal or sized binary/octal/hex literal")
                })?;
                if signal.value_type().is_some_and(|t| t.is_signed()) && !sized && width < 32 {
                    return Err(refuse(&format!(
                        "an unsized constant against the signed `{name}` (sign extension)"
                    )));
                }
                if width < 64 && value >> width != 0 {
                    return Err(refuse(&format!(
                        "the constant {value} does not fit `{name}`"
                    )));
                }
                pred = TermPred::Eq(value);
                if !eq {
                    negate = !negate;
                }
            } else if bitwise && width != 1 {
                return Err(refuse(&format!("`~` of the multi-bit `{name}`")));
            }
            return Ok((signal, negate, pred));
        }
        cur = s.parent();
    }
    Err(refuse(&format!("`{name}` is not declared")))
}

/// A constant of a `default disable iff` comparison: a decimal, or a sized
/// `N'd`/`N'b`/`N'o`/`N'h` literal without x/z digits, fitting 64 bits.
/// `(value, sized)`.
fn parse_literal(lit: &str) -> Option<(u64, bool)> {
    let lit = lit.trim().replace('_', "");
    if let Some((size, rest)) = lit.split_once('\'') {
        let size: u32 = size.trim().parse().ok().filter(|&s| s > 0)?;
        let mut chars = rest.chars();
        let radix = match chars.next()?.to_ascii_lowercase() {
            'd' => 10,
            'b' => 2,
            'o' => 8,
            'h' => 16,
            _ => return None,
        };
        let value = u64::from_str_radix(chars.as_str().trim(), radix).ok()?;
        // A sized literal truncates to its size (LRM 5.7.1).
        let value = if size < 64 {
            value & ((1u64 << size) - 1)
        } else {
            value
        };
        return Some((value, true));
    }
    lit.parse::<u64>().ok().map(|v| (v, false))
}