From e3c095eabc6cece489497fa0658ed1ec168a30cf Mon Sep 17 00:00:00 2001 From: Simon Date: Wed, 8 Mar 2023 12:09:00 +0100 Subject: [PATCH] clean up of the solve fsm plugin, same interface for the brute force approach. --- .../include/solve_fsm/plugin_solve_fsm.h | 34 ++- plugins/solve_fsm/python/python_bindings.cpp | 145 ++++++---- plugins/solve_fsm/src/plugin_solve_fsm.cpp | 258 +++++++++--------- plugins/solve_fsm/test_plugin.py | 22 +- 4 files changed, 261 insertions(+), 198 deletions(-) diff --git a/plugins/solve_fsm/include/solve_fsm/plugin_solve_fsm.h b/plugins/solve_fsm/include/solve_fsm/plugin_solve_fsm.h index 1da17150e01..f631c600c63 100644 --- a/plugins/solve_fsm/include/solve_fsm/plugin_solve_fsm.h +++ b/plugins/solve_fsm/include/solve_fsm/plugin_solve_fsm.h @@ -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>> solve_fsm(Netlist* nl, const std::vector state_reg, @@ -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>> solve_fsm_brute_force(Netlist* nl, const std::vector state_reg, const std::vector transition_logic, const std::string graph_path = ""); + static Result>> + solve_fsm_brute_force(Netlist* nl, const std::vector state_reg, const std::vector transition_logic, const std::string graph_path = ""); /** * Generates the state graph of a finite state machine from the transitions of that fsm. @@ -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 generate_dot_graph(const std::vector& state_reg, const std::map>& transitions, const std::string& graph_path="", const u32 max_condition_length=128, const u32 base=10); + static Result generate_dot_graph(const std::vector& state_reg, + const std::map>& 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. @@ -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 generate_dot_graph(const std::vector& state_reg, const std::map>& transitions, const std::string& graph_path="", const u32 max_condition_length=128, const u32 base=10); + /* + static Result generate_dot_graph(const std::vector& state_reg, + const std::map>& transitions, + const std::string& graph_path = "", + const u32 max_condition_length = 128, + const u32 base = 10); + */ }; } // namespace hal diff --git a/plugins/solve_fsm/python/python_bindings.cpp b/plugins/solve_fsm/python/python_bindings.cpp index a3549ad4334..d81cec97185 100644 --- a/plugins/solve_fsm/python/python_bindings.cpp +++ b/plugins/solve_fsm/python/python_bindings.cpp @@ -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 state_reg, const std::vector transition_logic, const std::string graph_path="") -> std::optional>> { - 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 state_reg, const std::vector transition_logic, const std::string graph_path = "") + -> std::optional>> { + 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 state_reg, const std::vector transition_logic, const std::map initial_state={}, const std::string graph_path="", const u32 timeout=600000) -> std::optional>> { - 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 state_reg, + const std::vector transition_logic, + const std::map initial_state = {}, + const std::string graph_path = "", + const u32 timeout = 600000) -> std::optional>> { + 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& state_reg, const std::map>& transitions, const std::string& graph_path="", const u32 max_condition_length=128, const u32 base=10) -> std::optional { - 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& state_reg, + const std::map>& transitions, + const std::string& graph_path = "", + const u32 max_condition_length = 128, + const u32 base = 10) -> std::optional { + 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. diff --git a/plugins/solve_fsm/src/plugin_solve_fsm.cpp b/plugins/solve_fsm/src/plugin_solve_fsm.cpp index 35cf3c0024e..9c4833118c6 100644 --- a/plugins/solve_fsm/src/plugin_solve_fsm.cpp +++ b/plugins/solve_fsm/src/plugin_solve_fsm.cpp @@ -2,6 +2,7 @@ #include "hal_core/netlist/boolean_function.h" #include "hal_core/netlist/boolean_function/solver.h" +#include "hal_core/netlist/decorators/boolean_function_decorator.h" #include "hal_core/netlist/decorators/boolean_function_net_decorator.h" #include "hal_core/netlist/decorators/subgraph_netlist_decorator.h" #include "hal_core/netlist/endpoint.h" @@ -43,6 +44,7 @@ namespace hal namespace { + // generates a list of state flip flop output nets and the corresponding boolean function at their data input Result>> generate_state_bfs(Netlist* nl, const std::vector state_reg, const std::vector transition_logic) { std::map output_net_to_input_net; @@ -52,7 +54,8 @@ namespace hal const std::vector d_ports = ff->get_type()->get_pins([](const GatePin* pin) { return pin->get_type() == PinType::data; }); if (d_ports.size() != 1) { - return ERR("failed to create input - output mapping: currently not supporting flip-flops with multiple or no data inputs, but found " + std::to_string(d_ports.size()) + " for gate type " + ff->get_type()->get_name() + "."); + return ERR("failed to create input - output mapping: currently not supporting flip-flops with multiple or no data inputs, but found " + std::to_string(d_ports.size()) + + " for gate type " + ff->get_type()->get_name() + "."); } hal::Net* input_net; @@ -74,7 +77,7 @@ namespace hal std::vector> state_bfs; const std::vector subgraph_gates = {transition_logic.begin(), transition_logic.end()}; - const auto nl_dec = SubgraphNetlistDecorator(*nl); + const auto nl_dec = SubgraphNetlistDecorator(*nl); for (const auto& ff : state_reg) { @@ -85,51 +88,15 @@ namespace hal BooleanFunction bf; if (auto res = nl_dec.get_subgraph_function(subgraph_gates, input_net); res.is_error()) { - return ERR_APPEND(res.get_error(), "failed to generate boolean functions of state: could not generate subgraph function for state net " + std::to_string(input_net->get_id()) + "."); + return ERR_APPEND(res.get_error(), + "failed to generate boolean functions of state: could not generate subgraph function for state net " + std::to_string(input_net->get_id()) + "."); } else { bf = res.get(); } - - // replace all vcc and gnd nets with constant zeros and ones - for (const auto& gnd_gate : nl->get_gnd_gates()) - { - if (gnd_gate->get_fan_out_nets().size() != 1) - { - return ERR("failed to generate boolean functions of state: found GND gate " + std::to_string(gnd_gate->get_id()) + " with " + std::to_string(gnd_gate->get_fan_out_nets().size()) + " fan-out nets, but can handle only one."); - } - - Net* gnd_net = gnd_gate->get_fan_out_nets().at(0); - if (auto res = bf.substitute(BooleanFunctionNetDecorator(*gnd_net).get_boolean_variable_name(), BooleanFunction::Const(0, 1)); res.is_error()) - { - return ERR("failed to generate boolean functions of state: unable to replace GND net " + std::to_string(gnd_net->get_id()) + " with constant."); - } - else - { - bf = res.get(); - } - } - - for (const auto& vcc_gate : nl->get_vcc_gates()) - { - if (vcc_gate->get_fan_out_nets().size() != 1) - { - return ERR("failed to generate boolean functions of state: found VCC gate " + std::to_string(vcc_gate->get_id()) + " with " + std::to_string(vcc_gate->get_fan_out_nets().size()) + " fan-out nets, but can handle only one."); - } - - Net* vcc_net = vcc_gate->get_fan_out_nets().at(0); - - if (auto res = bf.substitute(BooleanFunctionNetDecorator(*vcc_net).get_boolean_variable_name(), BooleanFunction::Const(1, 1)); res.is_error()) - { - return ERR("failed to generate boolean functions of state: unable to replace VCC net " + std::to_string(vcc_net->get_id()) + " with constant."); - } - else - { - bf = res.get(); - } - } + BooleanFunctionDecorator(bf).substitute_power_ground_nets(nl); bf.simplify(); @@ -171,13 +138,64 @@ namespace hal state_bfs.push_back({input_net, bf}); } - + return OK(state_bfs); } - } // namespace + // takes a map of unconditional transitions and reconstructs the conditions under which each condition is taken + Result>> generate_conditional_transitions(const std::vector>& state_bfs, + const std::map>& transitions) + { + // generate all transitions that are reachable from the inital state. + std::map> conditional_transitions; + + // for all possible and previously found successor states we build the condition to reach them + for (const auto& [prev, successors] : transitions) + { + // this builds a mapping for all the output net variables of the state vector to the current starting state + std::map prev_mapping; + for (u32 i = 0; i < state_bfs.size(); i++) + { + prev_mapping.insert( + {BooleanFunctionNetDecorator(*(state_bfs.at(i).first)).get_boolean_variable_name(), ((prev >> i) & 1) ? BooleanFunction::Const(1, 1) : BooleanFunction::Const(0, 1)}); + } + + for (const auto& suc : successors) + { + // this all the boolean functions of incoming data nets to the state vector either vanilla incase the corresponding state bit is 1 in the successor state or negated incase the state bit is 0 in the successor state. + BooleanFunction condition; + + for (u32 i = 0; i < state_bfs.size(); i++) + { + auto next_state_bit_bf = ((suc >> i) & 1) ? state_bfs.at(i).second : BooleanFunction::Not(state_bfs.at(i).second.clone(), 1).get(); + + if (condition.is_empty()) + { + condition = next_state_bit_bf; + } + else + { + condition = BooleanFunction::And(std::move(condition), std::move(next_state_bit_bf), 1).get(); + } + } + + // replace all the variables of the previous state with their real values for our current state n and simplify. + condition = condition.substitute(prev_mapping).get(); + + // we are left with a condition that only includes the inputs to the fsm that needs to be fullfilled to reach the successor state from state n. + condition = condition.simplify(); + + conditional_transitions[prev].insert({suc, condition}); + } + } + + return OK(conditional_transitions); + } + + } // namespace - Result>> SolveFsmPlugin::solve_fsm_brute_force(Netlist* nl, const std::vector state_reg, const std::vector transition_logic, const std::string graph_path) + Result>> + SolveFsmPlugin::solve_fsm_brute_force(Netlist* nl, const std::vector state_reg, const std::vector transition_logic, const std::string graph_path) { const u32 state_size = state_reg.size(); if (state_size > 64) @@ -186,7 +204,7 @@ namespace hal } // extract Boolean functions for each state flip-flop - const auto state_bfs_res = generate_state_bfs(nl, state_reg, transition_logic); + const auto state_bfs_res = generate_state_bfs(nl, state_reg, transition_logic); if (state_bfs_res.is_error()) { return ERR_APPEND(state_bfs_res.get_error(), "failed to solve fsm: unable to generate Boolean functions for state."); @@ -197,7 +215,7 @@ namespace hal BooleanFunction next_state_vec = state_bfs.front().second; for (u32 i = 1; i < state_reg.size(); i++) { - next_state_vec = BooleanFunction::Concat(state_bfs.at(i).second.clone(), std::move(next_state_vec), next_state_vec.size() +1 ).get(); + next_state_vec = BooleanFunction::Concat(state_bfs.at(i).second.clone(), std::move(next_state_vec), next_state_vec.size() + 1).get(); } std::map> all_transitions; @@ -220,7 +238,7 @@ namespace hal } const auto state_bf = sub_res.get().simplify(); - const auto inputs = utils::to_vector(state_bf.get_variable_names()); + const auto inputs = utils::to_vector(state_bf.get_variable_names()); // brute force over all external inputs for (u64 input_val = 0; input_val < (u64(1) << inputs.size()); input_val++) @@ -252,23 +270,25 @@ namespace hal } } + const auto conditional_transitions = generate_conditional_transitions(state_bfs, all_transitions).get(); + /* DEBUG PRINTING */ - for (const auto& [org, successors] : all_transitions) + for (const auto& [org, successors] : conditional_transitions) { std::cout << org << ": " << std::endl; - for (const auto& suc : successors) + for (const auto& [suc, condition] : successors) { - std::cout << "\t" << suc << std::endl; + std::cout << "\t" << suc << ": " << condition.to_string() << std::endl; } } /* END DEBUG PRINTING */ - if (auto graph_res = generate_dot_graph(state_reg, all_transitions, graph_path, 0); graph_res.is_error()) + if (auto graph_res = generate_dot_graph(state_reg, conditional_transitions, graph_path); graph_res.is_error()) { return ERR_APPEND(graph_res.get_error(), "failed to solve fsm: unable to generate dot graph."); } - - return OK(all_transitions); + + return OK(conditional_transitions); } Result>> SolveFsmPlugin::solve_fsm(Netlist* nl, @@ -285,7 +305,7 @@ namespace hal } // extract Boolean functions for each state flip-flop - const auto state_bfs_res = generate_state_bfs(nl, state_reg, transition_logic); + const auto state_bfs_res = generate_state_bfs(nl, state_reg, transition_logic); if (state_bfs_res.is_error()) { return ERR_APPEND(state_bfs_res.get_error(), "failed to solve fsm: unable to generate Boolean functions for state."); @@ -297,12 +317,12 @@ namespace hal for (u32 i = 1; i < state_reg.size(); i++) { // bitvector representing the previous state - prev_state_vec = BooleanFunction::Concat(BooleanFunctionNetDecorator(*(state_bfs.at(i).first)).get_boolean_variable(), std::move(prev_state_vec), i+1).get(); - + prev_state_vec = BooleanFunction::Concat(BooleanFunctionNetDecorator(*(state_bfs.at(i).first)).get_boolean_variable(), std::move(prev_state_vec), i + 1).get(); + // bitvector including all the functions to calculate the next state - next_state_vec = BooleanFunction::Concat(state_bfs.at(i).second.clone(), std::move(next_state_vec), i+1).get(); + next_state_vec = BooleanFunction::Concat(state_bfs.at(i).second.clone(), std::move(next_state_vec), i + 1).get(); } - + // generate initial state u64 initial_state_num = 0; if (!initial_state.empty()) @@ -320,7 +340,7 @@ namespace hal } // generate all transitions that are reachable from the inital state. - std::map> all_transitions; + std::map> all_transitions; std::deque q; std::unordered_set visited; @@ -342,9 +362,11 @@ namespace hal // generate new transitions and add them to the queue SMT::Solver s; + + // set prev_state_vec to starting state s = s.with_constraint(SMT::Constraint{prev_state_vec.clone(), BooleanFunction::Const(n, state_size)}); - while(true) + while (true) { if (auto res = s.query(SMT::QueryConfig().with_model_generation().with_timeout(timeout)); res.is_error()) { @@ -353,7 +375,7 @@ namespace hal else { auto s_res = res.get(); - + if (s_res.is_unsat()) { break; @@ -363,17 +385,20 @@ namespace hal { return ERR("failed to solve fsm: received an unknown solver result for state " + std::to_string(n) + "."); } - - auto m = s_res.model.value(); - auto suc = m.evaluate(next_state_vec).get(); + auto m = s_res.model.value(); + auto suc = m.evaluate(next_state_vec).get(); + auto suc_num = 0; + + // a constant (numeral) successor state if (suc.is_constant()) { - successor_states.push_back(suc.get_constant_value().get()); - s = s.with_constraint(SMT::Constraint(BooleanFunction::Not(BooleanFunction::Eq(next_state_vec.clone(), suc.clone(), 1).get(), 1).get())); + suc_num = suc.get_constant_value().get(); } + // a successor state that includes boolean functions (for example in form of input variables) else { + // to resolve such a successor state, we simpply set all variables left in the state to zero (which is one possible solution) and continue to search for more valid solutions std::unordered_map> zero_mapping; for (const auto& var : suc.get_variable_names()) { @@ -382,50 +407,25 @@ namespace hal if (auto eval_res = suc.evaluate(zero_mapping); eval_res.is_error()) { - return ERR_APPEND(eval_res.get_error(), "failed to solve fsm: could not evaluate successors state to constant."); + return ERR_APPEND(eval_res.get_error(), "failed to solve fsm: could not evaluate successor state to constant."); } else { - const auto suc_num = BooleanFunction::to_u64(eval_res.get()).get(); - successor_states.push_back(suc_num); - s = s.with_constraint(SMT::Constraint(BooleanFunction::Not(BooleanFunction::Eq(next_state_vec.clone(), BooleanFunction::Const(suc_num, eval_res.get().size()), 1).get(), 1).get())); + suc_num = BooleanFunction::to_u64(eval_res.get()).get(); } } - } - } - - for (const auto& suc : successor_states) - { - // generate n mapping - std::map n_mapping; - BooleanFunction condition; - - for (u32 i = 0; i < state_reg.size(); i++) - { - n_mapping.insert({BooleanFunctionNetDecorator(*(state_bfs.at(i).first)).get_boolean_variable_name(), ((n >> i) & 1) ? BooleanFunction::Const(1, 1): BooleanFunction::Const(0, 1)}); - auto next_state_bit_bf = ((suc >> i) & 1) ? state_bfs.at(i).second : BooleanFunction::Not(state_bfs.at(i).second.clone(), 1).get(); - - if (condition.is_empty()) - { - condition = next_state_bit_bf; - } - else - { - condition = BooleanFunction::And(std::move(condition), std::move(next_state_bit_bf), 1).get(); - } + q.push_back(suc_num); + all_transitions[n].insert(suc_num); + s = s.with_constraint(SMT::Constraint(BooleanFunction::Not(BooleanFunction::Eq(next_state_vec.clone(), BooleanFunction::Const(suc_num, suc.size()), 1).get(), 1).get())); } - - condition = condition.substitute(n_mapping).get(); - condition = condition.simplify(); - - all_transitions[n].insert({suc, condition}); - q.push_back(suc); } } + const auto conditional_transitions = generate_conditional_transitions(state_bfs, all_transitions).get(); + /* DEBUG PRINTING */ - for (const auto& [org, successors] : all_transitions) + for (const auto& [org, successors] : conditional_transitions) { std::cout << org << ": " << std::endl; for (const auto& [suc, condition] : successors) @@ -435,30 +435,19 @@ namespace hal } /* END DEBUG PRINTING */ - if (auto graph_res = generate_dot_graph(state_reg, all_transitions, graph_path); graph_res.is_error()) + if (auto graph_res = generate_dot_graph(state_reg, conditional_transitions, graph_path); graph_res.is_error()) { return ERR_APPEND(graph_res.get_error(), "failed to solve fsm: unable to generate dot graph."); } - - return OK(all_transitions); - } - Result SolveFsmPlugin::generate_dot_graph(const std::vector& state_reg, const std::map>& transitions, const std::string& graph_path, const u32 max_condition_length, const u32 base) - { - std::map> dummy_conditional_transitions; - - for (const auto& [org, successors] : transitions) - { - for (const auto& suc : successors) - { - dummy_conditional_transitions[org].insert({suc, BooleanFunction()}); - } - } - - return generate_dot_graph(state_reg, dummy_conditional_transitions, graph_path, max_condition_length, base); - } + return OK(conditional_transitions); + } - Result SolveFsmPlugin::generate_dot_graph(const std::vector& state_reg, const std::map>& transitions, const std::string& graph_path, const u32 max_condition_length, const u32 base) + Result SolveFsmPlugin::generate_dot_graph(const std::vector& state_reg, + const std::map>& transitions, + const std::string& graph_path, + const u32 max_condition_length, + const u32 base) { auto generate_legend = [](const std::vector& reg) -> std::string { std::string name_str = ""; @@ -484,21 +473,23 @@ namespace hal std::string start_name; std::string end_name; - switch(base) + switch (base) { case 2: start_name = std::bitset<64>(org).to_string().substr(64 - state_reg.size(), 64); - end_name = std::bitset<64>(suc).to_string().substr(64 - state_reg.size(), 64); + end_name = std::bitset<64>(suc).to_string().substr(64 - state_reg.size(), 64); break; case 10: start_name = std::to_string(org); - end_name = std::to_string(suc); + end_name = std::to_string(suc); break; default: return ERR("failed to generate dot graph: base " + std::to_string(base) + "not implemented."); } - graph_str += start_name+ " -> " + end_name + "[label=\"" + cond.to_string().substr(0, max_condition_length) + "\", weight=\"" + cond.to_string().substr(0, max_condition_length) + "\"];\n";; + graph_str += + start_name + " -> " + end_name + "[label=\"" + cond.to_string().substr(0, max_condition_length) + "\", weight=\"" + cond.to_string().substr(0, max_condition_length) + "\"];\n"; + ; } } @@ -515,8 +506,29 @@ namespace hal ofs << graph_str; ofs.close(); } - + return OK(graph_str); } + /* + Result SolveFsmPlugin::generate_dot_graph(const std::vector& state_reg, + const std::map>& transitions, + const std::string& graph_path, + const u32 max_condition_length, + const u32 base) + { + std::map> dummy_conditional_transitions; + + for (const auto& [org, successors] : transitions) + { + for (const auto& suc : successors) + { + dummy_conditional_transitions[org].insert({suc, BooleanFunction()}); + } + } + + return generate_dot_graph(state_reg, dummy_conditional_transitions, graph_path, max_condition_length, base); + } + */ + } // namespace hal \ No newline at end of file diff --git a/plugins/solve_fsm/test_plugin.py b/plugins/solve_fsm/test_plugin.py index e142fd5cce7..43e579080c8 100644 --- a/plugins/solve_fsm/test_plugin.py +++ b/plugins/solve_fsm/test_plugin.py @@ -2,34 +2,34 @@ import sys, os #some necessary configuration: -sys.path.append("/home/simon/projects/hal/build/lib/") #this is where your hal python lib is located -os.environ["HAL_BASE_PATH"] = "/home/simon/projects/hal/build" # hal base path -import hal_py +base_path = "/home/simon/projects/hal/" -netlist_to_read = "netlist.v" -gate_library_path = "gate_library.lib" +sys.path.append(base_path + "build/lib/") #this is where your hal python lib is located +os.environ["HAL_BASE_PATH"] = base_path + "build" # hal base path +import hal_py #initialize HAL hal_py.plugin_manager.load_all_plugins() #read netlist -netlist = hal_py.NetlistFactory.load_netlist(netlist_to_read, gate_library_path) + +netlist = hal_py.NetlistFactory.load_netlist(base_path + "examples/fsm/fsm.v", base_path + "examples/fsm/example_library.hgl") from hal_plugins import solve_fsm pl_fsm = hal_py.plugin_manager.get_plugin_instance("solve_fsm") # UPDATE THE MODULE IDS OR CREATE YOUR OWN LIST OF GATES -state_mod = netlist.get_module_by_id(0) -transition_mod = netlist.get_module_by_id(0) +fsm_mod = netlist.get_module_by_id(1) -transition_gates = transition_mod.gates -state_gates = state_mod.gates +transition_gates = fsm_mod.get_gates(lambda g : g.type.has_property(hal_py.GateTypeProperty.combinational)) +state_gates = fsm_mod.get_gates(lambda g : g.type.has_property(hal_py.GateTypeProperty.sequential)) initial_state = {} +graph_path = base_path + "examples/fsm/graph.dot" timeout = 600000 -g = pl_fsm.solve_fsm(netlist, state_gates, transition_gates, initial_state, timeout) +g = pl_fsm.solve_fsm(netlist, state_gates, transition_gates, initial_state, graph_path, timeout) #unload everything hal related hal_py.plugin_manager.unload_all_plugins() \ No newline at end of file