10 namespace module_identification
14 #ifdef HAL_CANDIDATE_CONTEXT
18 auto gate_cache_res = subgraph_dec.make_subgraph_function_cache(
m_gates);
19 if (gate_cache_res.is_error())
21 return ERR_APPEND(gate_cache_res.get_error(),
"cannot populate context with Boolean functions: failed to create subgraph function cache");
23 auto gate_cache = gate_cache_res.get();
25 for (
const auto& n : nets)
27 auto bf_res = subgraph_dec.get_subgraph_function(n, gate_cache);
28 if (bf_res.is_error())
31 "cannot populate context with Boolean functions: failed to generate subgraph function for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()));
33 auto bf = bf_res.get();
35 auto sub_res = BooleanFunctionDecorator(bf).substitute_power_ground_nets(
m_netlist);
36 if (sub_res.is_error())
39 "cannot populate context with Boolean functions: failed to substitute power and ground nets for net " + n->get_name() +
" with ID "
40 + std::to_string(n->get_id()));
43 m_boolean_function_cache.insert({{n, {}}, sub_res.get().
simplify_local()});
51 if (
const auto it = m_boolean_function_cache.find({n, ctrl_mapping}); it != m_boolean_function_cache.end())
53 return OK(it->second);
56 return ERR(
"Failed to get boolean function from chache");
61 std::vector<BooleanFunction> functions;
62 for (
const auto&
net : nets)
65 if (bf_res.is_error())
67 return ERR(bf_res.get_error().get());
69 functions.push_back(bf_res.get().clone());
77 if (
const auto it = m_boolean_function_cache.find({n, ctrl_mapping}); it != m_boolean_function_cache.end())
79 return OK(it->second);
82 if (ctrl_mapping.empty())
84 auto func_res = SubgraphNetlistDecorator(*m_netlist).get_subgraph_function(
m_gates, n);
85 if (func_res.is_error())
88 "cannot get Boolean function from context for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()) +
": failed subgraph function generation");
90 auto bf = func_res.get();
92 auto sub_res = BooleanFunctionDecorator(bf).substitute_power_ground_nets(
m_netlist);
93 if (sub_res.is_error())
96 "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");
98 auto sub_bf = sub_res.get().simplify_local();
100 const auto [it, _] = m_boolean_function_cache.insert({{n, ctrl_mapping}, sub_bf});
101 return OK(it->second);
105 if (bf_res.is_error())
109 const auto& bf = bf_res.get();
111 std::map<std::string, BooleanFunction> substitution_map;
112 for (
const auto& [n_ctrl, val] : ctrl_mapping)
114 substitution_map.insert({BooleanFunctionNetDecorator(*n_ctrl).get_boolean_variable_name(),
BooleanFunction::Const(val)});
116 auto sub_res = bf.substitute(substitution_map);
117 if (sub_res.is_error())
120 "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");
122 const auto sub_bf = sub_res.get().simplify_local();
124 const auto [it, _] = m_boolean_function_cache.insert({{n, ctrl_mapping}, sub_bf});
125 return OK(it->second);
130 std::vector<BooleanFunction> functions;
131 for (
const auto&
net : nets)
134 if (bf_res.is_error())
136 return ERR(bf_res.get_error().get());
138 functions.push_back(bf_res.get().clone());
141 return OK(functions);
146 if (
const auto it = m_boolean_vars_cache.find({n, ctrl_mapping}); it != m_boolean_vars_cache.end())
148 return OK(it->second);
152 if (bf_res.is_error())
155 "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");
157 const auto& bf = bf_res.get();
159 const auto [it, _] = m_boolean_vars_cache.insert({{n, ctrl_mapping}, bf.get_variable_names()});
160 return OK(it->second);
166 if (var_names_res.is_error())
169 "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");
171 const auto& var_names = var_names_res.get();
173 std::set<Net*> result;
174 for (
const auto& var : var_names)
184 if (
const auto it = m_boolean_influence_cache.find({n, ctrl_mapping}); it != m_boolean_influence_cache.end())
186 return OK(it->second);
190 if (bf_res.is_error())
193 "cannot get Boolean influence from context for net " + n->get_name() +
" with ID " + std::to_string(n->get_id())
194 +
": failed to retrieve Boolean function from context");
196 const auto& bf = bf_res.get();
203 "cannot get Boolean influence from context for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()) +
": failed to calculate Boolean influence");
206 const auto [it, _] = m_boolean_influence_cache.insert({{n, ctrl_mapping}, res.get()});
207 return OK(it->second);
210 Result<std::vector<BooleanFunction::Value>>
211 CandidateContext::evaluate(
const Net* n,
const std::map<Net*, BooleanFunction::Value>& ctrl_mapping,
const std::map<std::string, BooleanFunction::Value>& eval_mapping)
214 std::unordered_map<std::string, BooleanFunction::Value> unordered_eval_mapping = {eval_mapping.begin(), eval_mapping.end()};
215 return OK({bf.evaluate(unordered_eval_mapping).get()});
219 #ifdef Z3_CANDIDATE_CONTEXT
223 if (func_res.is_error())
226 log_error(
"module_identification",
"Error on boolean sugraph function creation, for nets: {}", func_res.get_error().get());
228 auto functions = func_res.get();
230 for (
u32 idx = 0; idx < nets.size(); idx++)
232 auto bf = functions.at(idx);
236 z3::expr_vector from(m_ctx);
237 z3::expr_vector
to(m_ctx);
239 for (
const std::string& var_name : vars)
242 if (net_res.is_error())
244 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());
246 const Net*
net = net_res.get();
248 if (
const auto sources =
net->get_sources(); sources.size() == 1)
252 from.push_back(m_ctx.bv_const(var_name.c_str(), 1));
253 to.push_back(m_ctx.bv_val(1, 1));
257 from.push_back(m_ctx.bv_const(var_name.c_str(), 1));
258 to.push_back(m_ctx.bv_val(0, 1));
263 bf = bf.substitute(from,
to).simplify();
266 if (s_res.is_error())
268 std::cout <<
"ERROR: " << s_res.get_error().get() << std::endl;
272 m_boolean_function_cache.insert({{nets.at(idx), {}}, bf});
280 if (
const auto it = m_boolean_function_cache.find({n, ctrl_mapping}); it != m_boolean_function_cache.end())
282 return OK(it->second);
285 if (ctrl_mapping.empty())
288 if (func_res.is_error())
291 log_error(
"module_identification",
"Error on boolean sugraph function creation, for nets: {}", func_res.get_error().get());
293 auto bf = func_res.get();
298 z3::expr_vector from_power_gnd(m_ctx);
299 z3::expr_vector to_power_gnd(m_ctx);
301 for (
const std::string& var_name : vars)
304 if (net_res.is_error())
306 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());
308 const Net*
net = net_res.get();
310 if (
const auto sources =
net->get_sources(); sources.size() == 1)
314 from_power_gnd.push_back(m_ctx.bv_const(var_name.c_str(), 1));
315 to_power_gnd.push_back(m_ctx.bv_val(1, 1));
319 from_power_gnd.push_back(m_ctx.bv_const(var_name.c_str(), 1));
320 to_power_gnd.push_back(m_ctx.bv_val(0, 1));
325 bf = bf.substitute(from_power_gnd, to_power_gnd).simplify();
328 if (s_res.is_error())
330 std::cout <<
"ERROR: " << s_res.get_error().get() << std::endl;
334 m_boolean_function_cache.insert({{n, {}}, bf});
339 z3::expr_vector from(m_ctx);
340 z3::expr_vector
to(m_ctx);
341 for (
const auto& [cn, val] : ctrl_mapping)
343 from.push_back(m_ctx.bv_const(BooleanFunctionNetDecorator(*cn).get_boolean_variable_name().c_str(), 1));
344 to.push_back(m_ctx.bv_val(val == BooleanFunction::Value::ZERO ? 0 : 1, 1));
346 bf = bf.substitute(from,
to).simplify();
349 if (s_res.is_error())
351 std::cout <<
"ERROR: " << s_res.get_error().get() << std::endl;
355 const auto it = m_boolean_function_cache.insert({{n, ctrl_mapping}, bf});
356 return OK(it.first->second);
361 if (
const auto it = m_boolean_function_cache.find({n, ctrl_mapping}); it != m_boolean_function_cache.end())
363 return OK(it->second);
366 std::cout <<
"Control Mapping: " << std::endl;
367 for (
const auto& [cn, v] : ctrl_mapping)
369 std::cout <<
"\t" << cn->get_id() <<
": " << v << std::endl;
372 std::cout <<
"Candidate Gates: " << std::endl;
373 for (
const auto& g : this->
m_gates)
375 std::cout <<
"\t" << g->get_id() <<
": " << g->get_name() << std::endl;
378 return ERR(
"Failed to get boolean function for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()) +
" from boolean function cache");
381 Result<BooleanFunction> CandidateContext::get_hal_boolean_function(
const Net* n,
const std::map<Net*, BooleanFunction::Value>& ctrl_mapping)
383 if (
const auto it = m_boolean_function_hal_cache.find({n, ctrl_mapping}); it != m_boolean_function_hal_cache.end())
385 return OK(it->second);
389 if (bf_res.is_error())
391 return ERR(bf_res.get_error().get());
395 if (bf_hal_res.is_error())
397 return ERR(bf_hal_res.get_error().get());
400 const auto [it, _] = m_boolean_function_hal_cache.insert({{n, ctrl_mapping}, bf_hal_res.get()});
401 return OK(it->second);
404 Result<BooleanFunction> CandidateContext::get_hal_boolean_function_const(
const Net* n,
const std::map<Net*, BooleanFunction::Value>& ctrl_mapping)
406 if (
const auto it = m_boolean_function_hal_cache.find({n, ctrl_mapping}); it != m_boolean_function_hal_cache.end())
408 return OK(it->second);
411 std::cout <<
"Control Mapping: " << std::endl;
412 for (
const auto& [cn, v] : ctrl_mapping)
414 std::cout <<
"\t" << cn->get_id() <<
": " << v << std::endl;
417 std::cout <<
"Candidate Gates: " << std::endl;
418 for (
const auto& g : this->m_gates)
420 std::cout <<
"\t" << g->get_id() <<
": " << g->get_name() << std::endl;
423 return ERR(
"Failed to get boolean function for net " + n->get_name() +
" with ID " + std::to_string(n->get_id()) +
" from boolean function cache");
428 std::vector<BooleanFunction> functions;
429 for (
const auto&
net : nets)
431 const auto bf_hal_res = get_hal_boolean_function(
net, ctrl_mapping);
432 if (bf_hal_res.is_error())
434 return ERR(bf_hal_res.get_error().get());
437 functions.push_back(bf_hal_res.get());
440 return OK(functions);
445 std::vector<BooleanFunction> functions;
446 for (
const auto&
net : nets)
448 const auto bf_hal_res = get_hal_boolean_function_const(
net, ctrl_mapping);
449 if (bf_hal_res.is_error())
451 return ERR(bf_hal_res.get_error().get());
454 functions.push_back(bf_hal_res.get());
457 return OK(functions);
462 if (
const auto it = m_boolean_vars_cache.find({n, ctrl_mapping}); it != m_boolean_vars_cache.end())
464 return OK(it->second);
468 if (bf_res.is_error())
471 "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");
473 const auto& bf = bf_res.get();
476 return OK(it->second);
482 if (var_names_res.is_error())
485 "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");
487 const auto& var_names = var_names_res.get();
489 std::set<Net*> result;
490 for (
const auto& var : var_names)
500 if (
const auto it = m_boolean_influence_cache.find({n, ctrl_mapping}); it != m_boolean_influence_cache.end())
502 return OK(it->second);
509 return ERR_APPEND(res.get_error(),
"failed to create boolean influence");
511 m_boolean_influence_cache.insert({{n, ctrl_mapping}, res.get()});
513 return OK(m_boolean_influence_cache.at({n, ctrl_mapping}));
516 Result<std::vector<BooleanFunction::Value>>
517 CandidateContext::evaluate(
const Net* n,
const std::map<Net*, BooleanFunction::Value>& ctrl_mapping,
const std::map<std::string, BooleanFunction::Value>& eval_mapping)
521 z3::expr_vector from(m_ctx);
522 z3::expr_vector
to(m_ctx);
525 for (
const auto& [var_name, val] : eval_mapping)
527 z3::expr var = m_ctx.bv_const(var_name.c_str(), 1);
528 z3::expr val_expr = m_ctx.bv_val(val, 1);
530 to.push_back(val_expr);
534 z3::expr result = bf_z3.substitute(from,
to).simplify();
536 if (!result.is_numeral())
538 return ERR(
"eval result is non numeral");
541 const u64 res_int = result.get_numeral_uint64();
545 return OK({BooleanFunction::Value::ONE});
550 return OK({BooleanFunction::Value::ZERO});
553 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 ...
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.