Struct EngineConfig 

pub struct EngineConfig {

    pub ir: PropertyIr,
    pub kind: AssertKind,
    pub n_clocks: usize,
    pub leaf_reads: Vec<Vec<LocalVarId>>,
    pub leaf_writes: Vec<Option<LocalVarId>>,
    pub activated: bool,
    pub captured: Vec<LocalVarId>,
    pub disable_mixed: bool,
    pub history_depth: usize,
    pub hist_clocks: usize,
    pub future: bool,
    pub future_clock: u32,
    pub live_history: bool,
    pub tick_history: bool,
}

Everything the engine needs to know about one assertion.

Fields

ir: PropertyIr

kind: AssertKind

n_clocks: usize

The number of distinct clocks of the assertion.

leaf_reads: Vec<Vec<LocalVarId>>

Per leaf, the local variables its expression reads (each must be assigned when the leaf is evaluated, 16.10).

leaf_writes: Vec<Option<LocalVarId>>

Per leaf, the local variable a PLAIN assignment match item (v = e) writes: the kernel is handed its frame slot but the variable need not be assigned yet (the item is what assigns it).

activated: bool

A procedural concurrent assertion (16.14.6) instead of a static one: its attempts start only for instances queued with Engine::activate, not at every tick.

captured: Vec<LocalVarId>

The automaton local-variable slot of each value an instance captures (Engine::activate’s values, same order). Assigned when the attempt starts, so the leaves that read the captured items find them.

disable_mixed: bool

The disable iff condition reads captured values AND signals (16.12, 16.14.6.1). The condition is not a constant of the attempt, nor a pure signal: the engine evaluates it against the live signals once per distinct tuple of captured values (Host::live_with) and each attempt reads the record of its own tuple.

history_depth: usize

How many previous clock ticks’ rows a position carries behind its own (0: just the row). The sampled value functions of an assertion read them (16.9.3): $rose/$fell/$stable/$changed the previous tick’s, $past(x, n) the n-th previous. A position’s row handed to Host::leaf is then (1 + history_depth) * row_len entries long, the tick’s own sampled row first, then the row of the previous tick, then the one before it, and so on. Before the first tick the previous rows are the initial row (16.5.1: the default sampled value is the initial one). Only a single-clock assertion has such a history: with several clocks the positions are the union of the clocks’ ticks, not any one clock’s.

hist_clocks: usize

How many clocks past the assertion’s own EngineConfig::n_clocks the host also tells the ticks of (Host::clock_ticked is asked for clocks n_clocks..n_clocks + hist_clocks too). They have a history block in a position’s row like any clock but start no attempt and make no position: they are the clocking events ($past(x, 1, , @(posedge fclk))), gated events ($past(x, 2, en)) and global clock ($rose_gclk(x)) of the sampled value functions that are not the clock of their own leaf (16.9.3, 16.9.4).

future: bool

The property calls a global clocking future sampled value function (16.9.4): a position’s row carries, after its history, the sampled row of the NEXT tick of EngineConfig::future_clock (the global clock) strictly after the position’s time step. A position is therefore held back until that tick arrives, so every verdict, and the action it runs, comes at the global clock tick that follows the attempt’s end, as the LRM requires; the attempt’s interval is unchanged.

future_clock: u32

With EngineConfig::future: the global clock, one of the assertion’s clocks or one of its history-only ones.

live_history: bool

A live leaf (the disable iff condition, an asynchronous abort condition) reads sampled values: Host::live is handed the position-shaped row of the current time step, the step’s sampled row followed by every clock’s history (16.12, 16.9.3: $sampled(x) and $rose(x, @ev) in a disable condition are meaningful since the condition itself is not sampled).

tick_history: bool

A clocking event’s iff condition calls a sampled value function (16.9.3: legal when explicitly clocked): Host::clock_ticked is handed the position-shaped row of the step (Engine::tick_row), the step’s sampled row followed by every clock’s history as of before this step’s ticks, instead of the sampled row alone.

Trait Implementations

impl Clone for EngineConfig

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.