Module codegen_sva 

SVA/PSL Code Generation for Hardware Verification

Generates SystemVerilog Assertions (SVA), Property Specification Language (PSL), and Rust runtime monitors from temporal property specifications.

Modules

bitblast

Bit-blasting: BoundedExpr datapath (bitvector) operations → boolean ProofExpr.

cdc

Clock Domain Crossing (CDC) Formal Verification

ci

CI/CD Integration — SARIF Output for GitHub Security Tab

controller_gen

Designer → certified controller: turn a synthesized PhasePlan into a Verilog phase-FSM and let the existing RTL pipeline (parse_transition_system → prove_invariant) certify it.

coverage

Specification Coverage Metrics

fol_to_sva

FOL → SVA Formal Synthesis

fol_to_verify

FOL → Bounded Verification IR Translation

hw_pipeline

Hardware Verification Pipeline

power

Power-Aware Formal Verification

protocols

Pre-Verified Protocol Templates

rtl

RTL / transition-system bounded model checking — including multi-bit (bitvector) registers.

rtl_extract

Verilog Declaration Parser

rtl_kg

RTL KG + Spec-RTL Linking

signal_design

Conflict-free traffic-signal PHASE DESIGNER (certified SAT synthesis).

sufficiency

Property Sufficiency Analysis

sva_model

SVA Semantic Model

sva_to_proof

Bounded SVA/FOL obligation → ProofExpr (the certified-prover seam).

sva_to_verify

SVA → Bounded Verification IR Translation

sva_vacuity

SVA Nonvacuous Evaluation Tracking (IEEE 16.14.8)

synthesis_refine

CEGAR Refinement for SVA Synthesis

synthesize

Sprint 5C: Top-Level Synthesis API

traffic_flow

Traffic FLOW / capacity analysis as model checking.

verified_compiler

Verified SVA Compiler via Futamura Projections

verify_to_kernel

Spec Encoding: BoundedExpr → Kernel Term

z3_synth

Sprint 4A: Z3 Synthesis Constraint Builder

Structs

SvaProperty

A single SVA property ready for emission.

Enums

SvaAssertionKind

Assertion type — determines the SVA wrapper.

Functions

emit_psl_property

Emit a single PSL property.

emit_rust_monitor

Emit a Rust runtime monitor scaffold for a property.

emit_sva_module

Emit multiple SVA properties as a complete module.

emit_sva_property

Emit a single SVA property with its assertion wrapper.

sanitize_property_name

Sanitize a human-readable property name into a valid SVA identifier. “Data Integrity” → “p_data_integrity”