Module proc_assert 

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.

Structs

Entry

One queued instance.

Constants

PROCESS_KEY_FLAG

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).

Functions

drain

Takes every pending instance, in queueing order: they mature.

is_empty

Whether any instance is pending.

real_sv_rt_assert_input

i64 sv_rt_assert_input(i64 k): the kth captured value of the attempt whose action block is running (0 outside one).

real_sv_rt_proc_assert^⚠

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.

real_sv_rt_proc_assert_disable^⚠

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”.

register_process

Declares pid as the scheduler process of plan plan_index, so that a disable of its outermost scope reaches its deferred report queue.

register_site

Declares site as the control site of the procedural assertion key.

reset

Forgets every pending instance (the start of a run).

set_action_inputs

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).