Finite State Machine
ConceptA finite state machine (FSM) is a computational model that transitions among a finite set of states in response to inputs or events, used to model digital hardware, communication protocols, processors, pipeline stages, FPGA control logic, and software specification languages. The model underpins verification techniques such as Interval Property Checking, hardware-fuzzing coverage metrics that monitor state transitions, and formal properties for evaluating Single Event Upsets in RISC-V cores.
First seen 5/26/2026
Last seen 8/5/2026
Evidence 40 chunks
Wiki v7
WIKI
Overview
A finite state machine (FSM) is a computational model that transitions among a finite set of states in response to inputs or events. FSMs are widely used to model digital hardware, communication protocols, processors, pipeline stages, FPGA control logic, and software specification languages. [C1][C2][C3]
Formal FSM model in hardware verification
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
17 connectionsRegister coverage aims to track FSM states in the processor by monitoring register values.
IPC models synchronous circuits as finite state machines.
CSR-transition coverage tracks processor FSM state transitions through CSR changes.
Privilege mode is part of the processor FSM state tracked by CSR transitions.
Control FSMs are the primary targets of control path verification in RISC-V processors.
ProcessorFuzz aims to explore different FSM states of the processor.
FSMs are described in RTL hardware description languages.
DIFUZZRTL monitors FSM state transitions via register coverage.
CSR-transition coverage tracks FSM state transitions in the processor via CSR changes.
The Ibex Core controller uses a Finite State Machine to manage execution.
The next state function is a component of the finite state machine model.
The FSM model uses a next state function to define transitions.
TheHuzz uses FSM coverage among other metrics
Multicycle instructions use an FSM in an early pipeline stage for dispatching.
Finite state machine synchronization requirements create hard-to-activate regions.
The paper provided efficient bug detection on finite traces in RISC-V ALUs and control FSMs.
The specification language incorporates finite state machines to model system behavior.
LINKED ENTITIES
9 linksRegister Coverage infers-FSM-state DIFUZZRTL's register coverage monitors datapath registers to determine the current FSM state.
CSR-transition coverage exposes-FSM-state ProcessorFuzz proposes monitoring CSR transitions as feedback to expose new processor FSM states and transitions.
DiFuzzRTL uses-FSM-state-coverage DIFUZZRTL uses register coverage to infer the current FSM state in the cited processor-fuzzing context.
ProcessorFuzz targets-FSM-transitions ProcessorFuzz proposes CSR-transition coverage and the Transition Unit workflow for FSM-state exploration.
TheHuzz classifies-FSM-component-bugs TheHuzz classifies processor bugs by component, including FSM-classified bugs such as cache-coherency failures in the mor1kx cache controller.
specification language extended-by-FSM The contract-oriented specification language is extended with FSMs to drive symbolic animation and full test-scenario synthesis.
WhisperFuzz models-circuit-as-FSM-and-refines-with-MEG WhisperFuzz uses FSMs as the high-level model of sequential digital circuits (cache set, divider, etc.) and refines the FSM with Micro-Event Graphs for timing-side-channel localization.
Micro-Event Graph refines-FSM-paths WhisperFuzz's MEG refines FSM state-transition paths into Micro-Event Paths at finer RTL granularity to localize timing divergences.
HyPFuzz uses-FSM-coverage-metric HyPFuzz combines branch, condition, and FSM coverage metrics to monitor the sequential logic of the DUT.
CITATIONS
20 sources20 citations — click to expand
[1] An FSM is a computational model that transitions among a finite set of states in response to inputs or events. WhisperFuzz: White-Box Fuzzing for Detecting and Locating Timing Vulnerabilities in Processors
[2] A synchronous circuit is modeled as FSM M = (I, S, S0, Δ, Λ, O) with next-state function Δ : B^n × B^m → B^m and transition relation T(s, s′) = ∃x ∈ B^n : s′ ≡ Δ(x, s). Interval Property Checking with Incremental Invariant Generation (cited in previous article)
[3] Interval Property Checking unrolls the FSM transition relation T within a bounded time interval [0, c] and searches for counterexamples via SAT, with invariants added to avoid unreachable counterexamples. Interval Property Checking with Incremental Invariant Generation (cited in previous article)
[4] Pipeline datapath modeling uses Data_R(s, i) and Valid_R(s, i) mapping functions to capture architectural register values through pipeline stages; an FSM in an early stage dispatches partial multicycle instructions. Interval Property Checking with Incremental Invariant Generation (cited in previous article)
[5] A processor is a complex FSM; CSRs expose the current processor state and transitions in CSRs signify new processor FSM states. ProcessorFuzz (cited in previous article)
[6] DIFUZZRTL's register coverage monitors datapath registers to determine the current FSM state but only stores current state and ignores previous state, which can miss important transitions (illustrated with Bug 2 from state N1→N2). ProcessorFuzz (cited in previous article)
[7] ProcessorFuzz proposes CSR-transition coverage; each transition is stored as (Im, S0, S1) with instruction mnemonic, before-state, and after-state values; transitions are grouped and filtered (e.g., instret, status-CSR writes). ProcessorFuzz (cited in previous article)
[8] The Transition Unit (TU) takes an extended ISA trace log, extracts CSR transitions, and applies a filter to remove transitions that do not affect the architectural state. ProcessorFuzz (cited in previous article)
[9] In SoC bus protocols (AXI-4 Lite), two parallel FSMs (master and slave) must be synchronized via handshake signals (awvalid/awready, wvalid/wready, bvalid/bready); incorrect ordering can cause deadlocks or coverage plateaus. FuSS (cited in previous article)
[10] TheHuzz's bug table classifies cache-coherency bugs (e.g., Bug B4 in mor1kx) under the FSM component, modeling the cache controller as an FSM. TheHuzz (cited in previous article)
[11] Reachability for communicating finite-state machines connected by FIFO channels is undecidable in general, decidable for the recognizable channel property, and open for the rational channel property. Reachability problems for communicating finite state machines
[12] A scalable FSM overlay using memory decomposition on transitional logic reduces lookup tables by 15-29% for individual FSMs and 77-99% for an overlay supporting different FSMs, and reduces compilation time to tenths of a second. A Scalable, Low-Overhead Finite-State Machine Overlay for Rapid FPGA Application Development
[13] A constraint-logic-programming specification language inspired by contract-oriented programming is extended with FSMs to generate full test scenarios through symbolic animation, with type builders linking type semantics to a CSP framework. Constraint-based test generation (cited in previous article)
[14] A cache set is represented as an FSM with five states (LookUp, FreeBlock, Replace, Wait, Ready); cache-hit transition {LookUp → Ready} takes 3 cycles, miss-with-free-block {LookUp → FreeBlock → Wait → Ready} takes 19 cycles, and miss-without-free-block {LookUp → FreeBlock → Replace → Wait → Ready} takes 23 cycles. WhisperFuzz: White-Box Fuzzing for Detecting and Locating Timing Vulnerabilities in Processors
[15] WhisperFuzz notes that FSM states do not always take constant execution time and that an FSM model is abstract, motivating the Micro-Event Graph as a finer-grained representation of microarchitectural events. WhisperFuzz: White-Box Fuzzing for Detecting and Locating Timing Vulnerabilities in Processors
[16] HyPFuzz combines branch, condition, and FSM coverage metrics for code coverage; the FSM metric monitors the sequential logic of the DUT and treats any new coverage point as at least one new microarchitectural state transition triggered. WhisperFuzz: White-Box Fuzzing for Detecting and Locating Timing Vulnerabilities in Processors
[17] WhisperFuzz builds a Micro-Event Graph G(D) from RTL code, defines Micro-Event Paths (MEPs) as sequences of edges from input nodes to output nodes, maps MEPs to FSM paths at finer granularity, and uses divergence of MEPs to localize the wire (e.g., tag_addr) responsible for path differences. WhisperFuzz: White-Box Fuzzing for Detecting and Locating Timing Vulnerabilities in Processors
[18] In the Ibex core, the ibex_controller module is modeled as an FSM with current state stored in the 4-bit register ctrl_fsm_cs, identified as the most vulnerable register to SEU-induced SDCs; cpuctrl_q's LSB is also vulnerable. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core
[19] Hang scenarios for an FSM-modeled core include WFI, Dead State (FSM stuck and cannot leave), and Live State (FSM trapped in a sequence and cannot return to a state reachable from others); formal properties are developed with assertions and 'cover' statements to address designed state repetition. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core
[20] The ESP JETA 2025 review surveys FSM-related RISC-V control-path verification techniques: SMT-based bounded model checking for control logic, CSRFormal for CSRs/transition behaviors, DIFV for pipelines (deadlocks/hazards), AI-assisted Coq proof strategy selection, parameterized invariants, and Hybrid Automata pipeline modeling (Fetch/Decode/Execute/Memory/WriteBack) checked with Uppaal/HyTech. Scalable Formal Verification Strategies for RISC-V Based Control Paths: A Review