Solve FSM

Plugin to automatically generate FSM state transition graphs for given FSMs.

solve_fsm.solve_fsm(config: solve_fsm.Configuration) Optional[solve_fsm.StateTransitionGraph]

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

config (solve_fsm.Configuration) – The configuration of the FSM solver run.

Returns

The state transition graph of the FSM on success, None otherwise.

Return type

solve_fsm.StateTransitionGraph or None

class solve_fsm.SolveFsmPlugin

This class provides an interface to integrate FSM solving as a plugin within the HAL framework.

property description

The description of the plugin.

Type

str

get_description(self: solve_fsm.SolveFsmPlugin) str

Get the description of the plugin.

Returns

The description of the plugin.

Return type

str

get_name(self: solve_fsm.SolveFsmPlugin) str

Get the name of the plugin.

Returns

Plugin name.

Return type

str

get_version(self: solve_fsm.SolveFsmPlugin) str

Get the version of the plugin.

Returns

Plugin version.

Return type

str

property name

The name of the plugin.

Type

str

property version

The version of the plugin.

Type

str