9 namespace module_identification
13 #ifdef HAL_CANDIDATE_CONTEXT
19 for (
const auto& n : nets)
21 auto bf_res = subgraph_dec.get_subgraph_function(
m_gates, n, gate_cache);
22 if (bf_res.is_error())
25 "cannot populate context with Boolean functions: failed to generate subgraph function for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()));
27 auto bf = bf_res.get();
30 if (sub_res.is_error())
33 "cannot populate context with Boolean functions: failed to substitute power and ground nets for net " + n->get_name() +
" with ID "
34 + std::to_string(n->get_id()));
37 m_boolean_function_cache.insert({{n, {}}, sub_res.get().
simplify_local()});
45 if (
const auto it = m_boolean_function_cache.find({n, ctrl_mapping}); it != m_boolean_function_cache.end())
47 return OK(it->second);
50 return ERR(
"Failed to get boolean function from chache");
55 std::vector<BooleanFunction> functions;
56 for (
const auto&
net : nets)
59 if (bf_res.is_error())
61 return ERR(bf_res.get_error().get());
63 functions.push_back(bf_res.get().clone());
71 if (
const auto it = m_boolean_function_cache.find({n, ctrl_mapping}); it != m_boolean_function_cache.end())
73 return OK(it->second);
76 if (ctrl_mapping.empty())
78 auto func_res = SubgraphNetlistDecorator(*m_netlist).get_subgraph_function(
m_gates, n);
79 if (func_res.is_error())
82 "cannot get Boolean function from context for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()) +
": failed subgraph function generation");
84 auto bf = func_res.get();
86 auto sub_res = BooleanFunctionDecorator(bf).substitute_power_ground_nets(
m_netlist);
87 if (sub_res.is_error())
90 "cannot get Boolean function from context for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()) +
": failed to substitute power/ground nets");
92 auto sub_bf = sub_res.get().simplify_local();
94 const auto [it, _] = m_boolean_function_cache.insert({{n, ctrl_mapping}, sub_bf});
95 return OK(it->second);
99 if (bf_res.is_error())
103 const auto& bf = bf_res.get();
105 std::map<std::string, BooleanFunction> substitution_map;
106 for (
const auto& [n_ctrl, val] : ctrl_mapping)
108 substitution_map.insert({BooleanFunctionNetDecorator(*n_ctrl).get_boolean_variable_name(),
BooleanFunction::Const(val)});
110 auto sub_res = bf.substitute(substitution_map);
111 if (sub_res.is_error())
114 "cannot get Boolean function from context for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()) +
": failed to substitute with input mapping");
116 const auto sub_bf = sub_res.get().simplify_local();
118 const auto [it, _] = m_boolean_function_cache.insert({{n, ctrl_mapping}, sub_bf});
119 return OK(it->second);
124 std::vector<BooleanFunction> functions;
125 for (
const auto&
net : nets)
128 if (bf_res.is_error())
130 return ERR(bf_res.get_error().get());
132 functions.push_back(bf_res.get().clone());
135 return OK(functions);
140 if (
const auto it = m_boolean_vars_cache.find({n, ctrl_mapping}); it != m_boolean_vars_cache.end())
142 return OK(it->second);
146 if (bf_res.is_error())
149 "cannot get variable names from context for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()) +
": failed to retrieve Boolean function from context");
151 const auto& bf = bf_res.get();
153 const auto [it, _] = m_boolean_vars_cache.insert({{n, ctrl_mapping}, bf.get_variable_names()});
154 return OK(it->second);
160 if (var_names_res.is_error())
163 "cannot get variable nets from context for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()) +
": failed to retrieve variable names from context");
165 const auto& var_names = var_names_res.get();
167 std::set<Net*> result;
168 for (
const auto& var : var_names)
178 if (
const auto it = m_boolean_influence_cache.find({n, ctrl_mapping}); it != m_boolean_influence_cache.end())
180 return OK(it->second);
184 if (bf_res.is_error())
187 "cannot get Boolean influence from context for net " + n->get_name() +
" with ID " + std::to_string(n->get_id())
188 +
": failed to retrieve Boolean function from context");
190 const auto& bf = bf_res.get();
197 "cannot get Boolean influence from context for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()) +
": failed to calculate Boolean influence");
200 const auto [it, _] = m_boolean_influence_cache.insert({{n, ctrl_mapping}, res.get()});
201 return OK(it->second);
204 Result<std::vector<BooleanFunction::Value>>
205 CandidateContext::evaluate(
const Net* n,
const std::map<Net*, BooleanFunction::Value>& ctrl_mapping,
const std::map<std::string, BooleanFunction::Value>& eval_mapping)
208 std::unordered_map<std::string, BooleanFunction::Value> unordered_eval_mapping = {eval_mapping.begin(), eval_mapping.end()};
209 return OK({bf.evaluate(unordered_eval_mapping).get()});
213 #ifdef Z3_CANDIDATE_CONTEXT
217 if (func_res.is_error())
220 log_error(
"module_identification",
"Error on boolean sugraph function creation, for nets: {}", func_res.get_error().get());
222 auto functions = func_res.get();
224 for (
u32 idx = 0; idx < nets.size(); idx++)
226 auto bf = functions.at(idx);
230 z3::expr_vector from(m_ctx);
231 z3::expr_vector
to(m_ctx);
233 for (
const std::string& var_name : vars)
236 if (net_res.is_error())
238 log_error(
"module_identification",
"Error when trying to replace gnd and vcc nets in boolean function for variable '{}': {}", var_name, net_res.get_error().get());
240 const Net*
net = net_res.get();
242 if (
const auto sources =
net->get_sources(); sources.size() == 1)
246 from.push_back(m_ctx.bv_const(var_name.c_str(), 1));
247 to.push_back(m_ctx.bv_val(1, 1));
251 from.push_back(m_ctx.bv_const(var_name.c_str(), 1));
252 to.push_back(m_ctx.bv_val(0, 1));
257 bf = bf.substitute(from,
to).simplify();
260 if (s_res.is_error())
262 std::cout <<
"ERROR: " << s_res.get_error().get() << std::endl;
266 m_boolean_function_cache.insert({{nets.at(idx), {}}, bf});
274 if (
const auto it = m_boolean_function_cache.find({n, ctrl_mapping}); it != m_boolean_function_cache.end())
276 return OK(it->second);
279 if (ctrl_mapping.empty())
282 if (func_res.is_error())
285 log_error(
"module_identification",
"Error on boolean sugraph function creation, for nets: {}", func_res.get_error().get());
287 auto bf = func_res.get();
292 z3::expr_vector from_power_gnd(m_ctx);
293 z3::expr_vector to_power_gnd(m_ctx);
295 for (
const std::string& var_name : vars)
298 if (net_res.is_error())
300 log_error(
"module_identification",
"Error when trying to replace gnd and vcc nets in boolean function for variable '{}': {}", var_name, net_res.get_error().get());
302 const Net*
net = net_res.get();
304 if (
const auto sources =
net->get_sources(); sources.size() == 1)
308 from_power_gnd.push_back(m_ctx.bv_const(var_name.c_str(), 1));
309 to_power_gnd.push_back(m_ctx.bv_val(1, 1));
313 from_power_gnd.push_back(m_ctx.bv_const(var_name.c_str(), 1));
314 to_power_gnd.push_back(m_ctx.bv_val(0, 1));
319 bf = bf.substitute(from_power_gnd, to_power_gnd).simplify();
322 if (s_res.is_error())
324 std::cout <<
"ERROR: " << s_res.get_error().get() << std::endl;
328 m_boolean_function_cache.insert({{n, {}}, bf});
333 z3::expr_vector from(m_ctx);
334 z3::expr_vector
to(m_ctx);
335 for (
const auto& [cn, val] : ctrl_mapping)
337 from.push_back(m_ctx.bv_const(BooleanFunctionNetDecorator(*cn).get_boolean_variable_name().c_str(), 1));
338 to.push_back(m_ctx.bv_val(val == BooleanFunction::Value::ZERO ? 0 : 1, 1));
340 bf = bf.substitute(from,
to).simplify();
343 if (s_res.is_error())
345 std::cout <<
"ERROR: " << s_res.get_error().get() << std::endl;
349 const auto it = m_boolean_function_cache.insert({{n, ctrl_mapping}, bf});
350 return OK(it.first->second);
355 if (
const auto it = m_boolean_function_cache.find({n, ctrl_mapping}); it != m_boolean_function_cache.end())
357 return OK(it->second);
360 std::cout <<
"Control Mapping: " << std::endl;
361 for (
const auto& [cn, v] : ctrl_mapping)
363 std::cout <<
"\t" << cn->get_id() <<
": " << v << std::endl;
366 std::cout <<
"Candidate Gates: " << std::endl;
367 for (
const auto& g : this->
m_gates)
369 std::cout <<
"\t" << g->get_id() <<
": " << g->get_name() << std::endl;
372 return ERR(
"Failed to get boolean function for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()) +
" from boolean function cache");
375 Result<BooleanFunction> CandidateContext::get_hal_boolean_function(
const Net* n,
const std::map<Net*, BooleanFunction::Value>& ctrl_mapping)
377 if (
const auto it = m_boolean_function_hal_cache.find({n, ctrl_mapping}); it != m_boolean_function_hal_cache.end())
379 return OK(it->second);
383 if (bf_res.is_error())
385 return ERR(bf_res.get_error().get());
389 if (bf_hal_res.is_error())
391 return ERR(bf_hal_res.get_error().get());
394 const auto [it, _] = m_boolean_function_hal_cache.insert({{n, ctrl_mapping}, bf_hal_res.get()});
395 return OK(it->second);
398 Result<BooleanFunction> CandidateContext::get_hal_boolean_function_const(
const Net* n,
const std::map<Net*, BooleanFunction::Value>& ctrl_mapping)
400 if (
const auto it = m_boolean_function_hal_cache.find({n, ctrl_mapping}); it != m_boolean_function_hal_cache.end())
402 return OK(it->second);
405 std::cout <<
"Control Mapping: " << std::endl;
406 for (
const auto& [cn, v] : ctrl_mapping)
408 std::cout <<
"\t" << cn->get_id() <<
": " << v << std::endl;
411 std::cout <<
"Candidate Gates: " << std::endl;
412 for (
const auto& g : this->m_gates)
414 std::cout <<
"\t" << g->get_id() <<
": " << g->get_name() << std::endl;
417 return ERR(
"Failed to get boolean function for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()) +
" from boolean function cache");
422 std::vector<BooleanFunction> functions;
423 for (
const auto&
net : nets)
425 const auto bf_hal_res = get_hal_boolean_function(
net, ctrl_mapping);
426 if (bf_hal_res.is_error())
428 return ERR(bf_hal_res.get_error().get());
431 functions.push_back(bf_hal_res.get());
434 return OK(functions);
439 std::vector<BooleanFunction> functions;
440 for (
const auto&
net : nets)
442 const auto bf_hal_res = get_hal_boolean_function_const(
net, ctrl_mapping);
443 if (bf_hal_res.is_error())
445 return ERR(bf_hal_res.get_error().get());
448 functions.push_back(bf_hal_res.get());
451 return OK(functions);
456 if (
const auto it = m_boolean_vars_cache.find({n, ctrl_mapping}); it != m_boolean_vars_cache.end())
458 return OK(it->second);
462 if (bf_res.is_error())
465 "cannot get variable names from context for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()) +
": failed to retrieve Boolean function from context");
467 const auto& bf = bf_res.get();
470 return OK(it->second);
476 if (var_names_res.is_error())
479 "cannot get variable nets from context for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()) +
": failed to retrieve variable names from context");
481 const auto& var_names = var_names_res.get();
483 std::set<Net*> result;
484 for (
const auto& var : var_names)
494 if (
const auto it = m_boolean_influence_cache.find({n, ctrl_mapping}); it != m_boolean_influence_cache.end())
496 return OK(it->second);
503 return ERR_APPEND(res.get_error(),
"failed to create boolean influence");
505 m_boolean_influence_cache.insert({{n, ctrl_mapping}, res.get()});
507 return OK(m_boolean_influence_cache.at({n, ctrl_mapping}));
510 Result<std::vector<BooleanFunction::Value>>
511 CandidateContext::evaluate(
const Net* n,
const std::map<Net*, BooleanFunction::Value>& ctrl_mapping,
const std::map<std::string, BooleanFunction::Value>& eval_mapping)
515 z3::expr_vector from(m_ctx);
516 z3::expr_vector
to(m_ctx);
519 for (
const auto& [var_name, val] : eval_mapping)
521 z3::expr var = m_ctx.bv_const(var_name.c_str(), 1);
522 z3::expr val_expr = m_ctx.bv_val(val, 1);
524 to.push_back(val_expr);
528 z3::expr result = bf_z3.substitute(from,
to).simplify();
530 if (!result.is_numeral())
532 return ERR(
"eval result is non numeral");
535 const u64 res_int = result.get_numeral_uint64();
539 return OK({BooleanFunction::Value::ONE});
544 return OK({BooleanFunction::Value::ZERO});
547 return ERR(
"invalid value " + std::to_string(res_int) +
" as result of eval");
This file contains the CandidateContext struct and that is used for optimization purposes during the ...
Result< BooleanFunction > substitute_power_ground_nets(const Netlist *nl) const
static BooleanFunction Const(const BooleanFunction::Value &value)
static Result< Net * > get_net_from(const Netlist *netlist, const BooleanFunction &var)
#define log_error(channel,...)
#define ERR_APPEND(prev_error, message)
Result< std::unordered_map< std::string, double > > get_boolean_influence(const BooleanFunction &bf, const u32 num_evaluations=32000)
std::set< std::string > get_variable_names(const z3::expr &e)
Extracts all variable names from a z3 expression.
Result< z3::expr > simplify_local(const z3::expr &e, std::unordered_map< u32, z3::expr > &cache, const bool check_correctness=false)
Applies hand-crafted simplification rules iteratively until no further simplifications can be made.
Result< z3::expr > get_subgraph_z3_function(const std::vector< Gate * > &subgraph_gates, const Net *subgraph_output, z3::context &ctx)
Get the z3 expression representation of a combined Boolean function of a subgraph of combinational ga...
Result< std::vector< z3::expr > > get_subgraph_z3_functions(const std::vector< Gate * > &subgraph_gates, const std::vector< Net * > &subgraph_outputs, z3::context &ctx)
Get the z3 expression representations of combined Boolean functions of a subgraph of combinational ga...
Result< BooleanFunction > to_bf(const z3::expr &e)
hal::Result< const std::set< Net * > > get_variable_nets(const Net *n, const std::map< Net *, BooleanFunction::Value > &ctrl_mapping)
Retrieves the variable nets for a given net and control mapping.
hal::Result< std::unordered_map< std::string, double > > get_boolean_influence(const Net *n, const std::map< Net *, BooleanFunction::Value > &ctrl_mapping)
Retrieves the boolean influence for a given net and control mapping.
std::vector< Gate * > m_gates
The gates of the corresponding structural candidate.
CandidateContext(const Netlist *nl, const std::vector< Gate * > &gates)
Constructs a new CandidateContext object saving results for one structural candidate.
hal::Result< std::vector< BooleanFunction > > get_boolean_functions_const(const std::vector< Net * > nets, const std::map< Net *, BooleanFunction::Value > &ctrl_mapping) const
Retrieves a set of constant boolean functions for a given set of nets and control mapping.
hal::Result< const BooleanFunction > get_boolean_function_const(const Net *n, const std::map< Net *, BooleanFunction::Value > &ctrl_mapping) const
Retrieves a constant boolean function for a given net and control mapping.
hal::Result< std::monostate > populate_boolean_function_cache(const std::vector< Net * > nets)
Populates the boolean function cache for a set of nets.
const Netlist * m_netlist
The netlist associated with the candidate context.
hal::Result< const BooleanFunction > get_boolean_function(const Net *n, const std::map< Net *, BooleanFunction::Value > &ctrl_mapping)
Retrieves a boolean function for a given net and control mapping.
hal::Result< std::vector< BooleanFunction::Value > > evaluate(const Net *n, const std::map< Net *, BooleanFunction::Value > &ctrl_mapping, const std::map< std::string, BooleanFunction::Value > &eval_mapping)
Evaluates the boolean function for a given net, control mapping, and evaluation mapping.
hal::Result< const std::set< std::string > > get_variable_names(const Net *n, const std::map< Net *, BooleanFunction::Value > &ctrl_mapping)
Retrieves the variable names for a given net and control mapping.
hal::Result< std::vector< BooleanFunction > > get_boolean_functions(const std::vector< Net * > nets, const std::map< Net *, BooleanFunction::Value > &ctrl_mapping)
Retrieves a set of boolean functions for a given set of nets and control mapping.
The result of a module identification run containing the candidates.