Skip to content

Commit

Permalink
moved get_function_of_gate() into gate class.
Browse files Browse the repository at this point in the history
  • Loading branch information
SimonKlx committed Nov 29, 2022
1 parent 401ce7e commit a43c35b
Show file tree
Hide file tree
Showing 10 changed files with 659 additions and 91 deletions.
9 changes: 9 additions & 0 deletions include/hal_core/netlist/gate.h
Original file line number Diff line number Diff line change
Expand Up @@ -214,6 +214,15 @@ namespace hal
*/
std::unordered_map<std::string, BooleanFunction> get_boolean_functions(bool only_custom_functions = false) const;

/**
* Get the resolved Boolean function corresponding to the given pin.
* Resolved meaning, that the function is only depending on input nets and no internal or output pins.
*
* @param[in] pin - The pin.
* @returns The Boolean function on success, an error otherwise.
*/
Result<BooleanFunction> get_resolved_boolean_function(const GatePin* pin) const;

/**
* Add a Boolean function with the given name to the gate.
*
Expand Down
4 changes: 2 additions & 2 deletions include/hal_core/netlist/netlist.h
Original file line number Diff line number Diff line change
Expand Up @@ -317,7 +317,7 @@ namespace hal
* @param[in] name - The name of the net.
* @returns The new net on success, nullptr otherwise.
*/
Net* create_net(const u32 net_id, const std::string& name = "");
Net* create_net(const u32 net_id, const std::string& name);

/**
* Create a new net and add it to the netlist.<br>
Expand All @@ -326,7 +326,7 @@ namespace hal
* @param[in] name - The name of the net.
* @returns The new net on success, nullptr otherwise.
*/
Net* create_net(const std::string& name = "");
Net* create_net(const std::string& name);

/**
* Remove a net from the netlist.
Expand Down
2 changes: 1 addition & 1 deletion plugins/z3_utils/include/plugin_z3_utils.h
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ namespace hal
* @param[in] control_mapping - A control mapping that can be applied.
* @returns A string containing the verilog representation.
*/
std::string to_verilog(const z3::expr& e, const std::map<std::string, bool>& control_mapping);
std::string to_verilog(const z3::expr& e, const std::map<std::string, bool>& control_mapping={});

/**
* Extracts all variable names from a z3 expression.
Expand Down
85 changes: 14 additions & 71 deletions plugins/z3_utils/src/subgraph_function_generator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,73 +17,6 @@ namespace hal
{
namespace
{
Result<BooleanFunction> get_function_of_gate(const Gate* const gate, const GatePin* output_pin, std::map<std::pair<u32, const GatePin*>, BooleanFunction>& cache)
{
if (auto it = cache.find({gate->get_id(), output_pin}); it != cache.end())
{
return OK(it->second);
}

BooleanFunction bf = gate->get_boolean_function(output_pin);

std::vector<std::string> input_vars = utils::to_vector(bf.get_variable_names());
while (!input_vars.empty())
{
const std::string var = input_vars.back();
input_vars.pop_back();

const GatePin* pin = gate->get_type()->get_pin_by_name(var);
if (pin == nullptr)
{
return ERR("could not get Boolean function of gate '" + gate->get_name() + "' with ID " + std::to_string(gate->get_id()) + ": failed to get input pin '" + var
+ "' by name");
}

const PinDirection pin_dir = pin->get_direction();
if (pin_dir == PinDirection::input)
{
const Net* const input_net = gate->get_fan_in_net(var);
if (input_net == nullptr)
{
// if no net is connected, the input pin name cannot be replaced
return ERR("could not get Boolean function of gate '" + gate->get_name() + "' with ID " + std::to_string(gate->get_id()) + ": failed to get fan-in net at pin '"
+ pin->get_name() + "'");
}

const auto net_dec = BooleanFunctionNetDecorator(*input_net);
bf = bf.substitute(var, net_dec.get_boolean_variable_name());
}
else if ((pin_dir == PinDirection::internal) || (pin_dir == PinDirection::output))
{
BooleanFunction bf_interal = gate->get_boolean_function(var);
if (bf_interal.is_empty())
{
return ERR("could not get Boolean function of gate '" + gate->get_name() + "' with ID " + std::to_string(gate->get_id())
+ ": failed to get Boolean function at output pin '" + pin->get_name() + "'");
}

const std::vector<std::string> internal_input_vars = utils::to_vector(bf_interal.get_variable_names());
input_vars.insert(input_vars.end(), internal_input_vars.begin(), internal_input_vars.end());

if (auto substituted = bf.substitute(var, bf_interal); substituted.is_error())
{
return ERR_APPEND(substituted.get_error(),
"could not get Boolean function of gate '" + gate->get_name() + "' with ID " + std::to_string(gate->get_id()) + ": failed to substitute variable '"
+ var + "' with another Boolean function");
}
else
{
bf = substituted.get();
}
}
}

bf = bf.simplify();

cache.insert({{gate->get_id(), output_pin}, bf});
return OK(bf);
}

Result<z3::expr> get_function_of_net(const std::vector<Gate*>& subgraph_gates, const Net* net, z3::context& ctx, std::map<u32, z3::expr>& net_cache, std::map<std::pair<u32, const GatePin*>, BooleanFunction>& gate_cache)
{
if (const auto it = net_cache.find(net->get_id()); it != net_cache.end())
Expand Down Expand Up @@ -124,12 +57,22 @@ namespace hal
return OK(ret);
}

const auto& bf_res = get_function_of_gate(src, src_ep->get_pin(), gate_cache);
if (bf_res.is_error())
BooleanFunction bf;
if (const auto it = gate_cache.find({src->get_id(), src_ep->get_pin()}); it == gate_cache.end())
{
const auto bf_res = src->get_resolved_boolean_function(src_ep->get_pin());
if (bf_res.is_error())
{
return ERR_APPEND(bf_res.get_error(), "cannot get Boolean z3 function of net " + net->get_name() + " with ID " + std::to_string(net->get_id()) + ": failed to get function of gate.");
}
bf = bf_res.get();

gate_cache.insert({{src->get_id(), src_ep->get_pin()}, bf});
}
else
{
return ERR_APPEND(bf_res.get_error(), "cannot get Boolean z3 function of net " + net->get_name() + " with ID " + std::to_string(net->get_id()) + ": failed to get function of gate.");
bf = it->second;
}
const BooleanFunction bf = bf_res.get();

std::map<std::string, z3::expr> input_to_expr;

Expand Down
47 changes: 30 additions & 17 deletions src/netlist/decorators/subgraph_netlist_decorator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -201,13 +201,16 @@ namespace hal

namespace
{
/*
static Result<BooleanFunction> get_function_of_gate(const Gate* const gate, const GatePin* output_pin, std::map<std::pair<u32, const GatePin*>, BooleanFunction>& cache)
{
if (auto it = cache.find({gate->get_id(), output_pin}); it != cache.end())
{
return OK(it->second);
}
// TODO there has to be some kind of endless loop protection. RAM has Boolean function RDATA(0) = RDATA(0) & !MASK(0) -> leads to endless loop
BooleanFunction bf = gate->get_boolean_function(output_pin);
std::vector<std::string> input_vars = utils::to_vector(bf.get_variable_names());
Expand Down Expand Up @@ -267,10 +270,11 @@ namespace hal
cache.insert({{gate->get_id(), output_pin}, bf});
return OK(bf);
}
*/

Result<BooleanFunction> subgraph_function_recursive(const Net* n,
const std::vector<const Gate*>& subgraph_gates,
std::map<std::pair<u32, const GatePin*>, BooleanFunction>& cache,
std::map<std::pair<u32, const GatePin*>, BooleanFunction>& gate_cache,
std::unordered_set<const Net*>& on_stack)
{
if (on_stack.find(n) != on_stack.end())
Expand Down Expand Up @@ -309,18 +313,25 @@ namespace hal
return OK(net_dec.get_boolean_variable());
}

auto gate_func_res = get_function_of_gate(src_gate, src_ep->get_pin(), cache);
if (gate_func_res.is_error())
BooleanFunction gate_func;
if (const auto it = gate_cache.find({src_gate->get_id(), src_ep->get_pin()}); it == gate_cache.end())
{
return ERR_APPEND(gate_func_res.get_error(),
"could not get subgraph function of net '" + n->get_name() + "' with ID " + std::to_string(n->get_id()) + ": failed to get Boolean function of gate '"
+ src_gate->get_name() + "' with ID " + std::to_string(src_gate->get_id()));
const auto bf_res = src_gate->get_resolved_boolean_function(src_ep->get_pin());
if (bf_res.is_error())
{
return ERR_APPEND(bf_res.get_error(), "could not get subgraph function of net " + n->get_name() + " with ID " + std::to_string(n->get_id()) + ": failed to get function of gate.");
}
gate_func = bf_res.get().simplify();

gate_cache.insert({{src_gate->get_id(), src_ep->get_pin()}, gate_func});
}
else
{
gate_func = it->second;
}

on_stack.insert(n);

const BooleanFunction gate_func = gate_func_res.get();

std::map<std::string, BooleanFunction> input_to_bf;

for (const std::string& in_net_str : gate_func.get_variable_names())
Expand All @@ -333,7 +344,7 @@ namespace hal
return ERR("could not get subgraph function of net '" + n->get_name() + "' with ID " + std::to_string(n->get_id()) + ": cannot find in_net " + in_net_str + " at gate " + std::to_string(src_gate->get_id()) + "!");
}

auto input_bf_res = subgraph_function_recursive(in_net, subgraph_gates, cache, on_stack);
auto input_bf_res = subgraph_function_recursive(in_net, subgraph_gates, gate_cache, on_stack);

if (input_bf_res.is_error())
{
Expand Down Expand Up @@ -419,9 +430,11 @@ namespace hal
*/
} // namespace



Result<BooleanFunction> SubgraphNetlistDecorator::get_subgraph_function(const std::vector<const Gate*>& subgraph_gates,
const Net* subgraph_output,
std::map<std::pair<u32, const GatePin*>, BooleanFunction>& cache) const
std::map<std::pair<u32, const GatePin*>, BooleanFunction>& gate_cache) const
{
// check validity of subgraph_gates
if (subgraph_gates.empty())
Expand Down Expand Up @@ -459,14 +472,14 @@ namespace hal

std::unordered_set<const Net*> on_stack;

return subgraph_function_recursive(subgraph_output, subgraph_gates, cache, on_stack);
return subgraph_function_recursive(subgraph_output, subgraph_gates, gate_cache, on_stack);
}

Result<BooleanFunction>
SubgraphNetlistDecorator::get_subgraph_function(const std::vector<Gate*>& subgraph_gates, const Net* subgraph_output, std::map<std::pair<u32, const GatePin*>, BooleanFunction>& cache) const
SubgraphNetlistDecorator::get_subgraph_function(const std::vector<Gate*>& subgraph_gates, const Net* subgraph_output, std::map<std::pair<u32, const GatePin*>, BooleanFunction>& gate_cache) const
{
const auto subgraph_gates_const = std::vector<const Gate*>(subgraph_gates.begin(), subgraph_gates.end());
if (auto res = get_subgraph_function(subgraph_gates_const, subgraph_output, cache); res.is_error())
if (auto res = get_subgraph_function(subgraph_gates_const, subgraph_output, gate_cache); res.is_error())
{
return ERR(res.get_error());
}
Expand All @@ -477,9 +490,9 @@ namespace hal
}

Result<BooleanFunction>
SubgraphNetlistDecorator::get_subgraph_function(const Module* subgraph_module, const Net* subgraph_output, std::map<std::pair<u32, const GatePin*>, BooleanFunction>& cache) const
SubgraphNetlistDecorator::get_subgraph_function(const Module* subgraph_module, const Net* subgraph_output, std::map<std::pair<u32, const GatePin*>, BooleanFunction>& gate_cache) const
{
if (auto res = get_subgraph_function(subgraph_module->get_gates(), subgraph_output, cache); res.is_error())
if (auto res = get_subgraph_function(subgraph_module->get_gates(), subgraph_output, gate_cache); res.is_error())
{
return ERR(res.get_error());
}
Expand All @@ -491,8 +504,8 @@ namespace hal

Result<BooleanFunction> SubgraphNetlistDecorator::get_subgraph_function(const std::vector<const Gate*>& subgraph_gates, const Net* subgraph_output) const
{
std::map<std::pair<u32, const GatePin*>, BooleanFunction> cache;
if (auto res = get_subgraph_function(subgraph_gates, subgraph_output, cache); res.is_error())
std::map<std::pair<u32, const GatePin*>, BooleanFunction> gate_cache;
if (auto res = get_subgraph_function(subgraph_gates, subgraph_output, gate_cache); res.is_error())
{
return ERR(res.get_error());
}
Expand Down
76 changes: 76 additions & 0 deletions src/netlist/gate.cpp
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
#include "hal_core/netlist/gate.h"

#include "hal_core/netlist/decorators/boolean_function_net_decorator.h"
#include "hal_core/netlist/endpoint.h"
#include "hal_core/netlist/event_system/event_handler.h"
#include "hal_core/netlist/gate_library/gate_type.h"
Expand Down Expand Up @@ -260,6 +261,81 @@ namespace hal
return res;
}

Result<BooleanFunction> Gate::get_resolved_boolean_function(const GatePin* pin) const
{
const std::function<Result<BooleanFunction>(const GatePin*, std::unordered_set<std::string>&)> get_resolved_boolean_function_internal =
[this, &get_resolved_boolean_function_internal](const GatePin* output_pin, std::unordered_set<std::string>& on_stack) -> Result<BooleanFunction>
{
if (output_pin == nullptr)
{
return ERR("could not get resolved Boolean function of gate '" + this->get_name() + "' with ID " + std::to_string(this->get_id()) + ": given output pin is null.");
}

if (on_stack.find(output_pin->get_name()) != on_stack.end())
{
return ERR("could not get resolved Boolean function of gate '" + this->get_name() + "' with ID " + std::to_string(this->get_id()) + ": boolean functions of gate contain an endless recursion including pin '" + output_pin->get_name() + "'");
}
on_stack.insert(output_pin->get_name());

BooleanFunction bf = this->get_boolean_function(output_pin);

std::map<std::string, BooleanFunction> input_to_bf;
std::vector<std::string> input_vars = utils::to_vector(bf.get_variable_names());
for (const auto& var : bf.get_variable_names())
{
const GatePin* pin = this->get_type()->get_pin_by_name(var);
if (pin == nullptr)
{
return ERR("could not get resolved Boolean function of gate '" + this->get_name() + "' with ID " + std::to_string(this->get_id()) + ": failed to get input pin '" + var + "' by name");
}

const PinDirection pin_dir = pin->get_direction();
if (pin_dir == PinDirection::input)
{
const Net* const input_net = this->get_fan_in_net(var);
if (input_net == nullptr)
{
// if no net is connected, the input pin name cannot be replaced
return ERR("could not get resolved Boolean function of gate '" + this->get_name() + "' with ID " + std::to_string(this->get_id()) + ": failed to get fan-in net at pin '"
+ pin->get_name() + "'");
}

const auto net_dec = BooleanFunctionNetDecorator(*input_net);
input_to_bf.insert({var, net_dec.get_boolean_variable()});
}
else if ((pin_dir == PinDirection::internal) || (pin_dir == PinDirection::output))
{
const auto bf_interal_res = get_resolved_boolean_function_internal(pin, on_stack);
if (bf_interal_res.is_error())
{
return ERR_APPEND(bf_interal_res.get_error(), "could not get resolved Boolean function of gate '" + this->get_name() + "' with ID " + std::to_string(this->get_id())
+ ": failed to get Boolean function at output pin '" + pin->get_name() + "'");
}

input_to_bf.insert({pin->get_name(), bf_interal_res.get()});
}
}

if (auto substituted = bf.substitute(input_to_bf); substituted.is_error())
{
return ERR_APPEND(substituted.get_error(),
"could not get resolved Boolean function of gate '" + this->get_name() + "' with ID " + std::to_string(this->get_id()) + ": failed to substitute variable inputs with other Boolean functions");
}
else
{
bf = substituted.get();
}

on_stack.erase(output_pin->get_name());

return OK(bf);
};

std::unordered_set<std::string> on_stack;

return get_resolved_boolean_function_internal(pin, on_stack);
}

BooleanFunction Gate::get_lut_function(const GatePin* pin) const
{
UNUSED(pin);
Expand Down
20 changes: 20 additions & 0 deletions src/python_bindings/bindings/gate.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -200,6 +200,26 @@ namespace hal
:rtype: hal_py.BooleanFunction
)");

py_gate.def("get_resolved_boolean_function", [](const Gate& self, const GatePin* pin) -> std::optional<BooleanFunction> {
auto res = self.get_resolved_boolean_function(pin);
if (res.is_ok())
{
return res.get();
}
else
{
log_error("python_context", "{}", res.get_error().get());
return std::nullopt;
}
}, py::arg("pin") = nullptr, R"(
Get the resolved Boolean function corresponding to the given pin.
Resolved meaning, that the function is only depending on input nets and no internal or output pins.
:param hal_py.GatePin pin: The pin.
:returns: The Boolean function on success, an error otherwise.
:rtype: hal_py.BooleanFunction
)");

py_gate.def_property_readonly(
"boolean_functions", [](Gate* g) { return g->get_boolean_functions(); }, R"(
A dictionary from function name to Boolean function for all boolean functions associated with this gate.
Expand Down
Loading

0 comments on commit a43c35b

Please sign in to comment.