Struct Engine 

pub struct Engine { /* private fields */ }

One assertion’s runtime state. A clone evaluates a step without touching the original (a trial run, e.g. a checker’s solution attempt, 17.7.2).

Implementations

impl Engine

pub fn sampled_row(&self) -> &[u128]

The row this step’s tick samples: the previous step’s final values.

pub fn tick_row(&self) -> Cow<'_, [u128]>

The row Host::clock_ticked reads (see EngineConfig::tick_history): the sampled row, or with a history-reading clocking event the position row.

pub fn set_sampled_words(&mut self, words: &[(usize, u128)])

Overrides words of the sampled row with their current values: an active free checker variable’s sampled value is its current one (17.7.2).

pub fn new( cfg: EngineConfig, initial_row: Vec<u128>, ) -> Result<Self, EngineError>

pub fn set_checking(&mut self, on: bool)

$asserton/$assertoff (20.11): whether a static assertion starts new attempts. A procedural one starts attempts only for instances that matured (Engine::activate); whether an instance is queued at all is decided where it is queued, so the flag does not hold back an instance already waiting for its clock.

pub fn set_action_flags(&mut self, flags: u32)

The action flags attempts started from now on carry (see Event::flags).

pub fn kill(&mut self)

$assertkill (20.11): aborts every executing attempt – they report nothing and run no action – and drops the matured instances still waiting to start. The statistics keep what they counted.

pub fn kind(&self) -> AssertKind

pub fn stats(&self) -> Stats

pub fn live_set(&self) -> &[LeafId]

The live leaves the host must be able to answer Host::live for.

pub fn end_of_step(&mut self, row: Vec<u128>)

The signal row of the end of the time step that just finished: the sampled values of the next one.

pub fn end_of_step_with(&mut self, fill: impl FnOnce(&mut [u128]))

Self::end_of_step that has fill write the row in place (over zeros), which saves the allocation of a row per step.

pub fn activate(&mut self, now: u64, values: Vec<i64>)

A procedural concurrent assertion instance matured in the Observed region of time step now (16.14.6), with the values it captured when the procedure reached it. When the leading clock ticked in this very step its attempt begins at once; otherwise the instance waits for the next tick. Call it before Engine::fire of the same step.

pub fn activate_tagged(&mut self, now: u64, values: Vec<i64>, tag: u64)

Engine::activate with a tag the attempt’s Events carry back.

An AssertKind::Expect instance never starts in the step it was activated in, whether or not the leading clock ticked there: its first evaluation is on the subsequent clocking event (16.17).

pub fn live_tuples(&self) -> usize

The number of captured-value tuples whose disable iff value the engine records (see EngineConfig::disable_mixed); bounded by the live instances, which a long run’s test observes.

pub fn set_step(&mut self, id: u64, on: bool)

The Observed-region step at simulation time now. Returns the outcomes decided by it, in attempt-start order. Discards the attempt with ordinal id (VPI vpiAssertionKill, 39.5.2): it reports nothing; the assertion stays enabled. Whether it was pending. Turns step reporting for attempt id on or off (39.5.2 vpiAssertionEnableStep/vpiAssertionDisableStep). Reported steps are collected by Engine::take_steps.

pub fn set_step_new(&mut self, on: bool)

Whether every attempt that starts from now on has its steps reported (39.5.2: stepping requested for an attempt start time not reached yet). The caller turns it off again after the time step.

pub fn set_fail_leaf(&mut self, on: bool)

Whether a failure records the leaf it failed on (Engine::take_fail_leaves).

pub fn take_started(&mut self) -> Vec<(u64, u64)>

With EngineConfig::future: the start times of the attempts started since the last call, by attempt ordinal (empty otherwise).

pub fn take_steps(&mut self) -> Vec<StepRecord>

The steps reported since the last call.

pub fn take_fail_leaves(&mut self) -> Vec<(u64, Option<LeafId>)>

The failures reported since the last call with the leaf each failed on (None when it read none), by attempt ordinal.

pub fn kill_attempt(&mut self, id: u64) -> bool

pub fn disabled_attempts(&self) -> &[(u64, Option<u64>)]

The ordinals of the attempts the last Engine::fire found disabled.

pub fn fire( &mut self, host: &dyn Host, now: u64, ) -> Result<Vec<Event>, TraceError>

Trait Implementations

impl Clone for Engine

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.