vj_sim/sched/proc_assert.rs
1//! The procedural assertion queue of a concurrent assertion statement placed
2//! inside a procedure (LRM 1800-2023 16.14.6).
3//!
4//! When a process reaches `assert property (...)` the instance is not
5//! evaluated there: it is placed in the process's *procedural assertion queue*
6//! with the values the statement captures at that point (the current value of
7//! every automatic variable the assertion uses and of every `const'(expr)`,
8//! 16.14.6.1). In each Observed region the pending instances *mature*
9//! (16.14.6): the assertion engine drains this queue, and an instance whose
10//! leading clock ticked in the step starts an evaluation attempt at once, any
11//! other waits for the next tick.
12//!
13//! A pending instance is discarded when its process reaches a flush point
14//! (16.14.6.2): the process resumes from an event control or `wait`, an
15//! `always_comb`/`always_latch` is re-triggered, or the process's outermost
16//! scope is disabled. The kernel adapter's resume hook calls [`flush`] right
17//! next to the deferred-immediate flush; a `disable` statement reaches the queue
18//! through [`real_sv_rt_proc_assert_disable`], which clears the instances of the
19//! assertions it names (16.14.6.4: `disable <assertion label>`, or every
20//! assertion of the disabled outermost scope). Only pending instances are
21//! affected: a matured attempt has left this queue.
22//!
23//! The queue is thread-local, like the rest of the scheduler's run state.
24
25use std::cell::RefCell;
26use std::collections::HashMap;
27
28use crate::sched::assert_control::{self, SiteId};
29use crate::sched::{ProcessId, current_process};
30
31/// One queued instance.
32#[derive(Clone, Debug, PartialEq, Eq)]
33pub struct Entry {
34 /// The queueing process (`None`: no scheduler process was running).
35 pub process: Option<ProcessId>,
36 /// The assertion the instance belongs to (the plan index of its action
37 /// kernel).
38 pub key: u64,
39 /// The captured values, in capture-item order.
40 pub values: Vec<i64>,
41}
42
43thread_local! {
44 static QUEUE: RefCell<Vec<Entry>> = const { RefCell::new(Vec::new()) };
45 /// The assertion control site ([`crate::sched::assert_control`]) of each
46 /// procedural assertion, by plan index: `$assertoff` and `$assertkill` stop
47 /// its instances from being queued (20.11), `$assertkill` also empties
48 /// the queue of them.
49 static SITES: RefCell<HashMap<i64, SiteId>> = RefCell::new(HashMap::new());
50 /// The scheduler process of each plan that is one ([`register_process`]).
51 static PROCESSES: RefCell<HashMap<i64, ProcessId>> = RefCell::new(HashMap::new());
52}
53
54/// Set in a `disable` key (`sv_rt_proc_assert_disable`) that names a whole
55/// process rather than a procedural assertion: the low bits are the process's
56/// plan index ([`register_process`]). Disabling a process's outermost scope also
57/// flushes its deferred assertion report queue (LRM 16.4.4).
58pub const PROCESS_KEY_FLAG: i64 = 1 << 40;
59
60/// Declares `pid` as the scheduler process of plan `plan_index`, so that a
61/// `disable` of its outermost scope reaches its deferred report queue.
62pub fn register_process(plan_index: i64, pid: ProcessId) {
63 PROCESSES.with(|p| p.borrow_mut().insert(plan_index, pid));
64}
65
66/// Declares `site` as the control site of the procedural assertion `key`.
67pub fn register_site(key: i64, site: SiteId) {
68 SITES.with(|s| s.borrow_mut().insert(key, site));
69}
70
71/// Drops the pending instances of the assertions registered for any of `sites`
72/// (`$assertkill`, 20.11: "pending procedural assertion instances ... are
73/// flushed").
74pub(crate) fn clear_sites(sites: &[SiteId]) {
75 let keys: Vec<i64> = SITES.with(|s| {
76 s.borrow()
77 .iter()
78 .filter(|(_, site)| sites.contains(site))
79 .map(|(k, _)| *k)
80 .collect()
81 });
82 clear(&keys);
83}
84
85/// `void sv_rt_proc_assert(i64 key, ptr values, i64 n)`: the running process
86/// reached the procedural concurrent assertion `key` with the `n` captured
87/// values at `values`.
88///
89/// # Safety
90/// `values` points at `n` readable `i64`s (or `n` is 0).
91#[cfg_attr(feature = "aot-exports", unsafe(export_name = "sv_rt_proc_assert"))]
92pub unsafe extern "C" fn real_sv_rt_proc_assert(key: i64, values: *const i64, n: i64) {
93 // 20.11: an assertion that is off queues no new instance.
94 if let Some(site) = SITES.with(|s| s.borrow().get(&key).copied())
95 && !assert_control::state(site).checking
96 {
97 return;
98 }
99 let values = if n <= 0 || values.is_null() {
100 Vec::new()
101 } else {
102 // SAFETY: the caller's contract.
103 unsafe { std::slice::from_raw_parts(values, n as usize) }.to_vec()
104 };
105 let process = current_process();
106 QUEUE.with(|q| {
107 q.borrow_mut().push(Entry {
108 process,
109 key: key as u64,
110 values,
111 });
112 });
113}
114
115/// Discards `proc`'s pending instances (it reached a flush point).
116pub(crate) fn flush(proc: ProcessId) {
117 QUEUE.with(|q| q.borrow_mut().retain(|e| e.process != Some(proc)));
118}
119
120/// `void sv_rt_proc_assert_disable(ptr keys, i64 n)`: `disable` of procedural
121/// concurrent assertions (16.14.6.4) -- of one by its label, or of the outermost
122/// scope of the process they are in, in which case the pending queue is flushed.
123/// Clears the pending instances of the `n` assertions `keys` names (the plan
124/// indices of [`real_sv_rt_proc_assert`]'s `key`). An instance that already
125/// matured is not in the queue: "once a procedural concurrent assertion
126/// evaluation attempt has matured, it shall not be impacted by any disable".
127///
128/// # Safety
129/// `keys` points at `n` readable `i64`s (or `n` is 0).
130#[cfg_attr(
131 feature = "aot-exports",
132 unsafe(export_name = "sv_rt_proc_assert_disable")
133)]
134pub unsafe extern "C" fn real_sv_rt_proc_assert_disable(keys: *const i64, n: i64) {
135 if n <= 0 || keys.is_null() {
136 return;
137 }
138 // SAFETY: the caller's contract.
139 let keys = unsafe { std::slice::from_raw_parts(keys, n as usize) };
140 clear(keys);
141 // 16.4.4: the outermost scope of a process with a deferred assertion report
142 // queue: the queue is flushed.
143 for k in keys.iter().filter(|k| **k & PROCESS_KEY_FLAG != 0) {
144 if let Some(pid) = PROCESSES.with(|p| p.borrow().get(&(*k & !PROCESS_KEY_FLAG)).copied()) {
145 crate::sched::deferred::flush_deferred(pid);
146 }
147 }
148}
149
150/// Drops every pending instance of the assertions `keys`.
151pub(crate) fn clear(keys: &[i64]) {
152 QUEUE.with(|q| q.borrow_mut().retain(|e| !keys.contains(&(e.key as i64))));
153}
154
155/// Takes every pending instance, in queueing order: they mature.
156pub fn drain() -> Vec<Entry> {
157 QUEUE.with(|q| std::mem::take(&mut *q.borrow_mut()))
158}
159
160/// Whether any instance is pending.
161pub fn is_empty() -> bool {
162 QUEUE.with(|q| q.borrow().is_empty())
163}
164
165/// Forgets every pending instance (the start of a run).
166pub fn reset() {
167 QUEUE.with(|q| q.borrow_mut().clear());
168 SITES.with(|s| s.borrow_mut().clear());
169 PROCESSES.with(|p| p.borrow_mut().clear());
170}
171
172thread_local! {
173 static INPUTS: RefCell<Vec<i64>> = const { RefCell::new(Vec::new()) };
174}
175
176/// Sets the captured values the action kernel about to run reads through
177/// [`real_sv_rt_assert_input`]: the attempt's own, captured when its instance
178/// was queued (16.14.6.1: the action block sees them, not the live values).
179pub fn set_action_inputs(values: Vec<i64>) {
180 INPUTS.with(|i| *i.borrow_mut() = values);
181}
182
183/// `i64 sv_rt_assert_input(i64 k)`: the `k`th captured value of the attempt
184/// whose action block is running (0 outside one).
185#[cfg_attr(feature = "aot-exports", unsafe(export_name = "sv_rt_assert_input"))]
186pub extern "C" fn real_sv_rt_assert_input(k: i64) -> i64 {
187 INPUTS.with(|i| i.borrow().get(k as usize).copied().unwrap_or(0))
188}