The configuration of a run of the FSM solver. More...

#include </home/runner/work/hal/hal/plugins/solve_fsm/include/solve_fsm/configuration.h>

Collaboration diagram for hal::solve_fsm::Configuration:

Public Member Functions
	Configuration (Netlist *nl)
	Construct a new FSM solver configuration for the given netlist. More...

Configuration &	with_state_register (const std::vector< Gate * > &state_register)
	Set the flip-flops that make up the state register of the FSM. More...

Configuration &	with_transition_logic (const std::vector< Gate * > &transition_logic)
	Set the combinational gates that compute the next state of the FSM. More...

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. More...

Configuration &	with_initial_state (const std::map< Gate *, bool > &initial_state)
	Set the initial value of each flip-flop of the state register. More...

Configuration &	with_timeout (const u32 timeout)
	Set the timeout for the underlying SMT solver. More...

Configuration &	with_brute_force (const bool brute_force=true)
	Set whether to enumerate all states instead of using an SMT solver. More...

Public Attributes
Netlist *	netlist
	The netlist that implements the FSM. More...

std::vector< Gate * >	state_register = {}
	The flip-flops that make up the state register of the FSM. More...

std::vector< Gate * >	transition_logic = {}
	The combinational gates that compute the next state of the FSM. More...

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. More...

std::map< Gate *, bool >	initial_state = {}
	The initial value of each flip-flop of the state register. More...

u32	timeout = 600000
	The timeout for the underlying SMT solver in milliseconds. Defaults to 600000 ms. More...

bool	brute_force = false
	Enumerate all states instead of using an SMT solver. Defaults to `false`. More...

Detailed Description

The configuration of a run of the FSM solver.

Holds everything the solver needs to know about the FSM, including the netlist that implements it. The state register and the transition logic are mandatory, everything else is optional.

States are encoded as integers, with the first flip-flop of the state register providing the least significant bit.

Definition at line 58 of file configuration.h.

Constructor & Destructor Documentation

◆ Configuration()

hal::solve_fsm::Configuration::Configuration ( Netlist * nl )

Construct a new FSM solver configuration for the given netlist.

Parameters

[in] nl - The netlist that implements the FSM.

Definition at line 32 of file configuration.cpp.

Member Function Documentation

◆ with_brute_force()

Configuration & hal::solve_fsm::Configuration::with_brute_force ( const bool brute_force = true )

Set whether to enumerate all states instead of using an SMT solver.

Parameters

[in] brute_force - Set true to enumerate all states, false to use an SMT solver. Defaults to true.

Returns: The updated FSM solver configuration.

Definition at line 66 of file configuration.cpp.

References brute_force.

Referenced by hal::PYBIND11_PLUGIN().

◆ with_initial_state()

Configuration & hal::solve_fsm::Configuration::with_initial_state ( const std::map< Gate *, bool > & initial_state )

Set the initial value of each flip-flop of the state register.

Parameters

[in] initial_state - The initial value of each flip-flop of the state register.

Returns: The updated FSM solver configuration.

Definition at line 54 of file configuration.cpp.

References initial_state.

Referenced by hal::PYBIND11_PLUGIN().

◆ with_outputs()

Configuration & hal::solve_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.

Parameters

[in] outputs - The outputs, each given as a name and the nets that make up that output, least significant bit first.

Returns: The updated FSM solver configuration.

Definition at line 48 of file configuration.cpp.

References outputs.

Referenced by hal::PYBIND11_PLUGIN().

◆ with_state_register()

Configuration & hal::solve_fsm::Configuration::with_state_register ( const std::vector< Gate * > & state_register )

Set the flip-flops that make up the state register of the FSM.

Parameters

[in] state_register - The flip-flops of the state register, least significant bit first.

Returns: The updated FSM solver configuration.

Definition at line 36 of file configuration.cpp.

References state_register.

Referenced by hal::PYBIND11_PLUGIN().

◆ with_timeout()

Configuration & hal::solve_fsm::Configuration::with_timeout ( const u32 timeout )

Set the timeout for the underlying SMT solver.

Parameters

[in] timeout - The timeout in milliseconds.

Returns: The updated FSM solver configuration.

Definition at line 60 of file configuration.cpp.

References timeout.

Referenced by hal::PYBIND11_PLUGIN().

◆ with_transition_logic()

Configuration & hal::solve_fsm::Configuration::with_transition_logic ( const std::vector< Gate * > & transition_logic )

Set the combinational gates that compute the next state of the FSM.

Parameters

[in] transition_logic - The gates of the transition logic.

Returns: The updated FSM solver configuration.

Definition at line 42 of file configuration.cpp.

References transition_logic.

Referenced by hal::PYBIND11_PLUGIN().

Member Data Documentation

◆ brute_force

bool hal::solve_fsm::Configuration::brute_force = false

Enumerate all states instead of using an SMT solver. Defaults to false.

Brute forcing needs no external solver and is faster for small state registers, but its runtime doubles with every additional flip-flop. Both approaches produce the same state transition graph.

Definition at line 116 of file configuration.h.

Referenced by hal::PYBIND11_PLUGIN(), hal::solve_fsm::solve_fsm(), and with_brute_force().

◆ initial_state

std::map<Gate*, bool> hal::solve_fsm::Configuration::initial_state = {}

The initial value of each flip-flop of the state register.

Only states reachable from the resulting initial state are explored. Defaults to an empty map, in which case the FSM starts in state 0.

Definition at line 101 of file configuration.h.

Referenced by hal::PYBIND11_PLUGIN(), hal::solve_fsm::solve_fsm(), and with_initial_state().

◆ netlist

Netlist* hal::solve_fsm::Configuration::netlist

The netlist that implements the FSM.

Definition at line 70 of file configuration.h.

Referenced by hal::PYBIND11_PLUGIN(), and hal::solve_fsm::solve_fsm().

◆ outputs

std::vector<std::pair<std::string, std::vector<Net*> > > hal::solve_fsm::Configuration::outputs = {}

The outputs of the FSM, each given as a name and the nets that make up that output.

The first net of an output provides its least significant bit, so a single-bit output is a vector holding one net. Defaults to an empty vector, in which case no outputs are computed.

Definition at line 93 of file configuration.h.

Referenced by hal::PYBIND11_PLUGIN(), hal::solve_fsm::solve_fsm(), and with_outputs().

◆ state_register

std::vector<Gate*> hal::solve_fsm::Configuration::state_register = {}

The flip-flops that make up the state register of the FSM.

The first flip-flop provides the least significant bit of the state. Defaults to an empty vector, but a state register is required for the solver to run.

Definition at line 78 of file configuration.h.

Referenced by hal::PYBIND11_PLUGIN(), hal::solve_fsm::solve_fsm(), and with_state_register().

◆ timeout

u32 hal::solve_fsm::Configuration::timeout = 600000

The timeout for the underlying SMT solver in milliseconds. Defaults to 600000 ms.

Has no effect when brute_force is set, as no SMT solver is used then.

Definition at line 108 of file configuration.h.

Referenced by hal::PYBIND11_PLUGIN(), hal::solve_fsm::solve_fsm(), and with_timeout().

◆ transition_logic

std::vector<Gate*> hal::solve_fsm::Configuration::transition_logic = {}

The combinational gates that compute the next state of the FSM.

Defaults to an empty vector, but transition logic is required for the solver to run.

Definition at line 85 of file configuration.h.

Referenced by hal::PYBIND11_PLUGIN(), hal::solve_fsm::solve_fsm(), and with_transition_logic().

The documentation for this struct was generated from the following files:

plugins/solve_fsm/include/solve_fsm/configuration.h
plugins/solve_fsm/src/configuration.cpp

Public Member Functions

Public Attributes

Detailed Description

Constructor & Destructor Documentation

◆ Configuration()

Member Function Documentation

◆ with_brute_force()

◆ with_initial_state()

◆ with_outputs()

◆ with_state_register()

◆ with_timeout()

◆ with_transition_logic()

Member Data Documentation

◆ brute_force

◆ initial_state

◆ netlist

◆ outputs

◆ state_register

◆ timeout

◆ transition_logic