Solve FSM

class solve_fsm.SolveFsmPlugin
static 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.
  • dict[int, hal_py.BooleanFunction]] transitions (dict[int,) – 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:

str
get_name(self: solve_fsm.SolveFsmPlugin) → str
get_version(self: solve_fsm.SolveFsmPlugin) → str
static solve_fsm(nl: hal_py.Netlist, state_reg: List[hal_py.Gate], transition_logic: List[hal_py.Gate], intial_state: Dict[hal_py.Gate, bool] = {}, graph_path: str = '', timeout: int = 600000) → Optional[Dict[int, Dict[int, hal_py.BooleanFunction]]]

Generates the state graph of a finite state machine and returns a mapping from each state to a all its possible transitions. The transitions are another mapping from all the possible successor states to the corresponding condition under which the transition is taken. This function uses an SMT solver to find all possible successors and afterwards computes the necessary conditions.

Parameters:
  • nl (hal_py.Netlist) – The netlist.
  • state_reg (list[hal_py.Gate]) – A list containing all the gates of the fsm representing the state register.
  • transition_logic (list[hal_py.Gate]) – A list containing all the gates of the fsm representing the transition_logic.
  • initial_state (dict[hal_py.Gate,bool]) – A mapping from the state registers to their initial value. If omitted the intial state will be set to 0.
  • graph_path (str) – Path to the location where the state graph is saved in dot format.
  • timeout (int) – Timeout value for the sat solver in seconds.
Returns:

A mapping from each state to all its possible transitions.
Return type:

dict[int,dict[int,hal_py.BooleanFunction]]
static 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]]]

Generates the state graph of a finite state machine and returns a mapping from each state to a all its possible transitions. The transitions are another mapping from all the possible successor states to the corresponding condition under which the transition is taken. This function uses a brute force approach to find all possible successors and afterwards computes the necessary conditions.

Parameters:
  • nl (hal_py.Netlist) – The netlist.
  • state_reg (list[hal_py.Gate]) – A list containing all the gates of the fsm representing the state register.
  • transition_logic (list[hal_py.Gate]) – A list containing all the gates of the fsm representing the transition_logic.
  • graph_path (str) – Path to the location where the state graph is saved in dot format.
Returns:

A mapping from each state to all its possible transitions.
Return type:

dict[int,dict[int,hal_py.BooleanFunction]]