The state transition graph of an FSM, i.e., the behavior that its netlist implements. More...

#include </home/runner/work/hal/hal/plugins/solve_fsm/include/solve_fsm/state_transition_graph.h>

Collaboration diagram for hal::solve_fsm::StateTransitionGraph:

Public Member Functions
u32	get_state_size () const
	Get the number of flip-flops that make up the state register, i.e., the bit-size of a state. More...

Result< std::string >	generate_dot_graph (const std::filesystem::path &graph_path="", const u32 max_condition_length=128, const u32 base=10) const
	Render the state transition graph in the DOT format. More...

Result< std::string >	to_string (const u32 base=10) const
	Render the state transition graph as human-readable text, without truncating anything. More...

Result< std::monostate >	write_txt (const std::filesystem::path &file_path, const u32 base=10) const
	Write the state transition graph to a text file, without truncating anything. More...

Public Attributes
Netlist *	netlist = nullptr
	The netlist that implements the FSM. More...

std::vector< Gate * >	state_register
	The flip-flops that make up the state register, in the order that determines the encoding of a state. More...

std::vector< std::pair< std::string, std::vector< Net * > > >	output_nets
	The outputs of the FSM, each given as a name and the nets that make up that output. More...

std::map< u64, std::map< u64, BooleanFunction > >	transitions
	A map from each state to its successor states, together with the condition under which the respective transition is taken. More...

std::map< u64, std::vector< std::pair< std::string, BooleanFunction > > >	outputs
	A map from each state to the value of every output of the FSM in that state. More...

Detailed Description

The state transition graph of an FSM, i.e., the behavior that its netlist implements.

States are encoded as integers, with the first flip-flop of the state register providing the least significant bit. The same holds for the nets of a multi-bit output.

Definition at line 58 of file state_transition_graph.h.

Member Function Documentation

◆ generate_dot_graph()

Result< std::string > hal::solve_fsm::StateTransitionGraph::generate_dot_graph	(	const std::filesystem::path &	graph_path = `""`,
		const u32	max_condition_length = `128`,
		const u32	base = `10`
	)		const

Render the state transition graph in the DOT format.

Each state becomes a node labeled with its value and, if outputs were computed, with the value of every output in that state. Each transition becomes an edge labeled with its condition. Boolean functions are truncated to keep the graph readable, use to_string to get them in full.

Parameters

[in]	graph_path	- The file path at which to store the graph. No file is written if the path is left empty. Defaults to an empty path.
[in]	max_condition_length	- The maximum number of characters printed for a Boolean function. Defaults to 128.
[in]	base	- The base in which state and output values are printed, either 2 or 10. Defaults to 10.

Returns: OK() and the graph in the DOT format on success, an error otherwise.

Definition at line 87 of file state_transition_graph.cpp.

References ERR, get_state_size(), name, OK, outputs, hal::state, to_string(), and transitions.

◆ get_state_size()

u32 hal::solve_fsm::StateTransitionGraph::get_state_size ( ) const

Get the number of flip-flops that make up the state register, i.e., the bit-size of a state.

Returns: The bit-size of a state.

Definition at line 82 of file state_transition_graph.cpp.

References state_register.

Referenced by generate_dot_graph(), hal::PYBIND11_PLUGIN(), and to_string().

◆ to_string()

Result< std::string > hal::solve_fsm::StateTransitionGraph::to_string ( const u32 base = 10 ) const

Render the state transition graph as human-readable text, without truncating anything.

Starts with a legend that maps each bit of the state to the flip-flop holding it, each output to the nets that make it up, and every net variable appearing in a Boolean function to the net it stands for. The legend is followed by one block per state holding its outputs and all of its outgoing transitions together with the full condition of each.

Parameters

[in] base - The base in which state and output values are printed, either 2 or 10. Defaults to 10.

Returns: OK() and the state transition graph as text on success, an error otherwise.

Definition at line 178 of file state_transition_graph.cpp.

References ERR, hal::BooleanFunctionNetDecorator::get_net_from(), get_state_size(), name, netlist, OK, output_nets, outputs, hal::state, state_register, and transitions.

Referenced by generate_dot_graph(), and write_txt().

◆ write_txt()

Result< std::monostate > hal::solve_fsm::StateTransitionGraph::write_txt	(	const std::filesystem::path &	file_path,
		const u32	base = `10`
	)		const

Write the state transition graph to a text file, without truncating anything.

Parameters

[in]	file_path	- The file path at which to store the text representation.
[in]	base	- The base in which state and output values are printed, either 2 or 10. Defaults to 10.

Returns: OK() on success, an error otherwise.

Definition at line 286 of file state_transition_graph.cpp.

References ERR, ERR_APPEND, OK, and to_string().

Member Data Documentation

◆ netlist

Netlist* hal::solve_fsm::StateTransitionGraph::netlist = nullptr

The netlist that implements the FSM.

Definition at line 63 of file state_transition_graph.h.

Referenced by hal::PYBIND11_PLUGIN(), hal::solve_fsm::solve_fsm(), and to_string().

◆ output_nets

std::vector<std::pair<std::string, std::vector<Net*> > > hal::solve_fsm::StateTransitionGraph::output_nets

The outputs of the FSM, each given as a name and the nets that make up that output.

The first net of an output provides its least significant bit. Empty unless outputs were configured.

Definition at line 77 of file state_transition_graph.h.

Referenced by hal::PYBIND11_PLUGIN(), hal::solve_fsm::solve_fsm(), and to_string().

◆ outputs

std::map<u64, std::vector<std::pair<std::string, BooleanFunction> > > hal::solve_fsm::StateTransitionGraph::outputs

A map from each state to the value of every output of the FSM in that state.

The outputs of a state are given in the order in which they were configured. An output of a Moore FSM only depends on the state, so its Boolean function is constant. An output of a Mealy FSM may also depend on the inputs of the FSM, in which case its Boolean function still contains the input variables.

Empty unless outputs were configured.

Definition at line 93 of file state_transition_graph.h.

Referenced by generate_dot_graph(), hal::PYBIND11_PLUGIN(), hal::solve_fsm::solve_fsm(), and to_string().

◆ state_register

std::vector<Gate*> hal::solve_fsm::StateTransitionGraph::state_register

The flip-flops that make up the state register, in the order that determines the encoding of a state.

The first flip-flop provides the least significant bit, so this is what maps a state back to the netlist.

Definition at line 70 of file state_transition_graph.h.

Referenced by get_state_size(), hal::PYBIND11_PLUGIN(), hal::solve_fsm::solve_fsm(), and to_string().

◆ transitions

std::map<u64, std::map<u64, BooleanFunction> > hal::solve_fsm::StateTransitionGraph::transitions

A map from each state to its successor states, together with the condition under which the respective transition is taken.

Definition at line 82 of file state_transition_graph.h.

Referenced by generate_dot_graph(), hal::PYBIND11_PLUGIN(), hal::solve_fsm::solve_fsm(), and to_string().

The documentation for this struct was generated from the following files:

plugins/solve_fsm/include/solve_fsm/state_transition_graph.h
plugins/solve_fsm/src/state_transition_graph.cpp

Public Member Functions

Public Attributes

Detailed Description

Member Function Documentation

◆ generate_dot_graph()

◆ get_state_size()

◆ to_string()

◆ write_txt()

Member Data Documentation

◆ netlist

◆ output_nets

◆ outputs

◆ state_register

◆ transitions