vj-codegen 0.1.0

//! Procedural concurrent assertions (16.14.6, plan T30).
//!
//! An assertion statement inside a procedural block is *reached* by the process,
//! not evaluated by it. Reaching it queues an instance of the assertion with the
//! values the process has at that moment of every **automatic variable** and
//! every **`const'(expr)`** the assertion (its property and its pass/fail
//! statements) uses; everything else it names is a module signal, read from the
//! sampled values like any static assertion.
//!
//! Each such assertion is split in two (the same way a static one is):
//!
//! * the **host plan**, an extra one-shot process the module discovery adds right
//!   after the enclosing process ([`crate::module::DiscoveredProcess::assertion`]),
//!   whose root is the assertion statement itself: the engine of `sv-sim-bin`
//!   resumes it in the Reactive region to run the pass or fail statement, with the
//!   instance's captured values readable ([`SV_RT_ASSERT_INPUT_SYMBOL`] in
//!   `process_lower`);
//! * the **queue call** the enclosing process executes where the statement is,
//!   which hands the captured values to `sv_rt_proc_assert`.
//!
//! Both halves derive the captured items from the statement with
//! [`capture_items`], so they agree on count, order and meaning.

use std::collections::HashMap;

use sv_lang::kinds::{ExpressionKind, SymbolKind};
use sv_lang::{Expression, SemNode, Statement, Symbol, VariableLifetime};
use sv_sim_sim::symid::{SymbolId, SymbolUid};

use crate::error::LoweringError;
use crate::process_lower::SignalSlot;
use crate::types::TypeWidth;

/// An assertion statement hosted by its own plan. A procedural one with no clock
/// of its own infers the enclosing block's (16.14.6, resolved at emission).
#[derive(Clone, Copy)]
pub struct HostedAssertion<'d> {
    pub stmt: Statement<'d>,
    /// Nested in a procedural block (16.14.6), whose process queues instances of
    /// it; `false` for a static assertion (a new attempt at every clock tick).
    pub procedural: bool,
    /// The procedural checker instance (17.3) whose static assertion this is:
    /// the procedure that instantiates the checker queues it where the
    /// instantiation is reached, exactly like a procedural assertion of its own
    /// (`stmt` is then in the checker's body, which every instance of the same
    /// checker shares). `None` for an assertion written in the block itself.
    pub instance: Option<Symbol<'d>>,
}

impl<'d> HostedAssertion<'d> {
    /// The key under which the process that queues this assertion finds the
    /// plan hosting it ([`queued_assertion_key`]); `block` is the process.
    pub fn queue_key(&self, block: &Symbol<'_>) -> String {
        queued_assertion_key(block, self.instance.as_ref(), &self.stmt)
    }
}

impl std::fmt::Debug for HostedAssertion<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        let s = self.stmt.source_range().start;
        write!(f, "HostedAssertion({}.{})", s.buffer, s.offset)
    }
}

impl PartialEq for HostedAssertion<'_> {
    fn eq(&self, other: &Self) -> bool {
        self.stmt.source_range().start == other.stmt.source_range().start
            && self.instance.map(|i| i.uid()) == other.instance.map(|i| i.uid())
    }
}

impl Eq for HostedAssertion<'_> {}

/// The identity of the assertion statement `stmt` of the procedural block `block`:
/// two generate-loop copies of one block share a source location, hence the
/// block's own key.
pub fn assertion_key(block: &Symbol<'_>, stmt: &Statement<'_>) -> String {
    let s = stmt.source_range().start;
    format!("{}@{}.{}", block.uid().key_string(), s.buffer, s.offset)
}

/// [`assertion_key`] for an assertion of a procedural checker instance
/// `instance` (17.3) that the procedure `block` queues: every instance of one
/// checker shares the statement, so the instance is part of the identity.
pub fn queued_assertion_key(
    block: &Symbol<'_>,
    instance: Option<&Symbol<'_>>,
    stmt: &Statement<'_>,
) -> String {
    let base = assertion_key(block, stmt);
    match instance {
        Some(i) => format!("{base}#{}", i.uid().key_string()),
        None => base,
    }
}

/// One value an assertion instance captures when the process reaches it.
#[derive(Clone)]
pub struct CaptureItem<'d> {
    /// Where the lowered code finds the value: the variable's own key, or the
    /// synthetic key of a `const'(expr)` ([`SymbolId::synthetic_tagged`]).
    pub key: SymbolId,
    /// The expression the enclosing process evaluates to get the value: the
    /// variable's name, or the const cast itself.
    pub expr: Expression<'d>,
    pub width: u32,
    pub signed: bool,
}

impl CaptureItem<'_> {
    /// How many `i64` words the value travels in (the instance's capture buffer,
    /// the engine's frame slots, the action's inputs): one for a value of at most
    /// 64 bits (two-state, sign-extended when signed), and for a wider one
    /// `2 * ceil(width / 64)`: its value limbs, least significant first, then its
    /// unknown-plane limbs, so `x`/`z` bits survive the capture. This is the slot
    /// layout of a wide local variable ([`sv_sim_sim::sva::wide`]).
    pub fn words(&self) -> usize {
        if self.width > 64 {
            2 * (self.width as usize).div_ceil(64)
        } else {
            1
        }
    }
}

/// The total number of words `items` travel in ([`CaptureItem::words`]).
pub fn capture_words(items: &[CaptureItem<'_>]) -> usize {
    items.iter().map(CaptureItem::words).sum()
}

/// The synthetic key of the `const'(expr)` conversion `e`.
pub fn const_cast_key(e: &Expression<'_>) -> SymbolId {
    let s = e.source_range().start;
    SymbolId::synthetic_tagged(&format!("const_cast.{}.{}", s.buffer, s.offset))
}

/// The synthetic key under which the sampled value of the by-value actual `e` of
/// a subroutine call attached to a sequence (16.11) is primed while the call is
/// lowered: `lower_expr` finds `e` in `cx.locals` under it and reads the sampled
/// value instead of lowering the live expression.
pub fn call_arg_key(e: &Expression<'_>) -> SymbolId {
    let r = e.source_range();
    SymbolId::synthetic(&format!(
        "call_arg.{}.{}.{}",
        r.start.buffer, r.start.offset, r.end.offset
    ))
}

thread_local! {
    static CALL_ARGS_ACTIVE: std::cell::Cell<bool> = const { std::cell::Cell::new(false) };
}

/// Whether a match-item call is being lowered ([`CallArgScope`]), i.e. whether
/// `lower_expr` has to look for a sampled by-value actual. A flag so the lookup's
/// key is never built for any other expression.
pub fn call_args_active() -> bool {
    CALL_ARGS_ACTIVE.with(std::cell::Cell::get)
}

thread_local! {
    /// The by-value actuals of a spawned match-item task ([`SpawnArgScope`]): per
    /// [`call_arg_key`], the first assertion input word, the width and the
    /// signedness of the value the engine sampled.
    static SPAWN_ARGS: std::cell::RefCell<std::collections::HashMap<SymbolId, (usize, u32, bool)>> =
        std::cell::RefCell::new(std::collections::HashMap::new());
}

/// The assertion input a spawned match-item task's by-value actual `key` is read
/// from (`(first word, width, signed)`), while a [`SpawnArgScope`] is live.
pub fn spawn_arg_input(key: &SymbolId) -> Option<(usize, u32, bool)> {
    SPAWN_ARGS.with(|m| m.borrow().get(key).copied())
}

/// Marks the lowering of the process a match-item task call (16.11) runs as:
/// its formals are bound from the call's actuals in the process's own entry
/// block, and each by-value actual reads the value the engine sampled, from the
/// assertion inputs (`args`), where the inline lowering of the same call reads
/// primed locals ([`CallArgScope`]).
pub struct SpawnArgScope {
    _active: CallArgScope,
}

impl SpawnArgScope {
    pub fn enter(args: Vec<(SymbolId, (usize, u32, bool))>) -> SpawnArgScope {
        SPAWN_ARGS.with(|m| *m.borrow_mut() = args.into_iter().collect());
        SpawnArgScope {
            _active: CallArgScope::enter(),
        }
    }
}

impl Drop for SpawnArgScope {
    fn drop(&mut self) {
        SPAWN_ARGS.with(|m| m.borrow_mut().clear());
    }
}

/// Marks the lowering of one match-item call (16.11) for its lifetime.
pub struct CallArgScope(bool);

impl CallArgScope {
    pub fn enter() -> CallArgScope {
        CallArgScope(CALL_ARGS_ACTIVE.with(|c| c.replace(true)))
    }
}

impl Drop for CallArgScope {
    fn drop(&mut self) {
        CALL_ARGS_ACTIVE.with(|c| c.set(self.0));
    }
}

/// Whether `e` is an explicit `const'(expr)` cast.
pub fn is_const_cast(e: &Expression<'_>) -> bool {
    e.kind() == ExpressionKind::Conversion && e.conversion_is_const_cast() == Some(true)
}

/// Every automatic variable and outermost `const'(expr)` the assertion `stmt`
/// uses, in a deterministic order, each once. A variable is a module signal (and
/// so sampled, not captured) when `signals` has it.
///
/// A value of at most 64 bits is captured as a two-state `i64`; a wider one as
/// its four-state limbs ([`CaptureItem::words`]).
pub fn capture_items<'d>(
    signals: &HashMap<SymbolId, SignalSlot>,
    stmt: Statement<'d>,
    at: &Symbol<'d>,
) -> Result<Vec<CaptureItem<'d>>, LoweringError> {
    let mut items: Vec<CaptureItem<'d>> = Vec::new();
    // An `expect` (16.17) runs its pass/fail statements in the very process that
    // blocked on it, which reads its variables directly: only the property is
    // captured.
    let is_expect = stmt.assertion_kind() == Some(sv_lang::AssertionKind::Expect);
    let mut roots: Vec<SemNode<'d>> = if is_expect {
        Vec::new()
    } else {
        vec![stmt.as_sem_node()]
    };
    // The property's leaves: the generic walk does not reach every one (a named
    // sequence/property's arguments, a match item's expressions).
    if let Some(root) = stmt
        .as_sem_node()
        .children()
        .into_iter()
        .find_map(|n| n.as_assertion_expr())
    {
        let mut leaves = Vec::new();
        crate::sva::collect_boolean_leaves(root, &mut leaves);
        if is_expect {
            roots.push(root.as_sem_node());
        }
        roots.extend(leaves.into_iter().map(|l| l.as_sem_node()));
    }
    for root in roots {
        let mut stack = vec![root];
        while let Some(n) = stack.pop() {
            if let Some(e) = n.as_expression() {
                if is_const_cast(&e) {
                    let key = const_cast_key(&e);
                    if !items.iter().any(|i| i.key == key) {
                        items.push(item_of(key, e, at)?);
                    }
                    continue;
                }
                if matches!(
                    e.kind(),
                    ExpressionKind::NamedValue | ExpressionKind::HierarchicalValue
                ) && let Some(sym) = e.referenced_symbol()
                    && ((sym.kind() == SymbolKind::Variable
                        && sym.variable_lifetime() == VariableLifetime::Automatic)
                        // A task's formal (`task automatic wait_for(integer value, ..)`)
                        // is a local of the process that inlines the task.
                        || sym.kind() == SymbolKind::FormalArgument
                        // A `foreach` loop variable is an automatic local of the
                        // loop, captured like a `for` loop's (16.14.6).
                        || sym.kind() == SymbolKind::Iterator)
                    && !signals.contains_key(&sym.uid())
                {
                    let key = sym.uid();
                    if !items.iter().any(|i| i.key == key) {
                        items.push(item_of(key, e, at)?);
                    }
                }
            }
            let mut kids = n.children();
            kids.reverse();
            stack.extend(kids);
        }
    }
    items.sort_by(|a, b| a.key.cmp(&b.key));
    Ok(items)
}

/// The variables and nets the outermost `const'(expr)` casts of `stmt` read: the
/// procedure itself evaluates them when it reaches the assertion, so an
/// `always_comb`/`always_latch` is sensitive to them (9.2.2.2.1, 16.14.6.2).
pub fn const_cast_reads<'d>(stmt: Statement<'d>) -> Vec<Symbol<'d>> {
    let mut roots: Vec<SemNode<'d>> = vec![stmt.as_sem_node()];
    if let Some(root) = stmt
        .as_sem_node()
        .children()
        .into_iter()
        .find_map(|n| n.as_assertion_expr())
    {
        let mut leaves = Vec::new();
        crate::sva::collect_boolean_leaves(root, &mut leaves);
        roots.extend(leaves.into_iter().map(|l| l.as_sem_node()));
    }
    let mut out: Vec<Symbol<'d>> = Vec::new();
    for root in roots {
        let mut stack = vec![(root, false)];
        while let Some((n, inside)) = stack.pop() {
            let mut inside = inside;
            if let Some(e) = n.as_expression() {
                if is_const_cast(&e) {
                    inside = true;
                }
                if inside
                    && matches!(
                        e.kind(),
                        ExpressionKind::NamedValue | ExpressionKind::HierarchicalValue
                    )
                    && let Some(sym) = e.referenced_symbol()
                    && matches!(sym.kind(), SymbolKind::Variable | SymbolKind::Net)
                    && !out.contains(&sym)
                {
                    out.push(sym);
                }
            }
            stack.extend(n.children().into_iter().map(|k| (k, inside)));
        }
    }
    out
}

fn item_of<'d>(
    key: SymbolId,
    expr: Expression<'d>,
    at: &Symbol<'d>,
) -> Result<CaptureItem<'d>, LoweringError> {
    let ty = expr.expr_type().ok_or_else(|| {
        LoweringError::unsupported_at("a captured value with no type in an assertion", at)
    })?;
    if !ty.is_integral() {
        return Err(LoweringError::unsupported_at(
            "a captured real, string or aggregate value in a procedural concurrent assertion is \
             not executable yet",
            at,
        ));
    }
    let width = ty.value_width();
    if width == 0 {
        return Err(LoweringError::unsupported_at(
            "a captured value of no bits in a procedural concurrent assertion",
            at,
        ));
    }
    Ok(CaptureItem {
        key,
        expr,
        width,
        signed: ty.is_signed(),
    })
}

/// The name of the first value `leaf` reads that is neither a captured value
/// (`items`) nor an elaboration-time constant: a signal, memory or other
/// variable whose current or sampled value the leaf would need.
pub fn first_non_captured_read(items: &[CaptureItem<'_>], leaf: Expression<'_>) -> Option<String> {
    let mut stack = vec![leaf.as_sem_node()];
    while let Some(n) = stack.pop() {
        if let Some(e) = n.as_expression() {
            if is_const_cast(&e) || e.constant_value().is_some() {
                continue;
            }
            if matches!(
                e.kind(),
                ExpressionKind::NamedValue | ExpressionKind::HierarchicalValue
            ) && let Some(sym) = e.referenced_symbol()
                && !items.iter().any(|it| it.key == sym.uid())
            {
                return Some(sym.name().to_string());
            }
        }
        stack.extend(n.children());
    }
    None
}

/// The indices into `items` of the captured values `leaf` (an expression of the
/// assertion) refers to.
pub fn items_used_by(items: &[CaptureItem<'_>], leaf: Expression<'_>) -> Vec<usize> {
    let mut used = Vec::new();
    if items.is_empty() {
        return used;
    }
    let mut stack = vec![leaf.as_sem_node()];
    while let Some(n) = stack.pop() {
        if let Some(e) = n.as_expression() {
            if is_const_cast(&e) {
                let key = const_cast_key(&e);
                if let Some(i) = items.iter().position(|it| it.key == key)
                    && !used.contains(&i)
                {
                    used.push(i);
                }
                continue;
            }
            if matches!(
                e.kind(),
                ExpressionKind::NamedValue | ExpressionKind::HierarchicalValue
            ) && let Some(sym) = e.referenced_symbol()
                && let key = sym.uid()
                && let Some(i) = items.iter().position(|it| it.key == key)
                && !used.contains(&i)
            {
                used.push(i);
            }
        }
        stack.extend(sv_sim_sim::process::cfg::live_children(&n));
    }
    used
}