Skip to content

Commit e3c095e

Browse files
SimonKlxSimonKlx
committed
clean up of the solve fsm plugin, same interface for the brute force approach.
1 parent 34b3567 commit e3c095e

File tree

4 files changed

+261
-198
lines changed

4 files changed

+261
-198
lines changed

‎plugins/solve_fsm/include/solve_fsm/plugin_solve_fsm.h‎

Lines changed: 24 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -45,16 +45,17 @@ namespace hal
4545
void initialize() override;
4646

4747
/**
48-
* Generates the state graph of a finite state machine and returns a mapping from each state to a vector of all its possible transitions.
49-
* A transition consits of a successor state and a vector of input mappings that lead to such a transition.
50-
*
48+
* Generates the state graph of a finite state machine and returns a mapping from each state to a all its possible transitions.
49+
* The transitions are another mapping from all the possible successor states to the corresponding condition under which the transition is taken.
50+
* This function uses an SMT solver to find all possible successors and afterwards computes the necessary conditions.
51+
*
5152
* @param[in] nl - Pointer to the netlist.
5253
* @param[in] state_reg - A vector containing all the gates of the fsm representing the state register.
5354
* @param[in] transition_logic - A vector containing all the gates of the fsm representing the transition_logic.
5455
* @param[in] initial_state - A mapping from the state registers to their initial value. If omitted the intial state will be set to 0.
5556
* @param[in] graph_path - Path where the transition state graph in dot format is saved.
5657
* @param[in] timeout - Timeout value for the sat solvers. Defaults to 600000 ms.
57-
* @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.
58+
* @returns A mapping from each state to all its possible transitions.
5859
*/
5960
static Result<std::map<u64, std::map<u64, BooleanFunction>>> solve_fsm(Netlist* nl,
6061
const std::vector<Gate*> state_reg,
@@ -64,15 +65,18 @@ namespace hal
6465
const u32 timeout = 600000);
6566

6667
/**
67-
* 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.
68-
*
68+
* Generates the state graph of a finite state machine and returns a mapping from each state to a all its possible transitions.
69+
* The transitions are another mapping from all the possible successor states to the corresponding condition under which the transition is taken.
70+
* This function uses a burte force search to find all possible successors and afterwards computes the necessary conditions.
71+
*
6972
* @param[in] nl - Pointer to the netlist.
7073
* @param[in] state_reg - A vector containing all the gates of the fsm representing the state register.
7174
* @param[in] transition_logic - A vector containing all the gates of the fsm representing the transition_logic.
7275
* @param[in] graph_path - Path where the transition state graph in dot format is saved.
73-
* @returns A mapping from each state to all its possible successors states.
76+
* @returns A mapping from each state to all its possible transitions.
7477
*/
75-
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 = "");
78+
static Result<std::map<u64, std::map<u64, BooleanFunction>>>
79+
solve_fsm_brute_force(Netlist* nl, const std::vector<Gate*> state_reg, const std::vector<Gate*> transition_logic, const std::string graph_path = "");
7680

7781
/**
7882
* Generates the state graph of a finite state machine from the transitions of that fsm.
@@ -84,7 +88,11 @@ namespace hal
8488
* @param[in] base - The base with that the states are formatted and printed.
8589
* @returns A string representing the dot graph.
8690
*/
87-
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);
91+
static Result<std::string> generate_dot_graph(const std::vector<Gate*>& state_reg,
92+
const std::map<u64, std::map<u64, BooleanFunction>>& transitions,
93+
const std::string& graph_path = "",
94+
const u32 max_condition_length = 128,
95+
const u32 base = 10);
8896

8997
/**
9098
* Generates the state graph of a finite state machine from the transitions of that fsm.
@@ -96,6 +104,12 @@ namespace hal
96104
* @param[in] base - The base with that the states are formatted and printed.
97105
* @returns A string representing the dot graph.
98106
*/
99-
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);
107+
/*
108+
static Result<std::string> generate_dot_graph(const std::vector<Gate*>& state_reg,
109+
const std::map<u64, std::set<u64>>& transitions,
110+
const std::string& graph_path = "",
111+
const u32 max_condition_length = 128,
112+
const u32 base = 10);
113+
*/
100114
};
101115
} // namespace hal

‎plugins/solve_fsm/python/python_bindings.cpp‎

Lines changed: 91 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -31,62 +31,99 @@ namespace hal
3131
.def("get_name", &SolveFsmPlugin::get_name)
3232
.def_property_readonly("version", &SolveFsmPlugin::get_version)
3333
.def("get_version", &SolveFsmPlugin::get_version)
34-
.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>>> {
35-
auto res = SolveFsmPlugin::solve_fsm_brute_force(nl, state_reg, transition_logic, graph_path);
36-
if (res.is_ok())
37-
{
38-
return res.get();
39-
}
40-
else
41-
{
42-
log_error("python_context", "{}", res.get_error().get());
43-
return std::nullopt;
44-
}
45-
}, py::arg("nl"), py::arg("state_reg"), py::arg("transition_logic"), py::arg("graph_path") = std::string(""), R"(
46-
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.
47-
48-
:param halPy.Netlist nl: The netlist.
49-
:param list[halPy.Gate] state_reg: A list containing all the gates of the fsm representing the state register.
50-
:param list[halPy.Gate] transition_logic: A list containing all the gates of the fsm representing the transition_logic.
51-
:param str graph_path: Path to the location where the state graph is saved in dot format.
52-
:returns: A mapping from each state to all its possible successors states.
53-
:rtype: dict()
34+
.def_static(
35+
"solve_fsm_brute_force",
36+
[](Netlist* nl, const std::vector<Gate*> state_reg, const std::vector<Gate*> transition_logic, const std::string graph_path = "")
37+
-> std::optional<std::map<u64, std::map<u64, BooleanFunction>>> {
38+
auto res = SolveFsmPlugin::solve_fsm_brute_force(nl, state_reg, transition_logic, graph_path);
39+
if (res.is_ok())
40+
{
41+
return res.get();
42+
}
43+
else
44+
{
45+
log_error("python_context", "{}", res.get_error().get());
46+
return std::nullopt;
47+
}
48+
},
49+
py::arg("nl"),
50+
py::arg("state_reg"),
51+
py::arg("transition_logic"),
52+
py::arg("graph_path") = std::string(""),
53+
R"(
54+
Generates the state graph of a finite state machine and returns a mapping from each state to a all its possible transitions.
55+
The transitions are another mapping from all the possible successor states to the corresponding condition under which the transition is taken.
56+
This function uses a brute force approach to find all possible successors and afterwards computes the necessary conditions.
57+
58+
:param halPy.Netlist nl: The netlist.
59+
:param list[halPy.Gate] state_reg: A list containing all the gates of the fsm representing the state register.
60+
:param list[halPy.Gate] transition_logic: A list containing all the gates of the fsm representing the transition_logic.
61+
:param str graph_path: Path to the location where the state graph is saved in dot format.
62+
:returns: A mapping from each state to all its possible transitions.
63+
:rtype: dict()
5464
)")
55-
.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>>> {
56-
auto res = SolveFsmPlugin::solve_fsm(nl, state_reg, transition_logic, initial_state, graph_path, timeout);
57-
if (res.is_ok())
58-
{
59-
return res.get();
60-
}
61-
else
62-
{
63-
log_error("python_context", "{}", res.get_error().get());
64-
return std::nullopt;
65-
}
66-
}, py::arg("nl"), py::arg("state_reg"), py::arg("transition_logic"), py::arg("intial_state"), py::arg("graph_path"), py::arg("timeout"), R"(
67-
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.
68-
69-
:param halPy.Netlist nl: The netlist.
70-
:param list[halPy.Gate] state_reg: A list containing all the gates of the fsm representing the state register.
71-
:param list[halPy.Gate] transition_logic: A list containing all the gates of the fsm representing the transition_logic.
72-
: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.
73-
:param str graph_path: Path to the location where the state graph is saved in dot format.
74-
:param int timeout: Timeout value for the sat solver in seconds.
75-
:returns: A mapping from each state to all its possible successors states
76-
:rtype: dict()
65+
.def_static(
66+
"solve_fsm",
67+
[](Netlist* nl,
68+
const std::vector<Gate*> state_reg,
69+
const std::vector<Gate*> transition_logic,
70+
const std::map<Gate*, bool> initial_state = {},
71+
const std::string graph_path = "",
72+
const u32 timeout = 600000) -> std::optional<std::map<u64, std::map<u64, BooleanFunction>>> {
73+
auto res = SolveFsmPlugin::solve_fsm(nl, state_reg, transition_logic, initial_state, graph_path, timeout);
74+
if (res.is_ok())
75+
{
76+
return res.get();
77+
}
78+
else
79+
{
80+
log_error("python_context", "{}", res.get_error().get());
81+
return std::nullopt;
82+
}
83+
},
84+
py::arg("nl"),
85+
py::arg("state_reg"),
86+
py::arg("transition_logic"),
87+
py::arg("intial_state"),
88+
py::arg("graph_path"),
89+
py::arg("timeout"),
90+
R"(
91+
Generates the state graph of a finite state machine and returns a mapping from each state to a all its possible transitions.
92+
The transitions are another mapping from all the possible successor states to the corresponding condition under which the transition is taken.
93+
This function uses an SMT solver to find all possible successors and afterwards computes the necessary conditions.
94+
95+
:param halPy.Netlist nl: The netlist.
96+
:param list[halPy.Gate] state_reg: A list containing all the gates of the fsm representing the state register.
97+
:param list[halPy.Gate] transition_logic: A list containing all the gates of the fsm representing the transition_logic.
98+
: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.
99+
:param str graph_path: Path to the location where the state graph is saved in dot format.
100+
:param int timeout: Timeout value for the sat solver in seconds.
101+
:returns: A mapping from each state to all its possible transitions.
77102
)")
78-
.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> {
79-
auto res = SolveFsmPlugin::generate_dot_graph(state_reg, transitions, graph_path, max_condition_length, base);
80-
if (res.is_ok())
81-
{
82-
return res.get();
83-
}
84-
else
85-
{
86-
log_error("python_context", "{}", res.get_error().get());
87-
return std::nullopt;
88-
}
89-
}, 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"(
103+
.def_static(
104+
"generate_dot_graph",
105+
[](const std::vector<Gate*>& state_reg,
106+
const std::map<u64, std::map<u64, BooleanFunction>>& transitions,
107+
const std::string& graph_path = "",
108+
const u32 max_condition_length = 128,
109+
const u32 base = 10) -> std::optional<std::string> {
110+
auto res = SolveFsmPlugin::generate_dot_graph(state_reg, transitions, graph_path, max_condition_length, base);
111+
if (res.is_ok())
112+
{
113+
return res.get();
114+
}
115+
else
116+
{
117+
log_error("python_context", "{}", res.get_error().get());
118+
return std::nullopt;
119+
}
120+
},
121+
py::arg("state_reg"),
122+
py::arg("transitions"),
123+
py::arg("graph_path") = std::string(""),
124+
py::arg("max_condition_length") = u32(128),
125+
py::arg("base") = u32(10),
126+
R"(
90127
Generates the state graph of a finite state machine from the transitions of that fsm.
91128
92129
:param list[halPy.Gate] state_reg: Vector contianing the state registers.

0 commit comments

Comments
 (0)