Skip to content

Commit

Permalink
clean up of the solve fsm plugin, same interface for the brute force …
Browse files Browse the repository at this point in the history 
…approach.
  • Loading branch information
@SimonKlx
SimonKlx committed Mar 8, 2023
1 parent 34b3567 commit e3c095e
Show file tree
Hide file tree
Showing 4 changed files with 261 additions and 198 deletions.
34 changes: 24 additions & 10 deletions plugins/solve_fsm/include/solve_fsm/plugin_solve_fsm.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,16 +45,17 @@ namespace hal
void initialize() override;

/**
* Generates the state graph of a finite state machine and returns a mapping from each state to a vector of all its possible transitions.
* A transition consits of a successor state and a vector of input mappings that lead to such a transition.
*
* 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.
*
* @param[in] nl - Pointer to the netlist.
* @param[in] state_reg - A vector containing all the gates of the fsm representing the state register.
* @param[in] transition_logic - A vector containing all the gates of the fsm representing the transition_logic.
* @param[in] initial_state - A mapping from the state registers to their initial value. If omitted the intial state will be set to 0.
* @param[in] graph_path - Path where the transition state graph in dot format is saved.
* @param[in] timeout - Timeout value for the sat solvers. Defaults to 600000 ms.
* @returns A mapping from each state to all its possible transitions. The transitions are a map from the successor state to all the possible input mappings that lead to it.
* @returns A mapping from each state to all its possible transitions.
*/
static Result<std::map<u64, std::map<u64, BooleanFunction>>> solve_fsm(Netlist* nl,
const std::vector<Gate*> state_reg,
Expand All @@ -64,15 +65,18 @@ namespace hal
const u32 timeout = 600000);

/**
* Generates the state graph of a finite state machine and returns a mapping from each state to a vector of all its possible successor states using a simple brute force approach.
*
* 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 burte force search to find all possible successors and afterwards computes the necessary conditions.
*
* @param[in] nl - Pointer to the netlist.
* @param[in] state_reg - A vector containing all the gates of the fsm representing the state register.
* @param[in] transition_logic - A vector containing all the gates of the fsm representing the transition_logic.
* @param[in] graph_path - Path where the transition state graph in dot format is saved.
* @returns A mapping from each state to all its possible successors states.
* @returns A mapping from each state to all its possible transitions.
*/
static Result<std::map<u64, std::set<u64>>> solve_fsm_brute_force(Netlist* nl, const std::vector<Gate*> state_reg, const std::vector<Gate*> transition_logic, const std::string graph_path = "");
static Result<std::map<u64, std::map<u64, BooleanFunction>>>
solve_fsm_brute_force(Netlist* nl, const std::vector<Gate*> state_reg, const std::vector<Gate*> transition_logic, const std::string graph_path = "");

/**
* Generates the state graph of a finite state machine from the transitions of that fsm.
Expand All @@ -84,7 +88,11 @@ namespace hal
* @param[in] base - The base with that the states are formatted and printed.
* @returns A string representing the dot graph.
*/
static Result<std::string> generate_dot_graph(const std::vector<Gate*>& state_reg, const std::map<u64, std::map<u64, BooleanFunction>>& transitions, const std::string& graph_path="", const u32 max_condition_length=128, const u32 base=10);
static Result<std::string> generate_dot_graph(const std::vector<Gate*>& state_reg,
const std::map<u64, std::map<u64, BooleanFunction>>& transitions,
const std::string& graph_path = "",
const u32 max_condition_length = 128,
const u32 base = 10);

/**
* Generates the state graph of a finite state machine from the transitions of that fsm.
Expand All @@ -96,6 +104,12 @@ namespace hal
* @param[in] base - The base with that the states are formatted and printed.
* @returns A string representing the dot graph.
*/
static Result<std::string> generate_dot_graph(const std::vector<Gate*>& state_reg, const std::map<u64, std::set<u64>>& transitions, const std::string& graph_path="", const u32 max_condition_length=128, const u32 base=10);
/*
static Result<std::string> generate_dot_graph(const std::vector<Gate*>& state_reg,
const std::map<u64, std::set<u64>>& transitions,
const std::string& graph_path = "",
const u32 max_condition_length = 128,
const u32 base = 10);
*/
};
} // namespace hal
145 changes: 91 additions & 54 deletions plugins/solve_fsm/python/python_bindings.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,62 +31,99 @@ namespace hal
.def("get_name", &SolveFsmPlugin::get_name)
.def_property_readonly("version", &SolveFsmPlugin::get_version)
.def("get_version", &SolveFsmPlugin::get_version)
.def_static("solve_fsm_brute_force", [](Netlist* nl, const std::vector<Gate*> state_reg, const std::vector<Gate*> transition_logic, const std::string graph_path="") -> std::optional<std::map<u64, std::set<u64>>> {
auto res = SolveFsmPlugin::solve_fsm_brute_force(nl, state_reg, transition_logic, graph_path);
if (res.is_ok())
{
return res.get();
}
else
{
log_error("python_context", "{}", res.get_error().get());
return std::nullopt;
}
}, py::arg("nl"), py::arg("state_reg"), py::arg("transition_logic"), py::arg("graph_path") = std::string(""), R"(
Generates the state graph of a finite state machine and returns a mapping from each state to all its possible successor states using a simple brute force approach.
:param halPy.Netlist nl: The netlist.
:param list[halPy.Gate] state_reg: A list containing all the gates of the fsm representing the state register.
:param list[halPy.Gate] transition_logic: A list containing all the gates of the fsm representing the transition_logic.
:param str graph_path: Path to the location where the state graph is saved in dot format.
:returns: A mapping from each state to all its possible successors states.
:rtype: dict()
.def_static(
"solve_fsm_brute_force",
[](Netlist* nl, const std::vector<Gate*> state_reg, const std::vector<Gate*> transition_logic, const std::string graph_path = "")
-> std::optional<std::map<u64, std::map<u64, BooleanFunction>>> {
auto res = SolveFsmPlugin::solve_fsm_brute_force(nl, state_reg, transition_logic, graph_path);
if (res.is_ok())
{
return res.get();
}
else
{
log_error("python_context", "{}", res.get_error().get());
return std::nullopt;
}
},
py::arg("nl"),
py::arg("state_reg"),
py::arg("transition_logic"),
py::arg("graph_path") = std::string(""),
R"(
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.
:param halPy.Netlist nl: The netlist.
:param list[halPy.Gate] state_reg: A list containing all the gates of the fsm representing the state register.
:param list[halPy.Gate] transition_logic: A list containing all the gates of the fsm representing the transition_logic.
:param str graph_path: Path to the location where the state graph is saved in dot format.
:returns: A mapping from each state to all its possible transitions.
:rtype: dict()
)")
.def_static("solve_fsm", [](Netlist* nl, const std::vector<Gate*> state_reg, const std::vector<Gate*> transition_logic, const std::map<Gate*, bool> initial_state={}, const std::string graph_path="", const u32 timeout=600000) -> std::optional<std::map<u64, std::map<u64, BooleanFunction>>> {
auto res = SolveFsmPlugin::solve_fsm(nl, state_reg, transition_logic, initial_state, graph_path, timeout);
if (res.is_ok())
{
return res.get();
}
else
{
log_error("python_context", "{}", res.get_error().get());
return std::nullopt;
}
}, py::arg("nl"), py::arg("state_reg"), py::arg("transition_logic"), py::arg("intial_state"), py::arg("graph_path"), py::arg("timeout"), R"(
Generates the state graph of a finite state machine and returns a mapping from each state to all its possible successor states using z3 as sat solver.
:param halPy.Netlist nl: The netlist.
:param list[halPy.Gate] state_reg: A list containing all the gates of the fsm representing the state register.
:param list[halPy.Gate] transition_logic: A list containing all the gates of the fsm representing the transition_logic.
:param dict{halPy.Gate, bool} initial_state: A mapping from the state registers to their initial value. If omitted the intial state will be set to 0.
:param str graph_path: Path to the location where the state graph is saved in dot format.
:param int timeout: Timeout value for the sat solver in seconds.
:returns: A mapping from each state to all its possible successors states
:rtype: dict()
.def_static(
"solve_fsm",
[](Netlist* nl,
const std::vector<Gate*> state_reg,
const std::vector<Gate*> transition_logic,
const std::map<Gate*, bool> initial_state = {},
const std::string graph_path = "",
const u32 timeout = 600000) -> std::optional<std::map<u64, std::map<u64, BooleanFunction>>> {
auto res = SolveFsmPlugin::solve_fsm(nl, state_reg, transition_logic, initial_state, graph_path, timeout);
if (res.is_ok())
{
return res.get();
}
else
{
log_error("python_context", "{}", res.get_error().get());
return std::nullopt;
}
},
py::arg("nl"),
py::arg("state_reg"),
py::arg("transition_logic"),
py::arg("intial_state"),
py::arg("graph_path"),
py::arg("timeout"),
R"(
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.
:param halPy.Netlist nl: The netlist.
:param list[halPy.Gate] state_reg: A list containing all the gates of the fsm representing the state register.
:param list[halPy.Gate] transition_logic: A list containing all the gates of the fsm representing the transition_logic.
:param dict{halPy.Gate, bool} initial_state: A mapping from the state registers to their initial value. If omitted the intial state will be set to 0.
:param str graph_path: Path to the location where the state graph is saved in dot format.
:param int timeout: Timeout value for the sat solver in seconds.
:returns: A mapping from each state to all its possible transitions.
)")
.def_static("generate_dot_graph", [](const std::vector<Gate*>& state_reg, const std::map<u64, std::map<u64, BooleanFunction>>& transitions, const std::string& graph_path="", const u32 max_condition_length=128, const u32 base=10) -> std::optional<std::string> {
auto res = SolveFsmPlugin::generate_dot_graph(state_reg, transitions, graph_path, max_condition_length, base);
if (res.is_ok())
{
return res.get();
}
else
{
log_error("python_context", "{}", res.get_error().get());
return std::nullopt;
}
}, py::arg("state_reg"), py::arg("transitions"), py::arg("graph_path") = std::string(""), py::arg("max_condition_length") = u32(128), py::arg("base") = u32(10), R"(
.def_static(
"generate_dot_graph",
[](const std::vector<Gate*>& state_reg,
const std::map<u64, std::map<u64, BooleanFunction>>& transitions,
const std::string& graph_path = "",
const u32 max_condition_length = 128,
const u32 base = 10) -> std::optional<std::string> {
auto res = SolveFsmPlugin::generate_dot_graph(state_reg, transitions, graph_path, max_condition_length, base);
if (res.is_ok())
{
return res.get();
}
else
{
log_error("python_context", "{}", res.get_error().get());
return std::nullopt;
}
},
py::arg("state_reg"),
py::arg("transitions"),
py::arg("graph_path") = std::string(""),
py::arg("max_condition_length") = u32(128),
py::arg("base") = u32(10),
R"(
Generates the state graph of a finite state machine from the transitions of that fsm.
:param list[halPy.Gate] state_reg: Vector contianing the state registers.
Expand Down
Loading

0 comments on commit e3c095e

Please sign in to comment.