93 std::vector<std::pair<std::string, std::vector<Net*>>>
outputs = {};
Result< StateTransitionGraph > solve_fsm(const Configuration &config)
Recover the state transition graph of an FSM from the netlist that implements it.
The configuration of a run of the FSM solver.
Configuration & with_brute_force(const bool brute_force=true)
Set whether to enumerate all states instead of using an SMT solver.
Configuration & with_transition_logic(const std::vector< Gate * > &transition_logic)
Set the combinational gates that compute the next state of the FSM.
Configuration & with_timeout(const u32 timeout)
Set the timeout for the underlying SMT solver.
u32 timeout
The timeout for the underlying SMT solver in milliseconds. Defaults to 600000 ms.
std::vector< Gate * > state_register
The flip-flops that make up the state register of the FSM.
Configuration & with_outputs(const std::vector< std::pair< std::string, std::vector< Net * >>> &outputs)
Set the outputs of the FSM that the solver should evaluate in each state.
Configuration(Netlist *nl)
Construct a new FSM solver configuration for the given netlist.
Configuration & with_state_register(const std::vector< Gate * > &state_register)
Set the flip-flops that make up the state register of the FSM.
Netlist * netlist
The netlist that implements the FSM.
std::vector< std::pair< std::string, std::vector< Net * > > > outputs
The outputs of the FSM, each given as a name and the nets that make up that output.
Configuration & with_initial_state(const std::map< Gate *, bool > &initial_state)
Set the initial value of each flip-flop of the state register.
bool brute_force
Enumerate all states instead of using an SMT solver. Defaults to false.
std::map< Gate *, bool > initial_state
The initial value of each flip-flop of the state register.
std::vector< Gate * > transition_logic
The combinational gates that compute the next state of the FSM.