Module hw_pipeline 

Hardware Verification Pipeline

Public API for the LOGOS hardware verification pipeline: English spec → Kripke FOL → Knowledge Graph → SVA → Z3 Equivalence.

Structs

EquivalenceResult

Result of checking semantic equivalence between FOL and SVA.

HwSignalDecl

Declares a hardware signal with its English name and SVA name.

HwSpec

A compiled hardware specification.

KgLink

A directed relation between two nodes (indices into KgSummary::nodes).

KgNode

A node in the renderable knowledge-graph view: a signal with its role and width.

KgSummary

A compact, render-ready view of the hardware knowledge graph extracted from an English spec — signals as nodes, relations (drives / triggers / handshakes / …) as directed links.

PipelineResult

Full pipeline result.

SignalMap

Maps FOL argument names (from English proper nouns) to SVA signal names.

WaveSignal

One signal’s value over time in a counterexample waveform. width is the bit width (1 = a boolean control bit); each values[t] is the (reconstructed) register value at timestep t, or None if unconstrained there.

Waveform

A counterexample rendered as a waveform: signals (rows) over discrete timesteps (columns).

Enums

HwError

Error type for hardware verification pipeline.

VacuityReport

A vacuity verdict for a synthesized property.

Functions

check_bounded_equivalence

Check bounded equivalence between two BoundedExpr trees.

check_spec_vacuity

Vacuity check (Z3-free, certified): does the property’s trigger ever fire? An unsatisfiable antecedent means the property passes vacuously — a dead trigger that usually signals a malformed spec. Reuses logicaffeine_proof::bmc::check_vacuity.

check_structural_equivalence

Check structural equivalence between two SVA expressions.

compile_hw_property

Compile an English hardware property with signal declarations.

compile_hw_spec

Compile an English hardware spec to FOL text.

counterexample_waveform

Turn a counterexample’s bindings into a waveform. Handles both 1-bit signals (name@t) and bit-blasted multi-bit registers (name@t#i), reconstructing each register’s integer value per timestep from its bits. Signals are sorted by name; each row spans 0..timesteps. Malformed keys (no @t) are skipped.

emit_hw_sva

Emit SVA from a property specification.

extract_kg

Extract a Knowledge Graph from an English hardware spec (one call).

kg_summary

Extract a render-ready knowledge graph from an English hardware spec. Pure Rust (no Z3), so it runs in the browser. Merges the legacy and typed (ontology) edge sets.

prove_bounded_equivalence

Check FOL ↔ SVA semantic equivalence at a bound with our pure-Rust, certified prover (no Z3) — the in-browser counterpart of check_z3_equivalence. Lowers both bounded obligations to ProofExpr and discharges F ↔ S through the CDCL → RUP tiers: an equivalent verdict is RUP-certified, a non-equivalent one carries a counterexample trace (name@t → "1"/"0"). Errors (fail-closed, never a false “equivalent”) if either obligation leaves the Boolean fragment — data-path needs bit-blasting, not wired yet.

prove_spec_sva_equivalence

End-to-end: an English spec and a candidate SVA string → certified semantic equivalence with our prover. The Z3-free counterpart of check_z3_equivalence: the same translators, our CDCL → RUP tiers instead of Z3.

translate_spec_to_bounded

Translate a LOGOS spec to bounded verification IR using compile_kripke_with.

translate_sva_to_bounded

Translate an SVA string to bounded verification IR.