vj 0.2.0

//! The planner's side of the verification section of a design image
//! ([`vj_sim::image::verif`]): what the assertion engines, checker free
//! variables and sampled-value bookkeeping need, written down once as plain data.
//!
//! `vj build-aot` serializes it into the `.so`'s image; `vj run` builds
//! the very same [`VerifImage`] over a scratch symbol table and a resolver over
//! its JIT session, then hands both to `vj_exec::verif::Verif`. One
//! description, one runtime: the two modes cannot drift apart.

use std::collections::HashMap;

use vj_abi::ProcessFn;
use vj_codegen::assertion::{AssertionSpec, LeafRole};
use vj_codegen::error::LoweringError;
use vj_codegen::pipeline::CompiledPipeline;
use vj_codegen::process_lower::{SignalSlot, SignalSlotClass};
use vj_exec::KernelResolver;
use vj_sim::image::verif::{
    AssertionImage, CasePairImage, FreeGroupImage, FreeVarImage, SampledImage, SampledSiteImage,
    SpawnCallImage, VerifImage,
};
use vj_sim::netlist::InstanceId;
use vj_sim::symid::{SymbolId, SymbolUid};

/// What the builder needs to know about the kernel of one plan: its mangled
/// name, frame size and instance.
pub(crate) struct KernelInfo<'a> {
    pub name: &'a str,
    pub frame_words: u32,
    pub instance: InstanceId,
}

/// One instance's body and signal slots, for the free variables and the sampled
/// value state.
pub(crate) struct BodyInfo<'a, 'd> {
    pub instance: InstanceId,
    pub body: &'a sv_lang::Symbol<'d>,
    pub signals: &'a HashMap<SymbolId, SignalSlot>,
    pub port_sources: &'a crate::clocking::PortSources,
}

/// Builds the [`VerifImage`] of a design.
///
/// `assertions` are the lowering's [`AssertionSpec`]s; `kernel(plan_index)` the
/// kernel behind a plan; `bodies` every registered instance body (in
/// registration order); `trees` the syntax trees (a clocking block's event may
/// name a default or global clocking); `covergroups` the design's covergroups;
/// `intern` assigns a symbol index to a function name.
pub(crate) fn build<'a, 'd>(
    assertions: &[AssertionSpec],
    kernel: impl Fn(usize) -> Option<KernelInfo<'a>>,
    bodies: &[BodyInfo<'_, 'd>],
    trees: &[sv_lang::SyntaxTree],
    covergroups: &crate::covergroups::CovPlan<'d>,
    mut intern: impl FnMut(&str) -> u32,
) -> Result<VerifImage, LoweringError> {
    // 19: the covergroups' tables and sampling events.
    let mut out = VerifImage {
        covergroups: crate::covergroups::image(covergroups, &mut intern)?,
        ..VerifImage::default()
    };
    for spec in assertions {
        let at = format!("assertion `{}`", spec.label);
        let k = kernel(spec.plan_index)
            .ok_or_else(|| LoweringError::unsupported("an assertion plan with no kernel", &at))?;
        let name = &spec.name;
        let ticks = (0..spec.n_clocks + spec.hist_clocks)
            .map(|c| intern(&format!("{name}_t{c}")))
            .collect();
        let leaves: Vec<Option<u32>> = spec
            .roles
            .iter()
            .enumerate()
            .map(|(i, role)| match role {
                LeafRole::Unused => None,
                LeafRole::Bool | LeafRole::Value => Some(intern(&format!("{name}_l{i}"))),
            })
            .collect();
        // `{name}_lv{i}`, the live-state form of a leaf that holds a sampled
        // value function (16.12), for the leaves `spec.live_calls` names.
        let mut live_leaves: Vec<Option<u32>> = vec![None; leaves.len()];
        for &l in &spec.live_calls {
            if let Some(slot) = live_leaves.get_mut(l as usize) {
                *slot = Some(intern(&format!("{name}_lv{l}")));
            }
        }
        let cases = spec
            .case_pairs
            .iter()
            .enumerate()
            .map(|(i, (selector, label))| CasePairImage {
                selector: *selector,
                label: *label,
                symbol: intern(&format!("{name}_c{i}")),
            })
            .collect();
        out.assertions.push(AssertionImage {
            plan_index: spec.plan_index as u32,
            instance: k.instance,
            kernel: intern(k.name),
            frame_words: k.frame_words,
            label: spec.label.clone(),
            kind: spec.kind,
            ir: spec.ir.clone(),
            n_clocks: spec.n_clocks as u32,
            hist_clocks: spec.hist_clocks as u32,
            leaf_reads: spec.leaf_reads.clone(),
            leaf_writes: spec.leaf_writes.clone(),
            activated: spec.activated,
            disable_mixed: spec.disable_mixed,
            tick_history: spec.tick_history,
            captured: spec.captured.clone(),
            history_depth: spec.history_depth as u32,
            future: spec.future,
            future_clock: spec.future_clock,
            src_offset: spec.src_offset,
            leaf_src: spec.leaf_src.clone(),
            row_len: spec.row_len as u32,
            snap: intern(&format!("{name}_snap")),
            ticks,
            leaves,
            live_leaves,
            cases,
            site: spec.site.clone(),
            end_cell: spec.end_cell,
            current_words: spec
                .current_words
                .iter()
                .map(|(id, first, n)| (id.key_string(), *first as u32, *n as u32))
                .collect(),
            observed_words: spec
                .observed_words
                .iter()
                .map(|&(first, n)| (first as u32, n as u32))
                .collect(),
            coll_words: spec.coll_words.iter().map(|&w| w as u32).collect(),
            coll_nests: spec.coll_nests.clone(),
            spawn_calls: spec
                .spawn_calls
                .iter()
                .map(|c| SpawnCallImage {
                    call: c.call,
                    kernel: intern(&c.kernel),
                    frame_words: c.frame_words,
                    entry_pc: c.entry_pc,
                })
                .collect(),
        });
    }

    for b in bodies {
        // 14.13: the clocking blocks' samplers, in registration order.
        out.clocking.extend(crate::clocking::samplers(
            b.body,
            b.instance,
            b.signals,
            trees,
            b.port_sources,
            &mut intern,
        )?);
        // 17.7.2: the active free variables of each checker instance.
        for (_, vars) in vj_sim::netlist::free_var_groups(b.body) {
            let rng = vj_sim::netlist::free_var_seed(&vars[0]) ^ 0x5eed;
            let vars = vars
                .iter()
                .filter_map(|v| {
                    let info = b.signals.get(&v.uid())?;
                    Some(FreeVarImage {
                        id: v.uid().key_string(),
                        slot: info.slot,
                        width: info.width,
                        wide: info.class == SignalSlotClass::Wide,
                    })
                })
                .collect();
            out.free_groups.push(FreeGroupImage {
                instance: b.instance,
                vars,
                rng,
            });
        }
        // Sampled value functions: the hidden cells' shift sites and P copies.
        let at = b.body.hierarchical_path();
        let hidden = vj_sim::sva::sampled::hidden_slots(b.body)
            .map_err(|e| LoweringError::unsupported(&e.0, &at))?;
        if hidden.is_empty() {
            continue;
        }
        let slot_of = |id: &SymbolId| -> Result<u32, LoweringError> {
            b.signals.get(id).map(|s| s.slot).ok_or_else(|| {
                LoweringError::unsupported(
                    &format!(
                        "a sampled value function's hidden cell `{}` has no slot",
                        id.path()
                    ),
                    &at,
                )
            })
        };
        let mut sites = Vec::new();
        for site in &hidden.sites {
            let mut shifts = Vec::with_capacity(site.shifts.len());
            for step in &site.shifts {
                shifts.push((slot_of(&step.from)?, slot_of(&step.to)?));
            }
            sites.push(SampledSiteImage {
                guard: intern(&site.guard_name),
                shifts,
            });
        }
        let mut p_copies = Vec::with_capacity(hidden.p.len());
        for p in &hidden.p {
            if let Some(shape) = &p.foreign {
                // A candidate event signal of an enclosing instance's
                // clocking block (`hidden_slots`): only the global clocking
                // the lookup picked was registered as a foreign reference.
                // A hierarchical reference in a call is always registered.
                let Some(src) = b.signals.get(&p.source) else {
                    if shape.required {
                        return Err(LoweringError::unsupported(
                            &format!(
                                "a sampled value function over `{}`, a signal of another \
                                 instance that this instance has no reference to",
                                p.source.path()
                            ),
                            &at,
                        ));
                    }
                    continue;
                };
                // The cell's shape came from the first instance of the
                // template; another instance under a differently-typed clock
                // would be copied into the wrong width.
                if b.signals.get(&p.id).is_none_or(|c| c.width != src.width) {
                    return Err(LoweringError::unsupported(
                        &format!(
                            "the global clocking's event signal `{}` has a different width in \
                             two instances of one module; a sampled value function's clock \
                             history needs one width (LRM 14.14)",
                            p.source.path()
                        ),
                        &at,
                    ));
                }
            }
            p_copies.push((slot_of(&p.source)?, slot_of(&p.id)?));
        }
        out.sampled.push(SampledImage {
            instance: b.instance,
            sites,
            p_copies,
        });
    }
    Ok(out)
}

/// A symbol table that is not an image's: the JIT's, where each name is looked
/// up in the session instead of the `.so`.
#[derive(Default)]
pub(crate) struct ScratchSymbols {
    pub names: Vec<String>,
    index: HashMap<String, u32>,
}

impl ScratchSymbols {
    pub(crate) fn intern(&mut self, name: &str) -> u32 {
        if let Some(&i) = self.index.get(name) {
            return i;
        }
        let i = self.names.len() as u32;
        self.names.push(name.to_owned());
        self.index.insert(name.to_owned(), i);
        i
    }
}

/// A [`KernelResolver`] over the JIT session: a kernel by its process
/// function, every other symbol by the address of the function itself.
pub(crate) struct PipelineResolver<'p>(pub &'p CompiledPipeline);

impl KernelResolver for PipelineResolver<'_> {
    fn resolve(&self, _index: u32, name: &str) -> Option<ProcessFn> {
        self.0.get_process_fn(name)
    }

    fn address(&self, _index: u32, name: &str) -> Option<usize> {
        self.0.get_global_ptr(name).map(|p| p as usize)
    }
}