Module sva_model

Expand description

SVA Semantic Model

Provides an AST for a subset of SystemVerilog Assertions, a parser for that subset, and structural equivalence checking.

This model enables the Z3 semantic equivalence pipeline: FOL (from LOGOS) ↔ SVA (from LLM) checked for structural match.

Structs§

CheckerDecl: Checker declaration (IEEE Chapter 17)
DistItem: A dist item — value or range with weight
ElaborationContext: Context for elaborating directives with default clocking and disable iff. IEEE 16.15: default clocking applies to all assertions in scope that lack an explicit clock. IEEE 16.16: default disable iff applies the reset condition to all assertions lacking explicit disable iff.
LetDecl: Let declaration (IEEE 11.12) — pure expression substitution
PropertyDecl: Named property declaration (IEEE 16.12)
RandVar: Random variable in a checker (IEEE 17.7)
SequenceDecl: Named sequence declaration (IEEE 16.8)
SvaDirective: A concurrent assertion directive (IEEE 16.14)
SvaParseError: Parse error for SVA subset.
SvaPort: A port in a named sequence or property declaration

ClockEdge: Clock edge type
DistKind: Dist weight kind (IEEE 18.5.4)
ImmediateDeferred: Deferred assertion timing (IEEE 16.4)
RandVarType: Type discriminant for random variables (IEEE 17.7, extended in 2023)
SvaDirectiveKind: Assertion directive kind (IEEE 16.14)
SvaExpr: SVA expression AST — models a useful subset of SystemVerilog Assertions.
SvaPortType: Port type for named sequence/property declarations (IEEE 16.8, 16.12)

checker_quantifier_structure: Get checker’s random variable quantifier structure. Returns (const_rand_vars, per_timestep_rand_vars).
elaborate_directives: Elaborate a set of directives by applying default clocking and disable iff.
parse_sva: Parse a subset of SVA text into an SvaExpr.
parse_sva_directive: Parse a concurrent assertion directive (IEEE 16.14).
resolve_checker: Resolve a checker instance by binding ports into its assertions.
resolve_let_instance: Resolve let declarations by inlining expression substitution. IEEE 11.12: let is pure expression substitution with no temporal semantics.
resolve_sequence_instance: Resolve a sequence instance by substituting actuals for formals.
sva_expr_to_string: Render an SvaExpr back to valid SVA text. Closes the round-trip: parse_sva(text) → SvaExpr → sva_expr_to_string → text.
sva_exprs_structurally_equivalent: Check if two SvaExpr trees are structurally equivalent.
translate_dist_to_ranges: Translate dist items into range constraints for formal verification. IEEE 16.14.2: In formal mode, dist ≡ inside (range restriction only).
validate_dist: Validate dist list is non-empty.