Struct SvaTranslator 

pub struct SvaTranslator {
    pub bound: u32,
    /* private fields */
}

Translator that converts SvaExpr to bounded timestep verification IR.

Fields

bound: u32

Implementations

impl SvaTranslator

pub fn new(bound: u32) -> Self

pub fn translate(&mut self, expr: &SvaExpr, t: u32) -> BoundedExpr

Translate an SVA expression at a specific timestep.

pub fn translate_sequence( &mut self, expr: &SvaExpr, t: u32, ) -> Vec<SequenceMatch>

Translate an SvaExpr as a SEQUENCE, returning all possible match endpoints.

Unlike translate() which returns a single BoundedExpr, this returns the set of (condition, length) pairs representing all possible matches. This is the foundation for proper IEEE 1800 sequence-level operators:

• SequenceAnd: both match, composite at max endpoint
• SequenceOr: union of match sets
• Intersect: both match at SAME length
• first_match: only shortest match
• throughout / within: desugared via intersect

pub fn translate_property(&mut self, expr: &SvaExpr) -> TranslateResult

Translate a top-level SVA property: conjoin over all timesteps [0, bound). This models G(property) — the property must hold at every reachable state.

pub fn translate_directive( &mut self, directive: &SvaDirective, ) -> DirectiveResult

Translate a concurrent assertion directive (IEEE 16.14).

Returns a DirectiveResult with the translated expression and the directive’s semantic role (check, constraint, or reachability query).