vj-sim 0.3.0

//! The procedural assertion queue of a concurrent assertion statement placed
//! inside a procedure (LRM 1800-2023 16.14.6).
//!
//! When a process reaches `assert property (...)` the instance is not
//! evaluated there: it is placed in the process's *procedural assertion queue*
//! with the values the statement captures at that point (the current value of
//! every automatic variable the assertion uses and of every `const'(expr)`,
//! 16.14.6.1). In each Observed region the pending instances *mature*
//! (16.14.6): the assertion engine drains this queue, and an instance whose
//! leading clock ticked in the step starts an evaluation attempt at once, any
//! other waits for the next tick.
//!
//! A pending instance is discarded when its process reaches a flush point
//! (16.14.6.2): the process resumes from an event control or `wait`, an
//! `always_comb`/`always_latch` is re-triggered, or the process's outermost
//! scope is disabled. The kernel adapter's resume hook calls [`flush`] right
//! next to the deferred-immediate flush; a `disable` statement reaches the queue
//! through [`real_sv_rt_proc_assert_disable`], which clears the instances of the
//! assertions it names (16.14.6.4: `disable <assertion label>`, or every
//! assertion of the disabled outermost scope). Only pending instances are
//! affected: a matured attempt has left this queue.
//!
//! The queue is thread-local, like the rest of the scheduler's run state.

use std::cell::RefCell;
use std::collections::HashMap;

use crate::sched::assert_control::{self, SiteId};
use crate::sched::{ProcessId, current_process};

/// One queued instance.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Entry {
    /// The queueing process (`None`: no scheduler process was running).
    pub process: Option<ProcessId>,
    /// The assertion the instance belongs to (the plan index of its action
    /// kernel).
    pub key: u64,
    /// The captured values, in capture-item order.
    pub values: Vec<i64>,
}

thread_local! {
    static QUEUE: RefCell<Vec<Entry>> = const { RefCell::new(Vec::new()) };
    /// The assertion control site ([`crate::sched::assert_control`]) of each
    /// procedural assertion, by plan index: `$assertoff` and `$assertkill` stop
    /// its instances from being queued (20.11), `$assertkill` also empties
    /// the queue of them.
    static SITES: RefCell<HashMap<i64, SiteId>> = RefCell::new(HashMap::new());
    /// The scheduler process of each plan that is one ([`register_process`]).
    static PROCESSES: RefCell<HashMap<i64, ProcessId>> = RefCell::new(HashMap::new());
}

/// Set in a `disable` key (`sv_rt_proc_assert_disable`) that names a whole
/// process rather than a procedural assertion: the low bits are the process's
/// plan index ([`register_process`]). Disabling a process's outermost scope also
/// flushes its deferred assertion report queue (LRM 16.4.4).
pub const PROCESS_KEY_FLAG: i64 = 1 << 40;

/// Declares `pid` as the scheduler process of plan `plan_index`, so that a
/// `disable` of its outermost scope reaches its deferred report queue.
pub fn register_process(plan_index: i64, pid: ProcessId) {
    PROCESSES.with(|p| p.borrow_mut().insert(plan_index, pid));
}

/// Declares `site` as the control site of the procedural assertion `key`.
pub fn register_site(key: i64, site: SiteId) {
    SITES.with(|s| s.borrow_mut().insert(key, site));
}

/// Drops the pending instances of the assertions registered for any of `sites`
/// (`$assertkill`, 20.11: "pending procedural assertion instances ... are
/// flushed").
pub(crate) fn clear_sites(sites: &[SiteId]) {
    let keys: Vec<i64> = SITES.with(|s| {
        s.borrow()
            .iter()
            .filter(|(_, site)| sites.contains(site))
            .map(|(k, _)| *k)
            .collect()
    });
    clear(&keys);
}

/// `void sv_rt_proc_assert(i64 key, ptr values, i64 n)`: the running process
/// reached the procedural concurrent assertion `key` with the `n` captured
/// values at `values`.
///
/// # Safety
/// `values` points at `n` readable `i64`s (or `n` is 0).
#[cfg_attr(feature = "aot-exports", unsafe(export_name = "sv_rt_proc_assert"))]
pub unsafe extern "C" fn real_sv_rt_proc_assert(key: i64, values: *const i64, n: i64) {
    // 20.11: an assertion that is off queues no new instance.
    if let Some(site) = SITES.with(|s| s.borrow().get(&key).copied())
        && !assert_control::state(site).checking
    {
        return;
    }
    let values = if n <= 0 || values.is_null() {
        Vec::new()
    } else {
        // SAFETY: the caller's contract.
        unsafe { std::slice::from_raw_parts(values, n as usize) }.to_vec()
    };
    let process = current_process();
    QUEUE.with(|q| {
        q.borrow_mut().push(Entry {
            process,
            key: key as u64,
            values,
        });
    });
}

/// Discards `proc`'s pending instances (it reached a flush point).
pub(crate) fn flush(proc: ProcessId) {
    QUEUE.with(|q| q.borrow_mut().retain(|e| e.process != Some(proc)));
}

/// `void sv_rt_proc_assert_disable(ptr keys, i64 n)`: `disable` of procedural
/// concurrent assertions (16.14.6.4) -- of one by its label, or of the outermost
/// scope of the process they are in, in which case the pending queue is flushed.
/// Clears the pending instances of the `n` assertions `keys` names (the plan
/// indices of [`real_sv_rt_proc_assert`]'s `key`). An instance that already
/// matured is not in the queue: "once a procedural concurrent assertion
/// evaluation attempt has matured, it shall not be impacted by any disable".
///
/// # Safety
/// `keys` points at `n` readable `i64`s (or `n` is 0).
#[cfg_attr(
    feature = "aot-exports",
    unsafe(export_name = "sv_rt_proc_assert_disable")
)]
pub unsafe extern "C" fn real_sv_rt_proc_assert_disable(keys: *const i64, n: i64) {
    if n <= 0 || keys.is_null() {
        return;
    }
    // SAFETY: the caller's contract.
    let keys = unsafe { std::slice::from_raw_parts(keys, n as usize) };
    clear(keys);
    // 16.4.4: the outermost scope of a process with a deferred assertion report
    // queue: the queue is flushed.
    for k in keys.iter().filter(|k| **k & PROCESS_KEY_FLAG != 0) {
        if let Some(pid) = PROCESSES.with(|p| p.borrow().get(&(*k & !PROCESS_KEY_FLAG)).copied()) {
            crate::sched::deferred::flush_deferred(pid);
        }
    }
}

/// Drops every pending instance of the assertions `keys`.
pub(crate) fn clear(keys: &[i64]) {
    QUEUE.with(|q| q.borrow_mut().retain(|e| !keys.contains(&(e.key as i64))));
}

/// Takes every pending instance, in queueing order: they mature.
pub fn drain() -> Vec<Entry> {
    QUEUE.with(|q| std::mem::take(&mut *q.borrow_mut()))
}

/// Whether any instance is pending.
pub fn is_empty() -> bool {
    QUEUE.with(|q| q.borrow().is_empty())
}

/// Forgets every pending instance (the start of a run).
pub fn reset() {
    QUEUE.with(|q| q.borrow_mut().clear());
    SITES.with(|s| s.borrow_mut().clear());
    PROCESSES.with(|p| p.borrow_mut().clear());
}

thread_local! {
    static INPUTS: RefCell<Vec<i64>> = const { RefCell::new(Vec::new()) };
}

/// Sets the captured values the action kernel about to run reads through
/// [`real_sv_rt_assert_input`]: the attempt's own, captured when its instance
/// was queued (16.14.6.1: the action block sees them, not the live values).
pub fn set_action_inputs(values: Vec<i64>) {
    INPUTS.with(|i| *i.borrow_mut() = values);
}

/// `i64 sv_rt_assert_input(i64 k)`: the `k`th captured value of the attempt
/// whose action block is running (0 outside one).
#[cfg_attr(feature = "aot-exports", unsafe(export_name = "sv_rt_assert_input"))]
pub extern "C" fn real_sv_rt_assert_input(k: i64) -> i64 {
    INPUTS.with(|i| i.borrow().get(k as usize).copied().unwrap_or(0))
}