Struct Automaton 

pub struct Automaton {
    pub states: Vec<State>,
    pub start: ThreadStateId,
    pub admits_empty: bool,
    pub first_match_groups: u32,
    pub local_vars: Vec<LocalVarDecl>,
    pub end_points: Vec<EndPoint>,
    pub entry_clock: ClockId,
}

A compiled automaton (plan §1.2’s “a dedicated, interpreted automaton per assertion, compiled once at elaboration time into a static transition table”) – one sequence/property tree’s whole static shape, addressed by ThreadStateId (an index into states), plus which state a freshly spawned thread starts in. Pure data, no sv-lang dependency (this module’s own doc comment), so it is equally usable by vj-codegen::sva::build (which constructs one from an AssertionExpr tree, under the frontend feature) and by the eventual vj-runtime::sva_engine (which only ever interprets an already-built one, with vj-sim’s frontend feature off, per this crate’s own default-features = false contract with vj-runtime).

Fields

states: Vec<State>

start: ThreadStateId

admits_empty: bool

true when the sequence this automaton was built from admits the EMPTY match (16.9.2.1: a match spanning zero clock ticks, e.g. a[*0], a[*0:2]). The empty match is not a path through states (a path always consumes at least the tick it starts on), so it cannot be an accepting state; this flag carries it separately. A sequence that admits the empty match and nothing else can never match when used as a property (16.9.2.1 “a sequence that admits only an empty match cannot be used as a property”); one that admits both matches on its non-empty paths only – consumers decide how to treat the empty match (T10 only records it; the property layers that care are T19+).

first_match_groups: u32

How many FirstMatchIds this automaton uses (0..first_match_groups): the size of the per-attempt first-match table the engine allocates (keyed by group and begin tick, see Transition::FirstMatchBegin).

local_vars: Vec<LocalVarDecl>

The local-variable slots (LocalVarId(i) is local_vars[i]): the size and element types of the per-thread frame the engine allocates, see LocalVarId. Every slot of every instance expansion has its own entry (a slot is never reused for a different variable), so the frame is as wide as the assertion’s total number of local-variable declarations plus the and/intersect shadows.

end_points: Vec<EndPoint>

The sequence instances whose end points this automaton tests (EndPointId(i) is end_points[i]), each a whole automaton of its own.

entry_clock: ClockId

The clock a thread is in at Automaton::start (sva T28): the clock of the sequence’s first Boolean operand. ClockId(0) unless the sequence opens with a clocking event of its own that is not the assertion’s.

Implementations

impl Automaton

pub fn empty() -> Self

An automaton with one (unreachable until wired) state and no edges – the empty table a builder starts folding states/edges into.

pub fn new_local_var(&mut self, width: u32, signed: bool) -> LocalVarId

Mints the next local variable, of the given integral type, and returns its (head) slot. A variable wider than 64 bits gets LocalVarDecl::slots consecutive slots: the head carries the declared type and value limb 0, the rest are plain 64-bit unsigned limb slots (value limbs 1.., then the unknown limbs), so everything that names a variable by its head slot (reads, copies, steps) reaches the others by position.

pub fn local_var(&self, id: LocalVarId) -> &LocalVarDecl

Borrows id’s declared type. id must be a slot this automaton minted (see Automaton::add_edge’s identical note).

pub fn new_end_point(&mut self, point: EndPoint) -> EndPointId

Registers a sequence instance whose end point this automaton tests.

pub fn end_point(&self, id: EndPointId) -> &EndPoint

Borrows id’s instance (an id this automaton minted, like Automaton::local_var).

pub fn new_first_match_group(&mut self) -> FirstMatchId

Mints the next FirstMatchId (one per first_match region).

pub fn new_state(&mut self) -> ThreadStateId

Allocates a fresh state with no outgoing edges and returns its id.

pub fn add_edge( &mut self, from: ThreadStateId, guard: Option<LeafId>, label: Transition, target: ThreadStateId, )

Appends one edge to from’s row. from must be a state this same Automaton has already allocated (via Automaton::new_state) – out-of-range ids panic (a builder-internal invariant, never reachable from untrusted input: every ThreadStateId this crate’s builder ever hands to this method came from this same Automaton’s own new_state, per the one caller that exists today, vj-codegen::sva::build).

pub fn state(&self, id: ThreadStateId) -> &State

Borrows id’s row.

pub fn max_span(&self) -> Option<u32>

An upper bound on how many clock ticks past its start tick any match of this automaton can end: the sum of every delay edge’s upper bound (a simple path takes each edge at most once, and a repetition is already unrolled into delay edges), or None when some delay is unbounded (##[1:$], [*]) or a Transition::ClockSync / end-point edge makes the span a function of another clock. A cover-sequence attempt (16.14.3) that has run this long has reported every match it ever will.

pub fn end_point_lookback(&self) -> Vec<(ClockId, Option<u32>)>

For every sequence instance this automaton (or an instance of it) tests: its clock, and how many of that clock’s ticks before a testing thread’s position an attempt of it may have started and still end there (None for an instance with no bounded span, an unbounded repetition: its status needs every past start).

pub fn has_calls(&self) -> bool

Whether any edge of this automaton (not of its end-point instances, see Automaton::end_points_have_calls) attaches a subroutine call (16.11).

pub fn end_points_have_calls(&self) -> bool

Whether a sequence instance an end-point method tests (at any depth) attaches a subroutine call.

Trait Implementations

impl Clone for Automaton

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Automaton

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for Automaton

impl PartialEq for Automaton

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for Automaton