HAL  v4.5.0-83-g30c8f0afc
The Hardware Analyzer - a comprehensive reverse engineering and manipulation framework for gate-level netlists.
sequential_symbolic_execution.cpp
Go to the documentation of this file.
1 #pragma once
2 
3 #include "hal_core/netlist/boolean_function/simplification.h"
4 #include "hal_core/netlist/decorators/boolean_function_net_decorator.h"
5 #include "hal_core/netlist/gate.h"
6 #include "hal_core/netlist/gate_library/gate_type_component/ff_component.h"
7 #include "hal_core/netlist/module.h"
8 #include "hal_core/netlist/net.h"
9 #include "hal_core/netlist/netlist.h"
10 #include "hal_core/utilities/utils.h"
11 #include "z3_utils/simplification.h"
12 #include "z3_utils/z3_utils.h"
13 
14 #include <sys/resource.h>
15 
16 namespace hal
17 {
18  namespace sse
19  {
20  namespace
21  {
22  inline BooleanFunction
23  get_function_of_gate(const Gate* const gate, const std::string& output_pin, const u32 time_index, std::map<std::tuple<u32, std::string, u32>, BooleanFunction>& cache)
24  {
25  if (auto it = cache.find({gate->get_id(), output_pin, time_index}); it != cache.end())
26  {
27  return it->second;
28  }
29 
30  BooleanFunction bf = gate->get_boolean_function(output_pin);
31 
32  std::vector<std::string> input_vars = utils::to_vector(bf.get_variable_names());
33  while (!input_vars.empty())
34  {
35  const std::string var = input_vars.back();
36  input_vars.pop_back();
37 
38  const PinDirection pin_dir = gate->get_type()->get_pins([var](GatePin* p) { return p->get_name() == var; }).front()->get_direction();
39 
40  if (pin_dir == PinDirection::input)
41  {
42  const Net* const input_net = gate->get_fan_in_net(var);
43  if (input_net == nullptr)
44  {
45  // if no net is connected, the input pin name cannot be replaced
46  log_warning("sequential_symbolic_execution", "no net is connected to input pin '{}' of gate with ID {}, cannot replace pin name with net ID.", var, gate->get_id());
47  return bf;
48  }
49 
50  bf = bf.substitute(var, "net_" + std::to_string(input_net->get_id()) + "_" + std::to_string(time_index));
51  }
52  else if ((pin_dir == PinDirection::internal) || (pin_dir == PinDirection::output))
53  {
54  BooleanFunction bf_interal = gate->get_boolean_function(var);
55  if (bf_interal.is_empty())
56  {
57  log_warning("sequential_symbolic_execution",
58  "trying to replace {} in function {} for gate {} and pin {} but cannot find boolean fucntion.",
59  var,
60  bf.to_string(),
61  gate->get_id(),
62  output_pin);
63  return bf;
64  }
65 
66  const std::vector<std::string> internal_input_vars = utils::to_vector(bf_interal.get_variable_names());
67  input_vars.insert(input_vars.end(), internal_input_vars.begin(), internal_input_vars.end());
68 
69  auto substituted = bf.substitute(var, bf_interal);
70  if (substituted.is_error())
71  {
72  log_error("sequential_symbolic_execution", "{}", substituted.get_error().get());
73  return BooleanFunction();
74  }
75  bf = substituted.get();
76  }
77  }
78 
79  cache.insert({{gate->get_id(), output_pin, time_index}, bf});
80  return bf;
81  }
82 
83  inline BooleanFunction
84  get_function_of_seq_gate(const Gate* const gate, const std::string& output_pin, const u32 time_index, std::map<std::tuple<u32, std::string, u32>, BooleanFunction>& cache)
85  {
86  if (auto it = cache.find({gate->get_id(), output_pin, time_index}); it != cache.end())
87  {
88  return it->second;
89  }
90 
91  auto state_pins = gate->get_type()->get_pins([](GatePin* p) { return p->get_type() == PinType::state; });
92 
93  if (state_pins.size() != 1)
94  {
95  log_error("iphone_tools", "Found {} state pisn for gate {} of type {}. Can only handle one!", state_pins.size(), gate->get_id(), gate->get_type()->get_name());
96  }
97 
98  auto state_pin = *(state_pins.begin());
99 
100  auto internal_state_bf = gate->get_type()->get_boolean_function(state_pin);
101  if (!internal_state_bf.is_variable())
102  {
103  log_error("sequential_symbolic_execution", "Internal state of ff type {} is not a single variable. Cannot handle!", gate->get_type()->get_name());
104  }
105  auto internal_state_name = *(internal_state_bf.get_variable_names().begin());
106 
107  if (internal_state_bf.is_empty())
108  {
109  log_error("sequential_symbolic_execution", "No booleanfunction for pin {} at gatetype {}!", output_pin, gate->get_type()->get_name());
110  }
111 
112  auto ff_cfg = gate->get_type()->get_component_as<FFComponent>([](const GateTypeComponent* gtc) { return gtc->get_type() == GateTypeComponent::ComponentType::ff; });
113 
114  auto bf = (ff_cfg->get_clock_function() & ff_cfg->get_next_state_function()) | (~ff_cfg->get_clock_function() & internal_state_bf);
115 
116  if (auto async_reset = ff_cfg->get_async_reset_function(); !async_reset.is_empty())
117  {
118  bf = bf & (~async_reset);
119  }
120  if (auto async_set = ff_cfg->get_async_set_function(); !async_set.is_empty())
121  {
122  bf = bf | async_set;
123  }
124 
125  bf = bf.substitute(internal_state_name, state_pin->get_name());
126 
127  // const std::map<std::string, BooleanFunction> gate_type_to_boolean_function = {
128  // {"SB_DFFER", BooleanFunction::from_string("(((C & E) & !R) & D) | (((!C | !E) & !R) & Q)").get()},
129  // {"SB_DFFS", BooleanFunction::from_string("(C & (D | S)) | (!C & Q)").get()},
130  // {"SB_DFFES", BooleanFunction::from_string("(C & ((E & D) | S | (!E & Q))) | (!C & Q)").get()},
131  // };
132 
133  if (gate->get_type()->get_pins([output_pin](GatePin* p) { return p->get_name() == output_pin; }).front()->get_type() == PinType::neg_state)
134  {
135  bf = ~bf;
136  }
137 
138  for (const auto& pin_name : bf.get_variable_names())
139  {
140  const auto pin = gate->get_type()->get_pins([pin_name](GatePin* p) { return p->get_name() == pin_name; }).front();
141  const auto net = (pin->get_direction() == PinDirection::input) ? gate->get_fan_in_net(pin) : gate->get_fan_out_net(pin);
142  // const u32 new_time_index = (pin->get_type() == PinType::neg_state || pin->get_type() == PinType::state) ? (time_index - 1) : time_index;
143  const u32 new_time_index = time_index - 1;
144 
145  if (net != nullptr)
146  {
147  const std::string net_name = "net_" + std::to_string(net->get_id()) + "_" + std::to_string(new_time_index);
148  bf = bf.substitute(pin_name, net_name);
149  }
150  }
151 
152  cache.insert({{gate->get_id(), output_pin, time_index}, bf});
153  return bf;
154  }
155 
156  Result<z3::expr> get_function_of_net_z3_word_level_internal(Net* net,
157  const u32 time_index,
158  const std::vector<bool>& subgraph_gates_byte_map,
159  const std::vector<std::map<u32, bool>>& known_inputs,
160  const std::map<PinGroup<ModulePin>*, BooleanFunction>& word_level_calculations,
161  std::map<std::tuple<u32, std::string, u32>, BooleanFunction>& gate_cache,
162  std::map<std::pair<u32, u32>, z3::expr>& net_cache,
163  const bool substitute_endpoints,
164  z3::context& ctx)
165  {
166  // std::cout << "Getting function at time step " << time_index << " for net " << net->get_id() << " - " << net->get_name() << std::endl;
167 
168  if (net == nullptr)
169  {
170  return ERR("nullptr given for target net");
171  }
172  else if (net->get_num_of_sources() > 1)
173  {
174  return ERR("target net " + net->get_name() + " with ID " + std::to_string(net->get_id()) + "has more than one source");
175  }
176 
177  if (known_inputs.at(time_index).find(net->get_id()) != known_inputs.at(time_index).end())
178  {
179  const auto known_value = known_inputs.at(time_index).at(net->get_id()) ? 1 : 0;
180  const auto bf = ctx.bv_val(known_value, 1);
181  net_cache.insert({{net->get_id(), time_index}, bf});
182  return OK(bf);
183  }
184 
185  if (const auto it = net_cache.find({net->get_id(), time_index}); it != net_cache.end())
186  {
187  return OK(it->second);
188  }
189 
190  if (net->is_global_input_net())
191  {
192  if (substitute_endpoints)
193  {
194  const auto pin = net->get_netlist()->get_top_module()->get_pin_by_net(net);
195  const auto [pin_group, index] = pin->get_group();
196  const std::string name = pin_group->get_name() + "_" + std::to_string(time_index);
197 
198  const auto bf = ctx.bv_const(name.c_str(), pin_group->size()).extract(index, index);
199  net_cache.insert({{net->get_id(), time_index}, bf});
200  return OK(bf);
201  }
202 
203  const auto bf = ctx.bv_const(("net_" + std::to_string(net->get_id()) + "_" + std::to_string(time_index)).c_str(), 1);
204  net_cache.insert({{net->get_id(), time_index}, bf});
205  return OK(bf);
206  }
207 
208  if (net->get_num_of_sources() == 0)
209  {
210  // log_debug("sequential_symbolic_execution", "target net with ID {} has no sources.", net->get_id());
211 
212  const auto bf = ctx.bv_const(("net_" + std::to_string(net->get_id()) + "_" + std::to_string(time_index)).c_str(), 1);
213  net_cache.insert({{net->get_id(), time_index}, bf});
214  return OK(bf);
215  }
216 
217  const Gate* src_gate = net->get_sources()[0]->get_gate();
218  const std::string src_pin = net->get_sources()[0]->get_pin()->get_name();
219  const bool has_sequential_src = src_gate->get_type()->has_property(GateTypeProperty::sequential);
220 
221  const auto all_src_modules = src_gate->get_modules(nullptr, true);
222 
223  // reached end of subgraph or time limit
224  if ((!subgraph_gates_byte_map.at(src_gate->get_id())) || (has_sequential_src && (time_index == 0)))
225  {
226  if (substitute_endpoints)
227  {
228  // Find highest order module with an intact bitorder to substitute net with sliced bit field from module
229  for (auto it = all_src_modules.rbegin(); it != all_src_modules.rend(); it++)
230  {
231  const auto src_mod = *it;
232  if (src_mod->is_output_net(net))
233  {
234  const auto pin = src_mod->get_pin_by_net(net);
235  const auto [pin_group, index] = pin->get_group();
236 
237  if (pin_group->size() > 1)
238  {
239  const std::string name = src_mod->get_name() + "_" + pin_group->get_name() + "_" + std::to_string(time_index);
240  const auto bf = ctx.bv_const(name.c_str(), pin_group->size()).extract(index, index);
241  net_cache.insert({{net->get_id(), time_index}, bf});
242  return OK(bf);
243  }
244  }
245  }
246  }
247 
248  const auto bf = ctx.bv_const(("net_" + std::to_string(net->get_id()) + "_" + std::to_string(time_index)).c_str(), 1);
249  net_cache.insert({{net->get_id(), time_index}, bf});
250  return OK(bf);
251  }
252 
253  // check whether we reached a net that is part of a pin group with a multi bit calculation
254  for (auto it = all_src_modules.rbegin(); it != all_src_modules.rend(); it++)
255  {
256  const auto src_mod = *it;
257  if (src_mod->is_output_net(net))
258  {
259  const auto pin = src_mod->get_pin_by_net(net);
260  const auto [pin_group, index] = pin->get_group();
261 
262  if (const auto it = word_level_calculations.find(pin_group); it != word_level_calculations.end())
263  {
264  const auto& wlc_operation = it->second;
265 
266  // check whether we have known inputs
267  std::map<std::string, BooleanFunction> known_signals;
268  for (const auto& var_name : wlc_operation.get_variable_names())
269  {
270  if (var_name == "UNKNOWN_OPERATION")
271  {
272  continue;
273  }
274 
275  const auto var_net_res = BooleanFunctionNetDecorator::get_net_from(net->get_netlist(), var_name);
276  if (var_net_res.is_error())
277  {
278  return ERR_APPEND(var_net_res.get_error(),
279  "cannot get function of net " + net->get_name() + " with ID " + std::to_string(net->get_id())
280  + ": failed to extract index from word level computation variable");
281  }
282  const auto var_net = var_net_res.get();
283 
284  if (const auto it = known_inputs[time_index].find(var_net->get_id()); it != known_inputs[time_index].end())
285  {
286  known_signals.insert({var_name, BooleanFunction::Const(it->second ? 1 : 0, 1)});
287  }
288  }
289 
290  const auto wlc_simplified = wlc_operation.substitute(known_signals).get().simplify_local();
291 
292  std::map<std::string, z3::expr> operand_signals;
293  for (const auto& var_name : wlc_simplified.get_variable_names())
294  {
295  if (var_name == "UNKNOWN_OPERATION")
296  {
297  continue;
298  }
299 
300  const auto var_net = BooleanFunctionNetDecorator::get_net_from(net->get_netlist(), var_name).get();
301 
302  if (const auto it = net_cache.find({var_net->get_id(), time_index}); it != net_cache.end())
303  {
304  operand_signals.emplace(var_name, it->second);
305  }
306  else
307  {
308  return ERR("cannot get function of net " + net->get_name() + " with ID " + std::to_string(net->get_id()) + ": failed to find net id "
309  + std::to_string(var_net->get_id()) + " for time index " + std::to_string(time_index) + " in net cache");
310  }
311  }
312 
313  auto bf_word_level_z3 = z3_utils::from_bf(wlc_simplified, ctx, operand_signals);
314  // bf_word_level_z3 = bf_word_level_z3.simplify();
315 
316  // insert result into cache for all nets of the pin group
317  for (u32 pin_idx = 0; pin_idx < pin_group->size(); pin_idx++)
318  {
319  const auto pin_net = pin_group->get_pins().at(pin_idx)->get_net();
320 
321  // TODO remove
322  // std::cout << "Pin net: " << pin_net->get_id() << " - " << pin_net->get_name() << " at index " << pin_idx << std::endl;
323 
324  z3::expr pin_e = bf_word_level_z3.extract(pin_idx, pin_idx);
325  pin_e = z3_utils::simplify_local(pin_e).get();
326 
327  net_cache.insert({{pin_net->get_id(), time_index}, pin_e});
328  }
329 
330  return OK(bf_word_level_z3.extract(index, index));
331  }
332  }
333  }
334 
335  BooleanFunction bf;
336  if (has_sequential_src)
337  {
338  bf = get_function_of_seq_gate(src_gate, src_pin, time_index, gate_cache);
339  }
340  else
341  {
342  bf = get_function_of_gate(src_gate, src_pin, time_index, gate_cache);
343  }
344 
345  // substitute known values in gate function to prevent following irrelevant paths
346  for (const auto& var : bf.get_variable_names())
347  {
348  const std::vector<std::string> split = utils::split(var, '_');
349  const u32 var_net_id = std::stoi(split.at(1));
350  const u32 var_time_index = std::stoi(split.at(2));
351 
352  if (known_inputs[var_time_index].find(var_net_id) != known_inputs[var_time_index].end())
353  {
354  BooleanFunction::Value known_value = known_inputs[var_time_index].at(var_net_id) ? BooleanFunction::Value::ONE : BooleanFunction::Value::ZERO;
355  if (auto substitution = bf.substitute(var, BooleanFunction::Const(known_value)); substitution.is_ok())
356  {
357  bf = substitution.get();
358  }
359  else
360  {
361  log_error("sequential_symbolic_execution", "{}", substitution.get_error().get());
362  }
363  }
364  }
365 
366  // NOTE regular simplify seems to have a memory leak (maybe also some saved data in abc)
367  if (auto simplification = Simplification::local_simplification(bf); simplification.is_ok())
368  {
369  bf = simplification.get();
370  }
371  else
372  {
373  log_error("sequential_symbolic_execution", "{}", simplification.get_error().get());
374  }
375 
376  std::map<std::string, z3::expr> var_name_to_function;
377 
378  for (const auto& var : bf.get_variable_names())
379  {
380  const std::vector<std::string> split = utils::split(var, '_');
381  const u32 var_net_id = std::stoi(split.at(1));
382  const u32 var_time_index = std::stoi(split.at(2));
383 
384  // Net* var_net = net->get_netlist()->get_net_by_id(var_net_id);
385  // auto var_bf_res =
386  // get_function_of_net_z3_word_level(var_net, time_index, subgraph_gates_byte_map, known_inputs, word_level_calculations, gate_cache, net_cache, substitute_endpoints, ctx);
387  // if (var_bf_res.is_error())
388  // {
389  // return var_bf_res;
390  // }
391 
392  if (const auto it = net_cache.find({var_net_id, var_time_index}); it != net_cache.end())
393  {
394  var_name_to_function.emplace(var, it->second);
395  }
396  else
397  {
398  return ERR("cannot get function of net " + net->get_name() + " with ID " + std::to_string(net->get_id()) + ": failed to find net id " + std::to_string(var_net_id)
399  + " for time index " + std::to_string(var_time_index) + " in net cache");
400  }
401  }
402 
403  auto bf_z3 = z3_utils::from_bf(bf, ctx, var_name_to_function);
404 
405  // bf_z3 = bf_z3.simplify();
406  const auto simplify_res = z3_utils::simplify_local(bf_z3);
407  if (simplify_res.is_error())
408  {
409  return ERR_APPEND(simplify_res.get_error(), "cannot get function of net " + net->get_name() + " with ID " + std::to_string(net->get_id()) + ": failed to simplify expression");
410  }
411  bf_z3 = simplify_res.get();
412 
413  net_cache.insert({{net->get_id(), time_index}, bf_z3});
414  return OK(bf_z3);
415  }
416 
417  Result<std::vector<std::pair<Net*, u32>>> get_net_inputs(Net* net,
418  const u32 time_index,
419  const std::vector<bool>& subgraph_gates_byte_map,
420  const std::vector<std::map<u32, bool>>& known_inputs,
421  const std::map<PinGroup<ModulePin>*, BooleanFunction>& word_level_calculations,
422  std::map<std::tuple<u32, std::string, u32>, BooleanFunction>& gate_cache,
423  std::map<std::pair<u32, u32>, z3::expr>& net_cache)
424  {
425  // std::cout << "Getting missing inputs at time step " << time_index << " for net " << net->get_id() << " - " << net->get_name() << std::endl;
426 
427  std::vector<std::pair<Net*, u32>> indexed_net_inputs;
428 
429  if (net == nullptr)
430  {
431  return ERR("nullptr given for target net");
432  }
433  else if (net->get_num_of_sources() > 1)
434  {
435  return ERR("target net " + net->get_name() + " with ID " + std::to_string(net->get_id()) + "has more than one source");
436  }
437 
438  if (known_inputs.at(time_index).find(net->get_id()) != known_inputs.at(time_index).end())
439  {
440  return OK({});
441  }
442 
443  if (const auto it = net_cache.find({net->get_id(), time_index}); it != net_cache.end())
444  {
445  return OK({});
446  }
447 
448  if (net->is_global_input_net())
449  {
450  return OK({});
451  }
452 
453  if (net->get_num_of_sources() == 0)
454  {
455  // log_debug("sequential_symbolic_execution", "target net with ID {} has no sources.", net->get_id());
456 
457  return OK({});
458  }
459 
460  const Gate* src_gate = net->get_sources()[0]->get_gate();
461  const std::string src_pin = net->get_sources()[0]->get_pin()->get_name();
462  const bool has_sequential_src = src_gate->get_type()->has_property(GateTypeProperty::sequential);
463 
464  const auto all_src_modules = src_gate->get_modules(nullptr, true);
465 
466  // reached end of subgraph or time limit
467  if ((!subgraph_gates_byte_map.at(src_gate->get_id())) || (has_sequential_src && (time_index == 0)))
468  {
469  return OK({});
470  }
471 
472  // check whether we reached a net that is part of a pin group with a multi bit calculation
473  for (auto it = all_src_modules.rbegin(); it != all_src_modules.rend(); it++)
474  {
475  const auto src_mod = *it;
476  if (src_mod->is_output_net(net))
477  {
478  const auto pin = src_mod->get_pin_by_net(net);
479  const auto [pin_group, index] = pin->get_group();
480 
481  if (const auto it = word_level_calculations.find(pin_group); it != word_level_calculations.end())
482  {
483  const auto& wlc_operation = it->second;
484 
485  // check whether we have known inputs
486  std::map<std::string, BooleanFunction> known_signals;
487  for (const auto& var_name : wlc_operation.get_variable_names())
488  {
489  if (var_name == "UNKNOWN_OPERATION")
490  {
491  continue;
492  }
493 
494  const auto var_net_res = BooleanFunctionNetDecorator::get_net_from(net->get_netlist(), var_name);
495  if (var_net_res.is_error())
496  {
497  return ERR_APPEND(var_net_res.get_error(),
498  "cannot get missing net inputs of net " + net->get_name() + " with ID " + std::to_string(net->get_id())
499  + ": failed to extract index from word level computation variable");
500  }
501  const auto var_net = var_net_res.get();
502 
503  if (const auto it = known_inputs[time_index].find(var_net->get_id()); it != known_inputs[time_index].end())
504  {
505  known_signals.insert({var_name, BooleanFunction::Const(it->second ? 1 : 0, 1)});
506  }
507  }
508 
509  const auto wlc_simplified = wlc_operation.substitute(known_signals).get().simplify_local();
510 
511  for (const auto& var_name : wlc_simplified.get_variable_names())
512  {
513  if (var_name == "UNKNOWN_OPERATION")
514  {
515  continue;
516  }
517 
518  auto var_net = BooleanFunctionNetDecorator::get_net_from(net->get_netlist(), var_name).get();
519 
520  if (const auto it = net_cache.find({var_net->get_id(), time_index}); it == net_cache.end())
521  {
522  indexed_net_inputs.push_back(std::pair<Net*, u32>{var_net, time_index});
523  }
524  }
525 
526  return OK(indexed_net_inputs);
527  }
528  }
529  }
530 
531  BooleanFunction bf;
532  if (has_sequential_src)
533  {
534  bf = get_function_of_seq_gate(src_gate, src_pin, time_index, gate_cache);
535  }
536  else
537  {
538  bf = get_function_of_gate(src_gate, src_pin, time_index, gate_cache);
539  }
540 
541  // substitute known values in gate function to prevent following irrelevant paths
542  for (const auto& var : bf.get_variable_names())
543  {
544  const std::vector<std::string> split = utils::split(var, '_');
545  const u32 var_net_id = std::stoi(split.at(1));
546  const u32 var_time_index = std::stoi(split.at(2));
547 
548  if (known_inputs[var_time_index].find(var_net_id) != known_inputs[var_time_index].end())
549  {
550  BooleanFunction::Value known_value = known_inputs[var_time_index].at(var_net_id) ? BooleanFunction::Value::ONE : BooleanFunction::Value::ZERO;
551  if (auto substitution = bf.substitute(var, BooleanFunction::Const(known_value)); substitution.is_ok())
552  {
553  bf = substitution.get();
554  }
555  else
556  {
557  log_error("sequential_symbolic_execution", "{}", substitution.get_error().get());
558  }
559  }
560  }
561 
562  // NOTE regular simplify seems to have a memory leak (maybe also some saved data in abc)
563  if (auto simplification = Simplification::local_simplification(bf); simplification.is_ok())
564  {
565  bf = simplification.get();
566  }
567  else
568  {
569  log_error("sequential_symbolic_execution", "{}", simplification.get_error().get());
570  }
571 
572  for (const auto& var : bf.get_variable_names())
573  {
574  const std::vector<std::string> split = utils::split(var, '_');
575  const u32 var_net_id = std::stoi(split.at(1));
576  const u32 var_time_index = std::stoi(split.at(2));
577 
578  Net* var_net = net->get_netlist()->get_net_by_id(var_net_id);
579 
580  if (const auto it = net_cache.find({var_net_id, var_time_index}); it == net_cache.end())
581  {
582  indexed_net_inputs.push_back({var_net, var_time_index});
583  }
584  }
585 
586  return OK(indexed_net_inputs);
587  }
588 
589  Result<z3::expr> get_function_of_net_z3_word_level(Net* net,
590  const u32 time_index,
591  const std::vector<bool>& subgraph_gates_byte_map,
592  const std::vector<std::map<u32, bool>>& known_inputs,
593  const std::map<PinGroup<ModulePin>*, BooleanFunction>& word_level_calculations,
594  std::map<std::tuple<u32, std::string, u32>, BooleanFunction>& gate_cache,
595  std::map<std::pair<u32, u32>, z3::expr>& net_cache,
596  const bool substitute_endpoints,
597  z3::context& ctx)
598  {
599  std::vector<std::pair<Net*, u32>> stack = {std::pair<Net*, u32>{net, time_index}};
600  std::set<std::pair<Net*, u32>> visited = {std::pair<Net*, u32>{net, time_index}};
601 
602  while (!stack.empty())
603  {
604  const auto [n, t] = stack.back();
605  const auto missing_inputs_res = get_net_inputs(n, t, subgraph_gates_byte_map, known_inputs, word_level_calculations, gate_cache, net_cache);
606  if (missing_inputs_res.is_error())
607  {
608  return ERR_APPEND(missing_inputs_res.get_error(),
609  "cannot get function of net " + net->get_name() + " with ID " + std::to_string(net->get_id()) + ": failed to get missing input nets for net " + n->get_name()
610  + " with ID " + std::to_string(n->get_id()) + " at time index " + std::to_string(t));
611  }
612 
613  const auto missing_inputs = missing_inputs_res.get();
614 
615  if (!missing_inputs.empty())
616  {
617  const u32 before = stack.size();
618  for (const auto& nt : missing_inputs)
619  {
620  if (visited.find(nt) == visited.end())
621  {
622  stack.push_back(nt);
623  visited.insert(nt);
624  }
625  }
626 
627  // If the stack size did not change, just add the missing inputs no matter what to the back of the stack
628  // Otherwise the top element will keep "waiting" until its inputs are resolved, however they lay further down in the stack
629  if (stack.size() == before)
630  {
631  for (const auto& nt : missing_inputs)
632  {
633  stack.push_back(nt);
634  visited.insert(nt);
635  }
636  }
637 
638  continue;
639  }
640 
641  const auto bf_res =
642  get_function_of_net_z3_word_level_internal(n, t, subgraph_gates_byte_map, known_inputs, word_level_calculations, gate_cache, net_cache, substitute_endpoints, ctx);
643  if (bf_res.is_error())
644  {
645  return bf_res;
646  }
647 
648  if (stack.size() == 1)
649  {
650  return bf_res;
651  }
652 
653  stack.pop_back();
654  }
655 
656  return ERR("unreachable reached");
657  }
658 
659  Result<z3::expr> subsitute_nets_with_pins(const z3::expr& e, const Netlist* nl, const bool simplify)
660  {
661  const auto var_names = z3_utils::get_variable_names(e);
662 
663  z3::expr_vector from(e.ctx());
664  z3::expr_vector to(e.ctx());
665 
666  for (const auto& vn : var_names)
667  {
668  // check whether the variable is a net variable
669  if (vn.find("net_") != 0)
670  {
671  continue;
672  }
673 
674  const std::vector<std::string> split = utils::split(vn, '_');
675  const u32 var_net_id = std::stoi(split.at(1));
676  const u32 var_time_index = std::stoi(split.at(2));
677 
678  Net* net = nl->get_net_by_id(var_net_id);
679 
680  if (net->is_global_input_net())
681  {
682  const auto pin = nl->get_top_module()->get_pin_by_net(net);
683  const auto [pin_group, index] = pin->get_group();
684 
685  const std::string name = pin_group->get_name() + "_" + std::to_string(var_time_index);
686  const auto to_bf = e.ctx().bv_const(name.c_str(), pin_group->size()).extract(index, index);
687  const auto from_bf = e.ctx().bv_const(vn.c_str(), 1);
688 
689  // TODO remove
690  // std::cout << "FROM: " << from_bf << std::endl;
691  // std::cout << "TO: " << to_bf << std::endl;
692 
693  from.push_back(from_bf);
694  to.push_back(to_bf);
695 
696  continue;
697  }
698 
699  if (net->get_num_of_sources() != 1)
700  {
701  continue;
702  }
703 
704  const Gate* src_gate = net->get_sources()[0]->get_gate();
705  const std::string src_pin = net->get_sources()[0]->get_pin()->get_name();
706 
707  const auto all_src_modules = src_gate->get_modules(nullptr, true);
708 
709  // Find highest order module with an intact bitorder to substitute net with sliced bit field from module
710  for (auto it = all_src_modules.rbegin(); it != all_src_modules.rend(); it++)
711  {
712  const auto src_mod = *it;
713  if (src_mod->is_output_net(net))
714  {
715  const auto pin = src_mod->get_pin_by_net(net);
716  const auto [pin_group, index] = pin->get_group();
717 
718  if (pin_group->size() > 1)
719  {
720  const std::string name = src_mod->get_name() + "_" + pin_group->get_name() + "_" + std::to_string(var_time_index);
721  const auto to_bf = e.ctx().bv_const(name.c_str(), pin_group->size()).extract(index, index);
722  const auto from_bf = e.ctx().bv_const(vn.c_str(), 1);
723 
724  from.push_back(from_bf);
725  to.push_back(to_bf);
726 
727  break;
728  }
729  }
730  }
731  }
732 
733  auto e_cpy = e;
734  auto res = e_cpy.substitute(from, to);
735  if (simplify)
736  {
737  // res = res.simplify();
738  const auto simplify_res = z3_utils::simplify_local(res);
739  if (simplify_res.is_error())
740  {
741  return ERR_APPEND(simplify_res.get_error(), "cannot substitute endpoints for z3::expr: failed to simplify expression");
742  }
743  res = simplify_res.get();
744  }
745 
746  return OK(res);
747  }
748 
749  } // namespace
750 
751  Result<z3::expr> get_value_at_z3(Net* net,
752  const u32 time_index,
753  const std::vector<bool>& subgraph_gates_byte_map,
754  const std::vector<std::map<u32, bool>>& known_inputs,
755  const std::map<PinGroup<ModulePin>*, BooleanFunction>& word_level_calculations,
756  const bool substitute_endpoints,
757  z3::context& ctx)
758  {
759  std::map<std::tuple<u32, std::string, u32>, BooleanFunction> gate_cache;
760  std::map<std::pair<u32, u32>, z3::expr> net_cache;
761 
762  auto bf_res = sse::get_function_of_net_z3_word_level(net, time_index, subgraph_gates_byte_map, known_inputs, word_level_calculations, gate_cache, net_cache, substitute_endpoints, ctx);
763 
764  return bf_res;
765  }
766 
767  Result<std::vector<z3::expr>> get_word_values_at_z3(const std::vector<std::vector<Net*>>& words,
768  const std::vector<u32>& time_indices,
769  const std::vector<bool>& subgraph_gates_byte_map,
770  const std::vector<std::map<u32, bool>>& known_inputs,
771  const std::map<PinGroup<ModulePin>*, BooleanFunction>& word_level_calculations,
772  const bool substitute_endpoints,
773  z3::context& ctx)
774  {
775  std::map<std::tuple<u32, std::string, u32>, BooleanFunction> gate_cache;
776  std::map<std::pair<u32, u32>, z3::expr> net_cache;
777 
778  std::vector<z3::expr> result;
779 
780  for (u32 word_idx = 0; word_idx < words.size(); word_idx++)
781  {
782  const auto& nets = words.at(word_idx);
783  const auto bf_res =
784  sse::get_function_of_net_z3_word_level(nets.front(), time_indices.at(word_idx), subgraph_gates_byte_map, known_inputs, word_level_calculations, gate_cache, net_cache, false, ctx);
785 
786  if (bf_res.is_error())
787  {
788  return ERR_APPEND(bf_res.get_error(), "cannot get word value for word at index " + std::to_string(word_idx) + ": failed to build single net function");
789  }
790 
791  z3::expr bf_word = bf_res.get();
792  for (u32 bit_idx = 1; bit_idx < nets.size(); bit_idx++)
793  {
794  const auto bf_bit_res = sse::get_function_of_net_z3_word_level(
795  nets.at(bit_idx), time_indices.at(word_idx), subgraph_gates_byte_map, known_inputs, word_level_calculations, gate_cache, net_cache, false, ctx);
796  if (bf_bit_res.is_error())
797  {
798  return ERR_APPEND(bf_res.get_error(), "cannot get word value for word at index " + std::to_string(word_idx) + ": failed to build single net function");
799  }
800 
801  bf_word = z3::concat(bf_bit_res.get(), bf_word);
802  }
803 
804  if (substitute_endpoints)
805  {
806  const Netlist* nl = words.front().front()->get_netlist();
807  const auto substitute_res = subsitute_nets_with_pins(bf_word, nl, true);
808  if (substitute_res.is_error())
809  {
810  return ERR_APPEND(substitute_res.get_error(), "cannot get word value for word at index " + std::to_string(word_idx) + ": failed to substitute nets with pins");
811  }
812  bf_word = substitute_res.get();
813  }
814 
815  // bf_word = bf_word.simplify();
816  const auto simplify_res = z3_utils::simplify_local(bf_word);
817  if (simplify_res.is_error())
818  {
819  return ERR_APPEND(simplify_res.get_error(), "cannot get word value for word at index " + std::to_string(word_idx) + ": failed to simplify expression");
820  }
821  bf_word = simplify_res.get();
822 
823  result.push_back(bf_word);
824  }
825 
826  return OK(result);
827  }
828 
829  Result<std::vector<z3::expr>> get_word_values_at_z3(const std::vector<std::pair<Module*, PinGroup<ModulePin>*>>& words,
830  const std::vector<u32>& time_indices,
831  const std::vector<bool>& subgraph_gates_byte_map,
832  const std::vector<std::map<u32, bool>>& known_inputs,
833  const std::map<PinGroup<ModulePin>*, BooleanFunction>& word_level_calculations,
834  const bool substitute_endpoints,
835  z3::context& ctx)
836  {
837  std::map<std::tuple<u32, std::string, u32>, BooleanFunction> gate_cache;
838  std::map<std::pair<u32, u32>, z3::expr> net_cache;
839 
840  std::vector<std::vector<Net*>> word_nets;
841 
842  for (const auto& [_m, pg] : words)
843  {
844  std::vector<Net*> nets;
845  for (const auto& pin : pg->get_pins())
846  {
847  nets.push_back(pin->get_net());
848  }
849  word_nets.push_back(nets);
850  }
851 
852  return get_word_values_at_z3(word_nets, time_indices, subgraph_gates_byte_map, known_inputs, word_level_calculations, substitute_endpoints, ctx);
853  }
854 
855  } // namespace sse
856 } // namespace hal
boolean_function_net_decorator.h
hal::BooleanFunction::Value
Value
represents the type of the node
Definition: boolean_function.h:74
hal::BooleanFunction::Const
static BooleanFunction Const(const BooleanFunction::Value &value)
Definition: boolean_function.cpp:256
hal::BooleanFunctionNetDecorator::get_net_from
static Result< Net * > get_net_from(const Netlist *netlist, const BooleanFunction &var)
Definition: boolean_function_net_decorator.cpp:44
hal::Net
Definition: net.h:58
u32
uint32_t u32
Definition: defines.h:41
ff_component.h
hal::ItemType::Net
@ Net
hal::ItemType::Gate
@ Gate
log_error
#define log_error(channel,...)
Definition: log.h:78
log_warning
#define log_warning(channel,...)
Definition: log.h:76
simplification.h
netlist.h
ERR
#define ERR(message)
Definition: result.h:60
OK
#define OK(...)
Definition: result.h:56
ERR_APPEND
#define ERR_APPEND(prev_error, message)
Definition: result.h:64
utils.h
hal::Simplification::local_simplification
Result< BooleanFunction > local_simplification(const BooleanFunction &function)
Definition: simplification_local.cpp:6
hal::core_strings::to
S to(const T &str)
Definition: special_strings.h:48
hal::sse::get_value_at_z3
Result< z3::expr > get_value_at_z3(Net *net, const u32 time_index, const std::vector< bool > &subgraph_gates_byte_map, const std::vector< std::map< u32, bool >> &known_inputs, const std::map< PinGroup< ModulePin > *, BooleanFunction > &word_level_calculations, const bool substitute_endpoints, z3::context &ctx)
Get the Z3 expression representing the value of a net at a specific time index.
Definition: sequential_symbolic_execution.cpp:751
hal::sse::get_word_values_at_z3
Result< std::vector< z3::expr > > get_word_values_at_z3(const std::vector< std::vector< Net * >> &words, const std::vector< u32 > &time_indices, const std::vector< bool > &subgraph_gates_byte_map, const std::vector< std::map< u32, bool >> &known_inputs, const std::map< PinGroup< ModulePin > *, BooleanFunction > &word_level_calculations, const bool substitute_endpoints, z3::context &ctx)
Get the Z3 expressions representing the values of multiple nets as words at specific time indices.
Definition: sequential_symbolic_execution.cpp:767
hal::utils::to_vector
std::vector< T > to_vector(const Container< T, Args... > &container)
Definition: utils.h:515
hal::utils::split
std::vector< T > split(const T &s, const char delim, bool obey_brackets=false)
Definition: utils.h:239
hal::z3_utils::get_variable_names
std::set< std::string > get_variable_names(const z3::expr &e)
Extracts all variable names from a z3 expression.
Definition: z3_utils.cpp:481
hal::z3_utils::simplify_local
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.
Definition: simplification.cpp:2020
hal::z3_utils::from_bf
z3::expr from_bf(const BooleanFunction &bf, z3::context &ctx, const std::map< std::string, z3::expr > &var2expr={})
Definition: z3_utils.cpp:15
hal::z3_utils::to_bf
Result< BooleanFunction > to_bf(const z3::expr &e)
Definition: z3_utils.cpp:443
hal
Definition: defines.h:45
hal::PinDirection
PinDirection
Definition: pin_direction.h:36
net
Net * net
Definition: netlist_serializer.cpp:57
name
std::string name
Definition: netlist_serializer.cpp:58
index
u32 index
Definition: netlist_preprocessing.cpp:1963
simplification.h
z3_utils.h