Module rtl 

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

A TransitionSystem is the classic (registers, property) model of synchronous hardware: each Register has a width, an initial value, and a next-state expression over the CURRENT state; a safety property must hold in every reachable state. 1-bit registers are control/FSM bits; wider registers are datapath, handled through the bit-blaster. This module time-indexes the model (r → r@t), lowers it through the certified prover seam (super::sva_to_proof::bounded_to_proof), and drives logicaffeine_proof::bmc. Pure Rust, certified, Z3-free.

parse_transition_system ingests a synthesizable Verilog subset (multi-bit reg, initial, one always @(posedge clk) block, assert property) with a typed (bool / bitvector) expression parser. Unsupported constructs error out — never a silent mis-parse.

Structs

Register

A hardware register: a width, an optional initial value, and its next-state function.

RtlParseError

A Verilog parse error (kept distinct so the BMC layer can surface it verbatim).

TransitionSystem

A synchronous transition system over Boolean and bitvector registers.

Enums

NextState

A next-state function: a direct expression, or a guarded if/else (from RTL reset/mux logic). Guards reference the current state and free inputs.

Functions

parse_transition_system

Parse a synthesizable Verilog module into a TransitionSystem. Errors (never silently mis-parses) on anything outside the supported subset.