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

It maps an input value and a current state to a next state. In this setting, the transition relation of the circuit is given by:

T(s, s′) = ∃x ∈ B^n : s′ ≡ Δ(x, s)

This relation states that s′ is a possible successor of s when there exists an input x for which the next state function produces s′ from s.

Role in architectural modeling

In the architectural-style formulation described in the evidence, a macro named next_state is explicitly defined to capture the effects of instructions and interrupts on the architectural state. The architectural state is represented as a user-defined VHDL record that combines elements such as the register file, status flags, and program counter. Interface data types for memories and ports are similarly defined.

The next_state macro returns the architectural state modified by execution of the current instruction. For example, the cited text describes a case in which an ADD instruction updates the register file of the current architectural state with the sum of source operands. In this usage, next_state is described as forming the core of the ISA.

Use in equivalence checking

The evidence describes an equivalence-proof structure relating an RTL CPU implementation to an ISA-level model. An abstraction function vstate maps implementation state to ISA architectural state. The proof goal is that applying the implementation transition relation T and then mapping the resulting CPU state to the ISA state corresponds to applying next_state at the ISA level.

A representative architectural property freezes:

instr       = decode(instruction) @ t
isa_state   = vstate @ t
isa_state_p = vstate @ t+1
nstate      = next_state(isa_state, instr) @ t

and proves:

at t+1: isa_state_p = nstate

This expresses that the ISA state observed at the next time point equals the state produced by next_state from the current ISA state and decoded instruction.

Use in instruction set simulator generation

The cited work uses the architectural-style property and its next_state function as the starting point for automatic generation of a C++ instruction set simulator. The generated simulator core is a C++ class that contains instruction-execution code and holds the architectural state. Generation steps include producing public functions for next_state, decode, and interface macros; producing private functions for remaining macros; generating a member variable for architectural state; replacing ITL/HDL types and operations by C++ equivalents; and replacing update expressions with direct array or structure overwrites in C++.

The update keyword is used in ITL to explicitly model write access to an array or record data structure, which is important for expressing how next_state modifies architectural state.