hal::solve_fsm Namespace Reference

Functions
Result< std::map< u64, std::map< u64, BooleanFunction > > >	solve_fsm (Netlist *nl, const std::vector< Gate * > &state_reg, const std::vector< Gate * > &transition_logic, const std::map< Gate *, bool > &initial_state={}, const std::filesystem::path &graph_path="", const u32 timeout=600000)
Result< std::map< u64, std::map< u64, BooleanFunction > > >	solve_fsm_brute_force (Netlist *nl, const std::vector< Gate * > &state_reg, const std::vector< Gate * > &transition_logic, const std::filesystem::path &graph_path="")
Result< std::string >	generate_dot_graph (const std::vector< Gate * > &state_reg, const std::map< u64, std::map< u64, BooleanFunction >> &transitions, const std::filesystem::path &graph_path="", const u32 max_condition_length=128, const u32 base=10)

Function Documentation

generate_dot_graph()

Result< std::string > hal::solve_fsm::generate_dot_graph	(	const std::vector< Gate * > &	state_reg,
		const std::map< u64, std::map< u64, BooleanFunction >> &	transitions,
		const std::filesystem::path &	graph_path = "",
		const u32	max_condition_length = 128,
		const u32	base = 10
	)

Generates the state graph of a finite state machine from the transitions of that fsm.

Parameters

[in]	state_reg	- Vector contianing the state registers.
[in]	transitions	- Transitions of the fsm given as a map from origin state to all possible successor states and the corresponding condition.
[in]	graph_path	- Path where the transition state graph in dot format is saved.
[in]	max_condition_length	- The maximum character length that is printed for boolean functions representing the conditions.
[in]	base	- The base with that the states are formatted and printed.

Returns

A string representing the dot graph.

Definition at line 533 of file solve_fsm.cpp.

References ERR, test_plugin::graph_path, and OK.

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

solve_fsm()

Result< std::map< u64, std::map< u64, BooleanFunction > > > hal::solve_fsm::solve_fsm	(	Netlist *	nl,
		const std::vector< Gate * > &	state_reg,
		const std::vector< Gate * > &	transition_logic,
		const std::map< Gate *, bool > &	initial_state = {},
		const std::filesystem::path &	graph_path = "",
		const u32	timeout = 600000
	)

Generate the state transition graph of a given FSM using SMT solving. The result is a map from each state of the FSM to all of its transitions. A transition is given as each successor state as well as the Boolean condition that needs to be fulfilled for the transition to take place. Optionally also produces a DOT file representing the state transition graph.

Parameters

[in]	nl	- The netlist to operate on.
[in]	state_reg	- A vector of flip-flop gates that make up the state register of the FSM.
[in]	transition_logic	- A vector of combinational gates that make up the transition logic of the FSM.
[in]	initial_state	- A map from the state register flip-flops to their initial (Boolean) value. If an empty map is provided, the initial state is set to 0. Defaults to an empty map.
[in]	graph_path	- File path at which to store the DOT state transition graph. No file is created if the path is left empty. Defaults to an empty path.
[in]	timeout	- Timeout for the underlying SAT solvers. Defaults to 600000 ms.

Returns

OK() and a map from each state to its successor states as well as the condition for the respective transition to be taken, an error otherwise.

Definition at line 381 of file solve_fsm.cpp.

References hal::BooleanFunction::clone(), hal::BooleanFunction::Concat(), hal::BooleanFunction::Const(), hal::BooleanFunction::Eq(), ERR, ERR_APPEND, generate_dot_graph(), hal::BooleanFunctionNetDecorator::get_boolean_variable(), test_plugin::graph_path, test_plugin::initial_state, test::n, hal::BooleanFunction::Not(), OK, hal::SMT::Solver::query(), test_plugin::timeout, hal::BooleanFunction::to_u64(), hal::SMT::Solver::with_constraint(), hal::SMT::QueryConfig::with_model_generation(), and hal::SMT::QueryConfig::with_timeout().

Referenced by hal::PYBIND11_PLUGIN().

solve_fsm_brute_force()

Result< std::map< u64, std::map< u64, BooleanFunction > > > hal::solve_fsm::solve_fsm_brute_force	(	Netlist *	nl,
		const std::vector< Gate * > &	state_reg,
		const std::vector< Gate * > &	transition_logic,
		const std::filesystem::path &	graph_path = ""
	)

Generate the state transition graph of a given FSM using brute force. The result is a map from each state of the FSM to all of its transitions. A transition is given as each successor state as well as the Boolean condition that needs to be fulfilled for the transition to take place. Optionally also produces a DOT file representing the state transition graph.

Parameters

[in]	nl	- The netlist to operate on.
[in]	state_reg	- A vector of flip-flop gates that make up the state register of the FSM.
[in]	transition_logic	- A vector of combinational gates that make up the transition logic of the FSM.
[in]	graph_path	- File path at which to store the DOT state transition graph. No file is created if the path is left empty. Defaults to an empty path.

Definition at line 285 of file solve_fsm.cpp.

References hal::BooleanFunction::Concat(), hal::BooleanFunction::Const(), ERR, ERR_APPEND, generate_dot_graph(), hal::BooleanFunctionNetDecorator::get_boolean_variable_name(), test_plugin::graph_path, OK, hal::BooleanFunction::size(), hal::state, hal::BooleanFunction::substitute(), hal::BooleanFunction::to_u64(), and hal::utils::to_vector().

Referenced by hal::PYBIND11_PLUGIN().