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. In formal hardware verification, a synchronous circuit is modeled as an FSM M = (I, S, S0, Δ, Λ, O) with input alphabet, output alphabet, finite state set, initial states, next-state function, and output function. FSMs are used to model processors, communication protocols, pipeline stages, and FPGA control logic, and they underpin techniques such as Interval Property Checking (IPC) and datapath mapping functions for pipeline verification.
First seen 5/26/2026
Last seen 6/8/2026
Evidence 23 chunks
Wiki v5
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, and other discrete-state systems. [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
11 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.
DIFUZZRTL monitors FSM state transitions via register coverage.
Privilege mode is part of the processor FSM state tracked by CSR transitions.
ProcessorFuzz aims to explore different FSM states of the processor.
CSR-transition coverage tracks FSM state transitions in the processor via CSR changes.
Multicycle instructions use an FSM in an early pipeline stage for dispatching.
The FSM model uses a next state function to define transitions.
The next state function is a component of the finite state machine model.
TheHuzz uses FSM coverage among other metrics
CITATIONS
11 sources11 citations — click to expand
[1] A synchronous circuit is modeled as an FSM M = (I, S, S0, Δ, Λ, O) with input alphabet I ⊆ B^n, output alphabet O ⊆ B^w, finite set of states S ⊆ B^m, output function Λ, and next-state function Δ, with initial states S0 ⊆ S and transition relation T(s, s′) = ∃x ∈ B^n : s′ ≡ Δ(x, s). Automated Formal Verification of Processors
[2] A safety property f = AG(φ) is translated to a Boolean function [[f]]_t such that a satisfying assignment of [[f]]_t corresponds to a counterexample of φ. Automated Formal Verification of Processors
[3] IPC unrolls the FSM transition relation within a bounded time interval [0, c] and conjoins it with [[f]]_t to form a SAT instance for counterexample search; invariants (often automatically generated, verifiable by k-induction) are added to avoid unreachable counterexamples. Automated Formal Verification of Processors
[4] Multicycle instructions in processor designs are dispatched by an FSM in an early pipeline stage; the most general exception model compatible with the approach injects a new instruction into the pipeline after exception acknowledgement. Automated Formal Verification of Processors
[5] An automatically generated mapping function Data_R(s, i) captures the complex mapping of the visible register R to the implementation; an additional mapping function Valid_R(s, i) captures whether the forwarding data is indeed valid. Automated Formal Verification of Processors
[6] A processor is described as a complex FSM whose current state is exposed via CSRs, with the architectural state held in the register file and status registers. ProcessorFuzz: Processor Fuzzing with Control and Status Register Transition Analysis
[7] DIFUZZRTL's register coverage only stores the current FSM state without the previous state, causing important test inputs to be discarded — illustrated by a RISC-V bug (Bug 2) that triggers in state N2 only if the previous state is N1. ProcessorFuzz: Processor Fuzzing with Control and Status Register Transition Analysis
[8] ProcessorFuzz applies a transition filter that drops transitions from writes to status CSRs (e.g., mstatus in RISC-V) because such transitions do not affect the architectural state of the processor, and avoids using counters like instret that would mark nearly every input as interesting. ProcessorFuzz: Processor Fuzzing with Control and Status Register Transition Analysis
[9] ProcessorFuzz's transition map stores each CSR transition as (Im, S0, S1) where Im is the producing instruction mnemonic, and groups CSR transitions by architectural unit (e.g., privileged vs unprivileged) to reduce state-space pressure. ProcessorFuzz: Processor Fuzzing with Control and Status Register Transition Analysis
[10] Reachability properties for communicating FSMs connected by unbounded FIFO channels are undecidable in general but decidable for protocols with the recognizable channel property; the question remains open for the rational channel property. Reachability problems for communicating finite state machines
[11] A scalable FSM overlay for FPGAs uses memory decomposition on transitional logic, achieving 15%–29% fewer LUTs for individual FSMs and 77%–99% fewer LUTs for overlays supporting different FSMs, with compilation reduced to tenths of a second. A Scalable, Low-Overhead Finite-State Machine Overlay for Rapid FPGA Application Development