Solve FSM
Plugin to automatically generate FSM state transition graphs for given FSMs.
- solve_fsm.generate_dot_graph(state_reg: List[hal_py.Gate], transitions: Dict[int, Dict[int, hal_py.BooleanFunction]], graph_path: str = '', max_condition_length: int = 128, base: int = 10) Optional[str]
Generates the state graph of a finite state machine from the transitions of that fsm.
- Parameters
state_reg (list[hal_py.Gate]) – Vector contianing the state registers.
transitions (dict[int, dict[int, hal_py.BooleanFunction]]) – Transitions of the fsm given as a map from origin state to all possible successor states and the corresponding condition.
graph_path (str) – Path to the location where the state graph is saved in dot format.
max_condition_length (int) – The maximum character length that is printed for boolean functions representing the conditions.
base (int) – The base with that the states are formatted and printed.
- Returns
A string representing the dot graph.
- Return type
- solve_fsm.solve_fsm(nl: hal_py.Netlist, state_reg: List[hal_py.Gate], transition_logic: List[hal_py.Gate], initial_state: Dict[hal_py.Gate, bool] = {}, graph_path: os.PathLike = '', timeout: int = 600000) Optional[Dict[int, Dict[int, hal_py.BooleanFunction]]]
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
nl (hal_py.Netlist) – The netlist to operate on.
state_reg (list[hal_py.Gate]) – A list of flip-flop gates that make up the state register of the FSM.
transition_logic (list[hal_py.Gate]) – A list of combinational gates that make up the transition logic of the FSM.
initial_state (dict[hal_py.Gate,bool]) – A dict from the state register flip-flops to their initial (Boolean) value. If an empty dict is provided, the initial state is set to 0. Defaults to an empty dict.
graph_path (pathlib.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.
timeout (int) – Timeout for the underlying SAT solvers. Defaults to 600000 ms.
- Returns
A dict from each state to its successor states as well as the condition for the respective transition to be taken on success, None otherwise.
- Return type
- solve_fsm.solve_fsm_brute_force(nl: hal_py.Netlist, state_reg: List[hal_py.Gate], transition_logic: List[hal_py.Gate], graph_path: str = '') Optional[Dict[int, Dict[int, hal_py.BooleanFunction]]]
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
nl (hal_py.Netlist) – The netlist to operate on.
state_reg (list[hal_py.Gate]) – A list of flip-flop gates that make up the state register of the FSM.
transition_logic (list[hal_py.Gate]) – A list of combinational gates that make up the transition logic of the FSM.
graph_path (pathlib.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.
- Returns
A dict from each state to its successor states as well as the condition for the respective transition to be taken on success, None otherwise.
- Return type
- class solve_fsm.SolveFsmPlugin
This class provides an interface to integrate FSM solving as a plugin within the HAL framework.
- get_description(self: solve_fsm.SolveFsmPlugin) str
Get the description of the plugin.
- Returns
The description of the plugin.
- Return type
- get_name(self: solve_fsm.SolveFsmPlugin) str
Get the name of the plugin.
- Returns
Plugin name.
- Return type
- get_version(self: solve_fsm.SolveFsmPlugin) str
Get the version of the plugin.
- Returns
Plugin version.
- Return type