vj_sim/image/

verif.rs

//! The verification half of a [`DesignImage`](super::DesignImage): what the
//! assertion engines, the sampled-value bookkeeping, the clocking-block
//! samplers and the covergroup runtime need beyond the kernels' machine code.
//!
//! Every function an entry refers to is a [`DesignImage::symbols`](super::DesignImage::symbols)
//! index, resolved by the same `KernelResolver` the kernels are (the signature
//! behind a symbol is fixed by what `vj-codegen` emits, see
//! `vj_exec::verif`). Nothing here names an `sv-lang` type, so a `.so`
//! carries it and a slang-free runner reads it: a design symbol is its
//! `SymbolId::key_string` text.

use crate::netlist::InstanceId;
use crate::sched::assert_control::SiteDesc;
use crate::state::EdgeKind;
use crate::sva::engine::AssertKind;
use crate::sva::ir::{LeafId, LocalVarId};
use crate::sva::property::PropertyIr;

/// One `(selector leaf, label leaf)` comparison of a property `case`, and the
/// compiled function that evaluates it.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct CasePairImage {
    pub selector: LeafId,
    pub label: LeafId,
    pub symbol: u32,
}

/// One concurrent assertion, procedural assertion, `expect`, sequence end-point
/// watcher or checker assertion: everything `vj_codegen::sva::emit::AssertionSpec`
/// carries, plus the symbols of the functions it compiled.
#[derive(Clone, Debug, PartialEq)]
pub struct AssertionImage {
    /// The plan index of the assertion's kernel: the key of its queued
    /// procedural instances and of its assertion-control site.
    pub plan_index: u32,
    pub instance: InstanceId,
    /// The kernel the assertion's action blocks run in (resumed with the
    /// pass/fail term; never registered as a process of its own).
    pub kernel: u32,
    pub frame_words: u32,
    pub label: String,
    pub kind: AssertKind,
    pub ir: PropertyIr,
    pub n_clocks: u32,
    /// Sampled value functions' own history clocks (16.12), beyond the
    /// assertion's own `n_clocks`: `ticks` has `n_clocks + hist_clocks`
    /// entries (`vj_sim::sva::engine::EngineConfig::hist_clocks`).
    pub hist_clocks: u32,
    pub leaf_reads: Vec<Vec<LocalVarId>>,
    pub leaf_writes: Vec<Option<LocalVarId>>,
    pub activated: bool,
    pub captured: Vec<LocalVarId>,
    /// See `EngineConfig::disable_mixed`.
    pub disable_mixed: bool,
    /// See `EngineConfig::tick_history`.
    pub tick_history: bool,
    pub history_depth: u32,
    pub future: bool,
    /// The clock (an index into all `n_clocks + hist_clocks`) whose next tick
    /// a `future`-sampled call's row holds, or `0` for a design with none.
    pub future_clock: u32,
    /// The byte offset of the assertion statement's own source range, for
    /// VPI assertion control (36.9, `None`: not an assertion statement).
    pub src_offset: Option<u64>,
    /// Per leaf, its expression's source range: what VPI reports a step's or
    /// a failure's leaves as (39.4.2).
    pub leaf_src: Vec<(u32, u64, u64)>,
    /// Entries in a sampled row.
    pub row_len: u32,
    /// `{name}_snap`.
    pub snap: u32,
    /// `{name}_t{c}` per clock (`n_clocks + hist_clocks` of them).
    pub ticks: Vec<u32>,
    /// `{name}_l{i}` per leaf; `None` for a leaf the engine never evaluates.
    pub leaves: Vec<Option<u32>>,
    /// `{name}_lv{i}`, parallel to `leaves`: the live-state form of a leaf
    /// that holds a sampled value function (16.12), evaluated on a position
    /// row instead of a plain signal row. `None` where `leaves[i]` is also
    /// `None`, or the leaf has no such function.
    pub live_leaves: Vec<Option<u32>>,
    /// `{name}_c{k}` per `case` comparison.
    pub cases: Vec<CasePairImage>,
    /// The assertion-control registry entry (20.11); `None` for a directive no
    /// control task reaches.
    pub site: Option<SiteDesc>,
    /// A sequence end-point watcher's cell (`AssertionSpec::end_cell`).
    pub end_cell: Option<u32>,
    /// `(design symbol key, first word, word count)`: the sampled-row words a
    /// checker free variable occupies (`AssertionSpec::current_words`).
    pub current_words: Vec<(String, u32, u32)>,
    /// `(first word, word count)` of the row words refreshed from the live
    /// cells at the Observed region (`AssertionSpec::observed_words`).
    pub observed_words: Vec<(u32, u32)>,
    /// The row words holding a collection handle (`AssertionSpec::coll_words`).
    pub coll_words: Vec<u32>,
    /// Per `coll_words` entry, where the collections inside its elements sit
    /// (`AssertionSpec::coll_nests`); no slots for a flat collection.
    pub coll_nests: Vec<crate::collections::Nest>,
    /// The match-item calls that run as processes of their own
    /// (`AssertionSpec::spawn_calls`).
    pub spawn_calls: Vec<SpawnCallImage>,
}

/// A sequence match-item call of a task that can suspend (16.11): the runner
/// spawns the kernel at each end point.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct SpawnCallImage {
    /// The call's index: its fired term is `2 + call`.
    pub call: u32,
    /// The kernel's symbol, a `ProcessFn`.
    pub kernel: u32,
    pub frame_words: u32,
    pub entry_pc: u32,
}

/// One active free variable of a checker instance (17.7.2).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct FreeVarImage {
    /// The design symbol's key, matched against `AssertionImage::current_words`.
    pub id: String,
    pub slot: u32,
    pub width: u32,
    pub wide: bool,
}

/// The active free variables of one checker instance.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct FreeGroupImage {
    pub instance: InstanceId,
    pub vars: Vec<FreeVarImage>,
    /// The generator the values are drawn from.
    pub rng: u64,
}

/// One clocked sampled-value call site: when its compiled guard reports the
/// clocking event occurred, the value history shifts.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct SampledSiteImage {
    /// The `vj_sva_guard_*` function (`extern "C" fn(SimHandle) -> u8`).
    pub guard: u32,
    /// `(from, to)` slots, in the order they must run.
    pub shifts: Vec<(u32, u32)>,
}

/// One instance's sampled-value state (`vj_sim::sva::sampled::hidden_slots`).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct SampledImage {
    pub instance: InstanceId,
    pub sites: Vec<SampledSiteImage>,
    /// `(signal, its P cell)`.
    pub p_copies: Vec<(u32, u32)>,
}

/// [`ClockingImage::skews`] code for `#1step`.
pub const SKEW_STEP: u64 = u64::MAX;

/// [`ClockingImage::skews`] code for an edge skew naming the edge OPPOSITE the
/// clocking event's (LRM 14.4): the value at the end of the step of the clock
/// signal's latest such edge. The event's own edge is `0`.
pub const SKEW_EDGE_OPP: u64 = u64::MAX - 1;

/// One clocking block's sampler (14.13): woken by the clocking event, it copies
/// each input clock variable's signal into its sample cell, then bumps the
/// event counter that `@(cb)` and `##N` wait on.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct ClockingImage {
    pub instance: InstanceId,
    /// The clocking event's terms: `(signal slot, edge)`; `None` is any change.
    pub terms: Vec<(u32, Option<EdgeKind>)>,
    /// `iff` guards (9.4.2.3, 14.12) as `(term index, gate function symbol)`
    /// (`u64 gate(handle)`, 1 = condition known true): a term that fired counts
    /// only while all of its gates hold, and the event is a clocking event if any
    /// fired term counts. Empty = ungated.
    pub gates: Vec<(u32, u32)>,
    /// `(signal slot, sample slot, width)` per input clock variable.
    pub samples: Vec<(u32, u32, u32)>,
    /// The input skew of each of `samples` (14.4), in scheduler ticks:
    /// [`SKEW_STEP`] is `#1step` (the Preponed value), `0` an explicit `#0`
    /// (sampled in the Observed region), `N` the value at the end of the time
    /// step `N` ticks before the event.
    pub skews: Vec<u64>,
    /// Per sample, the parts of a derived input clock variable source (14.5:
    /// `input x = a[3:0]`, `input y = {a, b[2:1]}`): `(signal slot, signal
    /// width, lsb, len)`, most significant first. An empty list (or a
    /// missing entry) is the plain signal of `samples`.
    pub parts: Vec<Vec<(u32, u32, u32, u32)>>,
    /// The block's event counter slot.
    pub counter: u32,
    /// The instance that owns each of `terms`' signal slots, parallel to it.
    /// A block clocked by an input port's wire is woken by the PARENT's signal
    /// the port connects to (14.13: the clocking event and the parent's
    /// `@(posedge clk)` are one event), not by the port's continuous-assignment
    /// copy, which updates a delta later.
    pub term_owners: Vec<InstanceId>,
}

/// The sampler of a covergroup with a clocking event (19.3: `covergroup cg
/// @(posedge clk)` samples every instance of itself on each event).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct CovSamplerImage {
    /// The event's terms: `(signal slot, edge)`; `None` is any change.
    pub terms: Vec<(u32, Option<EdgeKind>)>,
    /// `iff` gates (9.4.2.3) as `(term index, gate function symbol)`, the symbol
    /// as `ClockingImage::gates`: a term that fired counts only while all of its
    /// gates hold, and the event samples if any fired term counts.
    pub gates: Vec<(u32, u32)>,
    /// The terms that are an edge or a change of an EXPRESSION or select
    /// (`@(posedge a[3])`, `@(posedge (a & b))`), not of a whole signal.
    pub exprs: Vec<CovExprTermImage>,
    /// `type_option.strobe` (19.7.1): sample at the end of the time slot.
    pub strobe: bool,
}

/// A sampling-event term on an expression (19.3, 9.4.2): the sampler wakes on
/// a change of any signal the expression reads (the `wake` terms of
/// [`CovSamplerImage::terms`], each `(slot, any change)`), re-evaluates it
/// with `func` and compares with the value of the previous wake.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct CovExprTermImage {
    /// The value function symbol, `u64 f(handle)`: with an `edge`, bit 0 is the
    /// expression's least significant bit and bit 1 whether it is `x`/`z`;
    /// without one, the value in bits 0..32 and its unknown bits in 32..64.
    pub func: u32,
    /// `None` is any change of the value.
    pub edge: Option<EdgeKind>,
    /// Indices into the sampler's `terms` of the signals the expression reads.
    pub wake: Vec<u32>,
    /// `iff` gate function symbols (9.4.2.3) of this term.
    pub gates: Vec<u32>,
}

/// The clocking event of a class-embedded covergroup whose event reads a
/// property of each object (19.4: `covergroup cg @(posedge clk)` with `clk` a
/// class property): one watcher for the type polls every object's event
/// expressions whenever object state changes.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct CovClassClockImage {
    /// The event's terms: `(kernel id of the term's expression, edge)`; `None`
    /// is any change.
    pub terms: Vec<(u32, Option<EdgeKind>)>,
    /// `iff` gates (9.4.2.3) as `(term index, kernel id)`.
    pub gates: Vec<(u32, u32)>,
    /// `type_option.strobe` (19.7.1): sample at the end of the time slot.
    pub strobe: bool,
}

/// One covergroup of the design as compiled for one module instance (19.3).
#[derive(Clone, Debug, PartialEq)]
pub struct CovGroupImage {
    /// The design-wide type index `new` finds the table by.
    pub type_index: u32,
    /// The checker site the table belongs to (`0` outside a checker).
    pub site: u32,
    pub instance: InstanceId,
    pub decl: crate::covergroup::decl::CovGroupDecl,
    /// The `vj_cov_*` kernels (`CovKernelFn`), by id.
    pub kernels: Vec<u32>,
    pub sampler: Option<CovSamplerImage>,
    /// The per-object clocking event of a class-embedded covergroup.
    pub class_clock: Option<CovClassClockImage>,
    /// The block events (19.3 `@@(begin f)` / `@@(end f)`) that sample this
    /// covergroup, as the keys the subroutine's code passes to the runtime.
    pub blocks: Vec<u64>,
}

/// Everything verification-related a design image carries.
#[derive(Clone, Debug, Default, PartialEq)]
pub struct VerifImage {
    pub assertions: Vec<AssertionImage>,
    pub free_groups: Vec<FreeGroupImage>,
    pub sampled: Vec<SampledImage>,
    /// In registration order: instance by instance, each instance's blocks in
    /// declaration order.
    pub clocking: Vec<ClockingImage>,
    /// In table order: the index the runtime assigns a table is its position.
    pub covergroups: Vec<CovGroupImage>,
}

impl VerifImage {
    /// Whether the design has nothing to verify at run time.
    pub fn is_empty(&self) -> bool {
        let VerifImage {
            assertions,
            free_groups,
            sampled,
            clocking,
            covergroups,
        } = self;
        assertions.is_empty()
            && free_groups.is_empty()
            && sampled.is_empty()
            && clocking.is_empty()
            && covergroups.is_empty()
    }
}