From ac6fcb2547085d041a432a3182a3bfb2c3d2e6ea Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 19 Jan 2024 15:36:14 +0100 Subject: [PATCH] write_aiger: Detect and error out on combinational loops Without this it will overflow the stack when loops are present. --- backends/aiger/aiger.cc | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index bb804f230fb..f77a6497845 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -54,6 +54,8 @@ struct AigerWriter vector> aig_gates; vector aig_latchin, aig_latchinit, aig_outputs; + vector bit2aig_stack; + size_t next_loop_check = 1024; int aig_m = 0, aig_i = 0, aig_l = 0, aig_o = 0, aig_a = 0; int aig_b = 0, aig_c = 0, aig_j = 0, aig_f = 0; @@ -81,6 +83,23 @@ struct AigerWriter return it->second; } + if (bit2aig_stack.size() == next_loop_check) { + for (size_t i = 0; i < next_loop_check; ++i) + { + SigBit report_bit = bit2aig_stack[i]; + if (report_bit != bit) + continue; + for (size_t j = i; j < next_loop_check; ++j) { + report_bit = bit2aig_stack[j]; + if (report_bit.is_wire() && report_bit.wire->name.isPublic()) + break; + } + log_error("Found combinational logic loop while processing signal %s.\n", log_signal(report_bit)); + } + next_loop_check *= 2; + } + bit2aig_stack.push_back(bit); + // NB: Cannot use iterator returned from aig_map.insert() // since this function is called recursively @@ -101,6 +120,8 @@ struct AigerWriter a = initstate_ff; } + bit2aig_stack.pop_back(); + if (bit == State::Sx || bit == State::Sz) log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n");