Circuit-agnostic Property Checker

A circuit-agnostic property checker is a reusable verification component in the rtlv framework that operates on a generic Rosette circuit model rather than on a specific Verilog design, and decides whether the modeled circuit satisfies a target security or correctness property. The same checker implementation can be reused across multiple circuits, avoiding per-circuit duplication of verification logic.

Role in the rtlv Workflow

In the rtlv architecture, the circuit-agnostic property checker occupies the central position in the verification pipeline. The overall flow is:

1. The user supplies a circuit in Verilog.
2. Yosys synthesizes it into an SMT-LIB model.
3. rtlv's #lang yosys front end compiles the SMT-LIB model into a Rosette model (a Racket program).
4. The user supplies circuit/property-specific performance hints.
5. The circuit-agnostic property checker consumes the Rosette model plus the hints and returns either an "OK" verification result or a counterexample.

This separation isolates the trust-critical reasoning in a small, generic checker, while pushing per-circuit knowledge into untrusted hints, yielding a smaller trusted code base than a per-circuit verification script.

Performance Hint Interface

A defining feature of a circuit-agnostic property checker in rtlv is a performance hint interface. Hints allow the developer to suggest that the checker transform the circuit state in a certain way—for example, replacing a field with a fresh symbolic value or abstracting memory entries that depend only on allowed dependencies. The goal of these hints is generally to reduce the size of symbolic expressions and therefore simplify both symbolic execution and the final solver query.

The hint interface exposed by rtlv/shiva (the example circuit-agnostic property checker) includes:

• abstract [field-name]: Checks if the field only depends on allowed dependencies; if so, replaces it with a fresh symbolic, which is added to the allowed-dependencies set.
• overapproximate [field-name]: Replaces the field with a fresh symbolic without checking dependencies.
• abstract-or-overapproximate-vector: For each entry of a memory field, abstracts the entry if it only depends on allowed dependencies; otherwise overapproximates it.

Soundness and Trust Model

A key property of this design is that the property checker is sound and the hints are untrusted. No matter what hints a developer specifies, the tool will not erroneously say that a property holds when it does not. Supplying inadequate or incorrect hints can only harm performance or make the tool fail to prove the property; performance hints cannot be misused to make the tool erroneously report "OK."

This enables a workflow where the developer can freely experiment with performance hints without worrying about invalidating the proof. The verification tool itself is considered trusted, but by encapsulating the trusted code for transforming circuit state in a non-circuit-specific checker, the developer can apply performance hints as needed while maintaining high confidence in the proof's correctness. This is what made it possible to reuse the same checker for multiple circuits, including a small PicoRV32 SoC and a much more complex MicroTitan SoC.

Example: rtlv/shiva

rtlv/shiva is the canonical example of a circuit-agnostic property checker from the rtlv paper. It checks the output determinism property: a circuit satisfies output determinism if its outputs do not depend on data present in the circuit state prior to reset. This is a property similar to microarchitectural state clearing, and verifying it generally requires symbolically executing the circuit's boot code from an unconstrained initial state.

rtlv/shiva takes in a Rosette circuit model (including components such as the step function and register names), executes the circuit symbolically based on the model provided, and returns whether or not the circuit satisfies output determinism. Because it is circuit-agnostic, the same checker was used to verify output determinism for both the MicroTitan SoC (around 4,300 flip-flops, ~24,516 cycles of boot code) and the PicoRV32 SoC (around 1,300 flip-flops, 104 cycles of boot code).

Why the Design Matters

Without a circuit-agnostic abstraction, aggressive circuit-specific optimizations (which are often necessary to make symbolic execution tractable) would have to be trusted, since they would be embedded in the verification script for each circuit. By forcing these optimizations to flow through an explicit, untrusted hint interface, and by pushing all trust-critical transformations into the shared checker, the architecture preserves soundness while still permitting per-circuit peephole optimizations. This is what allows rtlv to scale from a small 1,300-flip-flop design verified in 1.3 seconds up to a 4,300-flip-flop SoC verified over 20,000+ cycles of boot code execution.