Hetu-Formal asks whether a temporal or structural property holds for every behavior the model allows, and returns either an attributable proof or a concrete counterexample. Built around a controlled proof spine of AIG construction, Tseitin CNF conversion, a native CDCL SAT solver and k-induction, it keeps proof semantics, counterexample generation and solver evidence consistent across property verification, equivalence, protocol, security and coverage applications.
Compiles a SystemVerilog Assertion subset into executable observer FSMs, proving invariants and solving cover goals with clean unsupported-property diagnostics.
Bounded model checking with concrete counterexample traces, k-induction with base and step evidence, and IC3/PDR unbounded safety with a certified inductive invariant.
Localization-based CEGAR built over the IC3 flow, plus liveness-to-safety lasso reasoning that returns a proof or a stem-and-loop starvation witness.
Sequential RTL-to-RTL validation, frozen-symbol datapath scoreboarding and datapath validation against integer and fixed-point reference expressions, including narrow multiply and saturation.
AXI, AHB, APB and generic ready/valid rule libraries bound to mapped design signals on the master or slave side, with environment assumptions constraining legal behavior.
Cover-property reachability with witnesses and formal unreachable analysis applied to real SoC unreachable-code points, feeding coverage closure evidence.
Information-flow verification using two-copy models to test non-interference between secret sources and observable outputs.
Vacuity, over-constraint, weak cone-of-influence and mutation-escape analysis so the proof environment itself is checked, not trusted.
A fenced Z3 SMT flow for supported integer and non-NaN IEEE-754 problems, returning UNKNOWN rather than a fabricated proof, with structured evidence JSON on every run.
| Stage | Verification, formal property verification and equivalence checking |
|---|---|
| Proof engines | Bounded model checking, k-induction, IC3/PDR, localization CEGAR, liveness-to-safety, native CDCL SAT with optional CaDiCaL agreement, fenced Z3 SMT |
| Applications | Property/assertion proof, model checking, LEC equivalence, connectivity and protocol, coverage and formal unreachability, security non-interference, low-power sequencing, functional-safety fault classification |
| Property input |
SystemVerilog Assertion subset (|->, |=>,
##n,
disable iff,
$past,
$rose,
$fell,
$stable, selected
s_eventually), protocol rule
libraries, environment assumptions
|
| Design inputs | RTL and mapped netlist within the supported Verilog subset, VCD-seeded simulation-to-formal initialization with conditional-verdict labelling |
| Outputs | Structured evidence JSON with engine, solver, depth, verdict and witness/proof metadata; concrete counterexample traces; certified invariants; formal UNR results for coverage closure |
| PDK / technology | Not required, operates on RTL and netlist (technology independent) |
| Flow | CLI-first native stage in the WIOWIZ verification flow, deterministic and evidence-sealed for regression and CI |
Hetu Formal 0.26.0 for Linux x86_64 includes the command-line engine and native Studio GUI. The GUI provides RTL import, command and argument controls, Run, Stop, result views, engine log and transcript.
SHA-25657063d5cd976e8c84bd2080125223bed0c937c1d7c0673bc3f67028fa829203e
Verify after download: sha256sum hetu-formal-0.26.0-linux-x86_64.tar.gz
