Next State Function
ConceptA next state function is the function in a finite-state model that computes the next state from an input and the current state. In the cited hardware-verification and instruction-set-simulator context, it also appears as an ITL macro, `next_state`, that updates architectural state according to the current decoded instruction and serves as the core of a formally checkable ISA description.
First seen 5/26/2026
Last seen 5/29/2026
Evidence 4 chunks
Wiki v1
WIKI
Definition
In the finite-state-machine model of a synchronous circuit, the next state function is denoted Δ. The circuit is modeled as M = (I, S, S0, Δ, Λ, O), where I is the input alphabet, S is the finite set of states, S0 is the set of initial states, Λ is the output function, and O is the output alphabet. The next state function has the type:
Δ : B^n × B^m → B^m
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
7 connectionsThe next state function forms the core of the ISA description, capturing instruction semantics.
Architectural style properties include an explicit definition of the next state function.
The next state function is a component of the finite state machine model.
The next_state macro implements the next state function of the ISA.
Architectural style properties require an explicit next state function definition.
The FSM model uses a next state function to define transitions.
Instruction decoding is part of the ISA description used by the next state function.
LINKED ENTITIES
4 linksFinite State Machine modeled_in The evidence states that a synchronous circuit is modeled as an FSM that includes the next state function Δ.
Architectural State updates The evidence says the next_state macro captures the effects of instructions and interrupts on architectural state and returns the architectural state modified by the current instruction.
Instruction Set Architecture core_of The evidence explicitly states that the next_state function forms the core of the ISA.
Instruction Set Simulator used_for_generation_of The evidence describes using the next_state-based architectural property as the starting point for automatic C++ ISS generation.
CITATIONS
9 sources9 citations — click to expand
[1] A synchronous circuit can be modeled as an FSM containing input alphabet, state set, initial states, output function, next state function, and output alphabet. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[2] The next state function has type Δ : B^n × B^m → B^m and defines the transition relation T(s, s′) = ∃x ∈ B^n : s′ ≡ Δ(x, s). Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[3] Architectural-style modeling explicitly defines a macro next_state that captures effects of instructions and interrupts on architectural state. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[4] Architectural state is represented as a user-defined VHDL record combining elements such as register file, status flags, and program counter. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[5] The next_state macro returns the architectural state modified by execution of the current instruction and forms the core of the ISA. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[6] The equivalence proof relates RTL transition behavior to ISA-level next_state behavior through the abstraction function vstate. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[7] A property using next_state can capture all behavior of the verified design and provide a formally checkable ISA description for ISS generation. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[8] ISS generation includes public functions for next_state, decode, and interface macros, a member variable for architectural state, C++ replacements for ITL/HDL types and operations, and replacement of update expressions by direct array or structure overwrites. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[9] The ITL update keyword explicitly defines write access to an array or record data structure. Generating an Efficient Instruction Set Simulator from a Complete Property Suite