hal::solve_fsm Namespace Reference

Recovers the state transition graph of a finite state machine from the gate-level netlist that implements it. More...

Classes
struct	Configuration
	The configuration of a run of the FSM solver. More...
struct	StateTransitionGraph
	The state transition graph of an FSM, i.e., the behavior that its netlist implements. More...

Functions
Result< StateTransitionGraph >	solve_fsm (const Configuration &config)
	Recover the state transition graph of an FSM from the netlist that implements it. More...

Detailed Description

Recovers the state transition graph of a finite state machine from the gate-level netlist that implements it.

Function Documentation

solve_fsm()

Result< StateTransitionGraph > hal::solve_fsm::solve_fsm

(

const Configuration &

config

)

Recover the state transition graph of an FSM from the netlist that implements it.

Explores the states that are reachable from the initial state and determines, for each of them, which successor states it can reach and under which condition. If outputs are configured, the value of each output in each state is computed as well.

No file is written. Use StateTransitionGraph::generate_dot_graph on the result to render the graph.

Parameters

[in]

config

- The configuration of the FSM solver run.

Returns

OK() and the state transition graph of the FSM on success, an error otherwise.

Definition at line 622 of file solve_fsm.cpp.

References hal::solve_fsm::Configuration::brute_force, ERR, ERR_APPEND, hal::Gate::get_id(), hal::Gate::get_name(), hal::solve_fsm::Configuration::initial_state, hal::solve_fsm::Configuration::netlist, hal::solve_fsm::StateTransitionGraph::netlist, OK, hal::solve_fsm::StateTransitionGraph::output_nets, hal::solve_fsm::Configuration::outputs, hal::solve_fsm::StateTransitionGraph::outputs, hal::state, hal::solve_fsm::Configuration::state_register, hal::solve_fsm::StateTransitionGraph::state_register, hal::solve_fsm::Configuration::timeout, hal::solve_fsm::Configuration::transition_logic, and hal::solve_fsm::StateTransitionGraph::transitions.

Referenced by hal::PYBIND11_PLUGIN().