Enum SvaExpr 

pub enum SvaExpr {
    Signal(String),
    Const(u64, u32),
    Rose(Box<SvaExpr>),
    Fell(Box<SvaExpr>),
    Past(Box<SvaExpr>, u32),
    And(Box<SvaExpr>, Box<SvaExpr>),
    Or(Box<SvaExpr>, Box<SvaExpr>),
    Not(Box<SvaExpr>),
    Eq(Box<SvaExpr>, Box<SvaExpr>),
    Implication {
        antecedent: Box<SvaExpr>,
        consequent: Box<SvaExpr>,
        overlapping: bool,
    },
    Delay {
        body: Box<SvaExpr>,
        min: u32,
        max: Option<u32>,
    },
    Repetition {
        body: Box<SvaExpr>,
        min: u32,
        max: Option<u32>,
    },
    SEventually(Box<SvaExpr>),
    SAlways(Box<SvaExpr>),
    Stable(Box<SvaExpr>),
    Changed(Box<SvaExpr>),
    DisableIff {
        condition: Box<SvaExpr>,
        body: Box<SvaExpr>,
    },
    Nexttime(Box<SvaExpr>, u32),
    IfElse {
        condition: Box<SvaExpr>,
        then_expr: Box<SvaExpr>,
        else_expr: Box<SvaExpr>,
    },
    NotEq(Box<SvaExpr>, Box<SvaExpr>),
    LessThan(Box<SvaExpr>, Box<SvaExpr>),
    GreaterThan(Box<SvaExpr>, Box<SvaExpr>),
    LessEqual(Box<SvaExpr>, Box<SvaExpr>),
    GreaterEqual(Box<SvaExpr>, Box<SvaExpr>),
    Ternary {
        condition: Box<SvaExpr>,
        then_expr: Box<SvaExpr>,
        else_expr: Box<SvaExpr>,
    },
    Throughout {
        signal: Box<SvaExpr>,
        sequence: Box<SvaExpr>,
    },
    Within {
        inner: Box<SvaExpr>,
        outer: Box<SvaExpr>,
    },
    FirstMatch(Box<SvaExpr>),
    Intersect {
        left: Box<SvaExpr>,
        right: Box<SvaExpr>,
    },
    OneHot0(Box<SvaExpr>),
    OneHot(Box<SvaExpr>),
    CountOnes(Box<SvaExpr>),
    IsUnknown(Box<SvaExpr>),
    Sampled(Box<SvaExpr>),
    Bits(Box<SvaExpr>),
    Clog2(Box<SvaExpr>),
    CountBits(Box<SvaExpr>, Vec<char>),
    IsUnbounded(Box<SvaExpr>),
    GotoRepetition {
        body: Box<SvaExpr>,
        count: u32,
    },
    NonConsecRepetition {
        body: Box<SvaExpr>,
        min: u32,
        max: Option<u32>,
    },
    AcceptOn {
        condition: Box<SvaExpr>,
        body: Box<SvaExpr>,
    },
    RejectOn {
        condition: Box<SvaExpr>,
        body: Box<SvaExpr>,
    },
    PropertyNot(Box<SvaExpr>),
    PropertyImplies(Box<SvaExpr>, Box<SvaExpr>),
    PropertyIff(Box<SvaExpr>, Box<SvaExpr>),
    Always(Box<SvaExpr>),
    AlwaysBounded {
        body: Box<SvaExpr>,
        min: u32,
        max: Option<u32>,
    },
    SAlwaysBounded {
        body: Box<SvaExpr>,
        min: u32,
        max: u32,
    },
    EventuallyBounded {
        body: Box<SvaExpr>,
        min: u32,
        max: u32,
    },
    SEventuallyBounded {
        body: Box<SvaExpr>,
        min: u32,
        max: Option<u32>,
    },
    Until {
        lhs: Box<SvaExpr>,
        rhs: Box<SvaExpr>,
        strong: bool,
        inclusive: bool,
    },
    Strong(Box<SvaExpr>),
    Weak(Box<SvaExpr>),
    SNexttime(Box<SvaExpr>, u32),
    FollowedBy {
        antecedent: Box<SvaExpr>,
        consequent: Box<SvaExpr>,
        overlapping: bool,
    },
    PropertyCase {
        expression: Box<SvaExpr>,
        items: Vec<(Vec<SvaExpr>, Box<SvaExpr>)>,
        default: Option<Box<SvaExpr>>,
    },
    SyncAcceptOn {
        condition: Box<SvaExpr>,
        body: Box<SvaExpr>,
    },
    SyncRejectOn {
        condition: Box<SvaExpr>,
        body: Box<SvaExpr>,
    },
    SequenceAnd(Box<SvaExpr>, Box<SvaExpr>),
    SequenceOr(Box<SvaExpr>, Box<SvaExpr>),
    ImmediateAssert {
        expression: Box<SvaExpr>,
        deferred: Option<ImmediateDeferred>,
    },
    FieldAccess {
        signal: Box<SvaExpr>,
        field: String,
    },
    EnumLiteral {
        type_name: Option<String>,
        value: String,
    },
    Triggered(String),
    Matched(String),
    BitAnd(Box<SvaExpr>, Box<SvaExpr>),
    BitOr(Box<SvaExpr>, Box<SvaExpr>),
    BitXor(Box<SvaExpr>, Box<SvaExpr>),
    BitNot(Box<SvaExpr>),
    ReductionAnd(Box<SvaExpr>),
    ReductionOr(Box<SvaExpr>),
    ReductionXor(Box<SvaExpr>),
    BitSelect {
        signal: Box<SvaExpr>,
        index: Box<SvaExpr>,
    },
    PartSelect {
        signal: Box<SvaExpr>,
        high: u32,
        low: u32,
    },
    Concat(Vec<SvaExpr>),
    SequenceAction {
        expression: Box<SvaExpr>,
        assignments: Vec<(String, Box<SvaExpr>)>,
    },
    LocalVar(String),
    ConstCast(Box<SvaExpr>),
    Clocked {
        clock: String,
        edge: ClockEdge,
        body: Box<SvaExpr>,
    },
    ArrayMap {
        array: Box<SvaExpr>,
        iterator: String,
        with_expr: Box<SvaExpr>,
    },
    TypeThis,
    RealConst(f64),
}

SVA expression AST — models a useful subset of SystemVerilog Assertions.

Variants

Signal(String)

Signal reference: req, ack, data_out

Const(u64, u32)

Integer constant with bit width: 8'hFF

Rose(Box<SvaExpr>)

Rising edge: $rose(sig)

Fell(Box<SvaExpr>)

Falling edge: $fell(sig)

Past(Box<SvaExpr>, u32)

Past value: $past(sig, n)

And(Box<SvaExpr>, Box<SvaExpr>)

Conjunction: a && b

Or(Box<SvaExpr>, Box<SvaExpr>)

Disjunction: a || b

Not(Box<SvaExpr>)

Negation: !a

Eq(Box<SvaExpr>, Box<SvaExpr>)

Equality: a == b

Implication

SVA implication: a |-> b (overlapping) or a |=> b (non-overlapping)

Fields

antecedent: Box<SvaExpr>

consequent: Box<SvaExpr>

overlapping: bool

Delay

Delay: ##[min:max] body

Fields

body: Box<SvaExpr>

min: u32

max: Option<u32>

Repetition

Sequence repetition: body[*N] or body[*min:max]

Fields

body: Box<SvaExpr>

min: u32

max: Option<u32>

SEventually(Box<SvaExpr>)

Strong eventually: s_eventually(body)

SAlways(Box<SvaExpr>)

Strong always: s_always(body)

Stable(Box<SvaExpr>)

Stable: $stable(sig) — signal unchanged from previous cycle

Changed(Box<SvaExpr>)

Changed: $changed(sig) — signal changed from previous cycle

DisableIff

Disable condition: disable iff (cond) body

Fields

condition: Box<SvaExpr>

body: Box<SvaExpr>

Nexttime(Box<SvaExpr>, u32)

Next time: nexttime(body) or nexttime[N](body)

IfElse

Conditional property: if (cond) P else Q

Fields

condition: Box<SvaExpr>

then_expr: Box<SvaExpr>

else_expr: Box<SvaExpr>

NotEq(Box<SvaExpr>, Box<SvaExpr>)

Inequality: a != b

LessThan(Box<SvaExpr>, Box<SvaExpr>)

Less than: a < b

GreaterThan(Box<SvaExpr>, Box<SvaExpr>)

Greater than: a > b

LessEqual(Box<SvaExpr>, Box<SvaExpr>)

Less or equal: a <= b

GreaterEqual(Box<SvaExpr>, Box<SvaExpr>)

Greater or equal: a >= b

Ternary

Ternary: cond ? a : b

Fields

condition: Box<SvaExpr>

then_expr: Box<SvaExpr>

else_expr: Box<SvaExpr>

Throughout

Throughout: sig throughout seq — signal holds during entire sequence

Fields

signal: Box<SvaExpr>

sequence: Box<SvaExpr>

Within

Within: seq1 within seq2 — first sequence completes within second

Fields

inner: Box<SvaExpr>

outer: Box<SvaExpr>

FirstMatch(Box<SvaExpr>)

First match: first_match(seq) — matches at first completion

Intersect

Intersect: seq1 intersect seq2 — both sequences match with same length

Fields

left: Box<SvaExpr>

right: Box<SvaExpr>

OneHot0(Box<SvaExpr>)

At most one bit set: $onehot0(sig) — popcount ≤ 1

OneHot(Box<SvaExpr>)

Exactly one bit set: $onehot(sig) — popcount = 1

CountOnes(Box<SvaExpr>)

Population count: $countones(sig) — returns integer

IsUnknown(Box<SvaExpr>)

X/Z detection: $isunknown(sig) — always false in 2-state formal

Sampled(Box<SvaExpr>)

Sampled value: $sampled(sig) — identity in synchronous formal

Bits(Box<SvaExpr>)

Bit width: $bits(sig) — returns integer

Clog2(Box<SvaExpr>)

Ceiling log2: $clog2(val) — minimum bits to represent val

CountBits(Box<SvaExpr>, Vec<char>)

Generalized bit counting: $countbits(sig, '0', '1', ...) (IEEE 20.9)

IsUnbounded(Box<SvaExpr>)

Parameter bound check: $isunbounded(param) (IEEE 20.9)

GotoRepetition

Goto repetition: sig[->N] — N non-consecutive matches

Fields

body: Box<SvaExpr>

count: u32

NonConsecRepetition

Non-consecutive repetition: sig[=N] or sig[=min:max]

Fields

body: Box<SvaExpr>

min: u32

max: Option<u32>

AcceptOn

Accept on: accept_on(cond) body — property passes if cond true

Fields

condition: Box<SvaExpr>

body: Box<SvaExpr>

RejectOn

Reject on: reject_on(cond) body — property fails if cond true

Fields

condition: Box<SvaExpr>

body: Box<SvaExpr>

PropertyNot(Box<SvaExpr>)

Property negation: not property_expr (IEEE 16.12.3) Distinct from boolean ! — negates temporal property evaluation. Flips strength: not(weak) → strong, not(strong) → weak (IEEE 16.12.15).

PropertyImplies(Box<SvaExpr>, Box<SvaExpr>)

Property implication: p implies q (IEEE 16.12.8) Distinct from sequence |-> — property-level not p or q.

PropertyIff(Box<SvaExpr>, Box<SvaExpr>)

Property biconditional: p iff q (IEEE 16.12.8) Equivalent to (p implies q) and (q implies p).

Always(Box<SvaExpr>)

Weak unbounded always: always p (IEEE 16.12.11) Passes if trace ends (weak semantics).

AlwaysBounded

Weak bounded always: always [m:n] p (IEEE 16.12.11) max=None means $ (weak allows $).

Fields

body: Box<SvaExpr>

min: u32

max: Option<u32>

SAlwaysBounded

Strong bounded always: s_always [m:n] p (IEEE 16.12.11) All ticks must exist. NO $ allowed.

Fields

body: Box<SvaExpr>

min: u32

max: u32

EventuallyBounded

Weak bounded eventually: eventually [m:n] p (IEEE 16.12.13) Range must be bounded (no $).

Fields

body: Box<SvaExpr>

min: u32

max: u32

SEventuallyBounded

Strong bounded eventually: s_eventually [m:n] p (IEEE 16.12.13) CAN use $ (max=None means $).

Fields

body: Box<SvaExpr>

min: u32

max: Option<u32>

Until

Until operator with 4 variants (IEEE 16.12.12): p until q (weak, non-overlapping) p s_until q (strong, non-overlapping) p until_with q (weak, overlapping) p s_until_with q (strong, overlapping)

Fields

lhs: Box<SvaExpr>

rhs: Box<SvaExpr>

strong: bool

inclusive: bool

Strong(Box<SvaExpr>)

Strong sequence: strong(seq) (IEEE 16.12.2) — match must exist within bound

Weak(Box<SvaExpr>)

Weak sequence: weak(seq) (IEEE 16.12.2) — no match needed if bound exhausted

SNexttime(Box<SvaExpr>, u32)

Strong nexttime: s_nexttime(body) or s_nexttime[N](body) (IEEE 16.12.10)

FollowedBy

Followed-by: seq #-# prop (overlapping) or seq #=# prop (non-overlapping) (IEEE 16.12.9)

Fields

antecedent: Box<SvaExpr>

consequent: Box<SvaExpr>

overlapping: bool

PropertyCase

Property case: case(expr) val: prop; ... default: prop; endcase (IEEE 16.12.16)

Fields

expression: Box<SvaExpr>

items: Vec<(Vec<SvaExpr>, Box<SvaExpr>)>

default: Option<Box<SvaExpr>>

SyncAcceptOn

Synchronous accept abort: sync_accept_on(cond) body (IEEE 16.12.14)

Fields

condition: Box<SvaExpr>

body: Box<SvaExpr>

SyncRejectOn

Synchronous reject abort: sync_reject_on(cond) body (IEEE 16.12.14)

Fields

condition: Box<SvaExpr>

body: Box<SvaExpr>

SequenceAnd(Box<SvaExpr>, Box<SvaExpr>)

Sequence AND: both operands match, composite ends at whichever finishes last

SequenceOr(Box<SvaExpr>, Box<SvaExpr>)

Sequence OR: at least one matches, composite match set is union

ImmediateAssert

Immediate assertion: assert(expr), assert #0(expr), assert final(expr)

Fields

expression: Box<SvaExpr>

deferred: Option<ImmediateDeferred>

FieldAccess

Field access: req.addr or req.header.id

Fields

signal: Box<SvaExpr>

field: String

EnumLiteral

Enum literal: ST_READ or state_t::READ

Fields

type_name: Option<String>

value: String

Triggered(String)

Triggered endpoint: seq_name.triggered

Matched(String)

Matched endpoint: seq_name.matched

BitAnd(Box<SvaExpr>, Box<SvaExpr>)

BitOr(Box<SvaExpr>, Box<SvaExpr>)

BitXor(Box<SvaExpr>, Box<SvaExpr>)

BitNot(Box<SvaExpr>)

ReductionAnd(Box<SvaExpr>)

ReductionOr(Box<SvaExpr>)

ReductionXor(Box<SvaExpr>)

BitSelect

Fields

signal: Box<SvaExpr>

index: Box<SvaExpr>

PartSelect

Fields

signal: Box<SvaExpr>

high: u32

low: u32

Concat(Vec<SvaExpr>)

SequenceAction

Sequence match with local variable assignments: (expr, v = rhs, w = rhs2) — expression matches AND variables assigned

Fields

expression: Box<SvaExpr>

assignments: Vec<(String, Box<SvaExpr>)>

LocalVar(String)

Local variable reference within a sequence/property

ConstCast(Box<SvaExpr>)

const’ cast: const'(expr) — freezes value at queue time

Clocked

Clocked expression: @(posedge clk) body — preserves clock annotation for multi-clock

Fields

clock: String

edge: ClockEdge

body: Box<SvaExpr>

ArrayMap

Array map method: A.map(x) with (expr) (IEEE 7.12, 2023)

Fields

array: Box<SvaExpr>

iterator: String

with_expr: Box<SvaExpr>

TypeThis

Type operator: type(this) (IEEE 6.23, 2023)

RealConst(f64)

Real literal constant: 1.5, 1.2E3 (IEEE 5.7.2, 2023)

Trait Implementations

impl Clone for SvaExpr

fn clone(&self) -> SvaExpr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SvaExpr

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

Formats the value using the given formatter.