From c23bbc429103ca84cb8a9cfb674aacf7d14109c6 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 16 Jun 2019 23:12:03 +0200 Subject: Add timescale and generated-by header to yosys-smtbmc MkVcd Signed-off-by: Clifford Wolf --- backends/smt2/smtio.py | 2 ++ 1 file changed, 2 insertions(+) (limited to 'backends') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index ab20a4af2..cea0fc56c 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -1023,6 +1023,8 @@ class MkVcd: assert t >= self.t if t != self.t: if self.t == -1: + print("$version Generated by Yosys-SMTBMC $end", file=self.f) + print("$timescale 1ns $end", file=self.f) print("$var integer 32 t smt_step $end", file=self.f) print("$var event 1 ! smt_clock $end", file=self.f) -- cgit v1.2.3 From 4a18e19fb86f5729ca764d5b0ee338f558f90a43 Mon Sep 17 00:00:00 2001 From: Ben Widawsky Date: Mon, 17 Jun 2019 14:45:48 -0700 Subject: Support filename rewrite in backends Signed-off-by: Ben Widawsky --- backends/aiger/aiger.cc | 1 + backends/ilang/ilang_backend.cc | 1 + backends/json/json.cc | 1 + backends/protobuf/protobuf.cc | 1 + 4 files changed, 4 insertions(+) (limited to 'backends') diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index dfe506c66..d685c5638 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -776,6 +776,7 @@ struct AigerBackend : public Backend { writer.write_aiger(*f, ascii_mode, miter_mode, symbols_mode); if (!map_filename.empty()) { + rewrite_filename(filename); std::ofstream mapf; mapf.open(map_filename.c_str(), std::ofstream::trunc); if (mapf.fail()) diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc index 04d1ee311..b4ba2b03f 100644 --- a/backends/ilang/ilang_backend.cc +++ b/backends/ilang/ilang_backend.cc @@ -483,6 +483,7 @@ struct DumpPass : public Pass { std::stringstream buf; if (!filename.empty()) { + rewrite_filename(filename); std::ofstream *ff = new std::ofstream; ff->open(filename.c_str(), append ? std::ofstream::app : std::ofstream::trunc); if (ff->fail()) { diff --git a/backends/json/json.cc b/backends/json/json.cc index f5c687981..5022d5da1 100644 --- a/backends/json/json.cc +++ b/backends/json/json.cc @@ -525,6 +525,7 @@ struct JsonPass : public Pass { std::stringstream buf; if (!filename.empty()) { + rewrite_filename(filename); std::ofstream *ff = new std::ofstream; ff->open(filename.c_str(), std::ofstream::trunc); if (ff->fail()) { diff --git a/backends/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc index 549fc73ae..fff110bb0 100644 --- a/backends/protobuf/protobuf.cc +++ b/backends/protobuf/protobuf.cc @@ -336,6 +336,7 @@ struct ProtobufPass : public Pass { std::stringstream buf; if (!filename.empty()) { + rewrite_filename(filename); std::ofstream *ff = new std::ofstream; ff->open(filename.c_str(), std::ofstream::trunc); if (ff->fail()) { -- cgit v1.2.3 From f2d541962e92fedce0fbb34d4cf5c1985c7cda40 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 20 Jun 2019 10:21:57 -0700 Subject: write_xaiger to skip POs driven by 1'bx --- backends/aiger/xaiger.cc | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 1485e2b0c..12b23cfe9 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -152,9 +152,13 @@ struct XAigerWriter } if (wire->port_output || keep) { - if (bit != wirebit) - alias_map[wirebit] = bit; - output_bits.insert(wirebit); + if (bit != RTLIL::Sx) { + if (bit != wirebit) + alias_map[wirebit] = bit; + output_bits.insert(wirebit); + } + else + log_debug("Skipping PO '%s' driven by 1'bx\n", log_signal(wirebit)); } } } -- cgit v1.2.3 From 4e5836a5fb009751a6f3bd7ec3eba20e223861f1 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 20 Jun 2019 10:47:20 -0700 Subject: Handle COs driven by 1'bx --- backends/aiger/xaiger.cc | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 12b23cfe9..42f54209b 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -355,10 +355,16 @@ struct XAigerWriter } int offset = 0; - for (const auto &b : rhs.bits()) { + for (auto b : rhs.bits()) { SigBit I = sigmap(b); - if (I != b) - alias_map[b] = I; + if (b == RTLIL::Sx) + b = RTLIL::S0; + else if (I != b) { + if (I == RTLIL::Sx) + alias_map[b] = RTLIL::S0; + else + alias_map[b] = I; + } co_bits.emplace_back(b, cell, port_name, offset++, 0); unused_bits.erase(b); } -- cgit v1.2.3 From 9faeba7a66c34d57bcae6ad83580e640ee5907e6 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 20 Jun 2019 19:27:00 -0700 Subject: Fix broken abc9.v test due to inout being 1'bx --- backends/aiger/xaiger.cc | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 42f54209b..f0a9ccdb9 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -75,6 +75,7 @@ struct XAigerWriter dict ordered_outputs; vector box_list; + bool omode = false; int mkgate(int a0, int a1) { @@ -409,9 +410,9 @@ struct XAigerWriter // If encountering an inout port, or a keep-ed wire, then create a new wire // with $inout.out suffix, make it a PO driven by the existing inout, and // inherit existing inout's drivers - if ((wire->port_input && wire->port_output && !undriven_bits.count(bit)) + if ((wire->port_input && wire->port_output && output_bits.count(bit) && !undriven_bits.count(bit)) || wire->attributes.count("\\keep")) { - log_assert(input_bits.count(bit) && output_bits.count(bit)); + log_assert(output_bits.count(bit)); RTLIL::IdString wire_name = wire->name.str() + "$inout.out"; RTLIL::Wire *new_wire = module->wire(wire_name); if (!new_wire) @@ -486,6 +487,12 @@ struct XAigerWriter ordered_outputs[bit] = aig_o++; aig_outputs.push_back(bit2aig(bit)); } + + if (output_bits.empty()) { + aig_o++; + aig_outputs.push_back(0); + omode = true; + } } void write_aiger(std::ostream &f, bool ascii_mode) @@ -741,6 +748,8 @@ struct XAigerWriter for (auto &it : output_lines) f << it.second; log_assert(output_lines.size() == output_bits.size()); + if (omode && output_bits.empty()) + f << "output " << output_lines.size() << " 0 $__dummy__\n"; wire_lines.sort(); for (auto &it : wire_lines) -- cgit v1.2.3 From ad36eb24c05b578ec8610c9f199280aacefebe54 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 20 Jun 2019 19:31:22 -0700 Subject: Fix different abc9 test --- backends/aiger/xaiger.cc | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index f0a9ccdb9..55a95d835 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -406,13 +406,14 @@ struct XAigerWriter } for (auto bit : input_bits) { + if (!output_bits.count(bit)) + continue; RTLIL::Wire *wire = bit.wire; // If encountering an inout port, or a keep-ed wire, then create a new wire // with $inout.out suffix, make it a PO driven by the existing inout, and // inherit existing inout's drivers - if ((wire->port_input && wire->port_output && output_bits.count(bit) && !undriven_bits.count(bit)) + if ((wire->port_input && wire->port_output && !undriven_bits.count(bit)) || wire->attributes.count("\\keep")) { - log_assert(output_bits.count(bit)); RTLIL::IdString wire_name = wire->name.str() + "$inout.out"; RTLIL::Wire *new_wire = module->wire(wire_name); if (!new_wire) -- cgit v1.2.3 From 8e56cfb6bbaa4e61b201c123b04a4eb4ca3403cf Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 20 Jun 2019 19:40:17 -0700 Subject: write_xaiger to flatten 1'bx/1'bz to 1'b0 again --- backends/aiger/xaiger.cc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 55a95d835..82f0f24b2 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -104,8 +104,10 @@ struct XAigerWriter aig_map[bit] = bit2aig(alias_map.at(bit)); } - if (bit == State::Sx || bit == State::Sz) - log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n"); + if (bit == State::Sx || bit == State::Sz) { + log_debug("Bit '%s' contains 'x' or 'z' bits. Treating as 1'b0.\n", log_signal(bit)); + aig_map[bit] = 0; + } } log_assert(aig_map.at(bit) >= 0); -- cgit v1.2.3 From c4ea6fff65d6b2e69a31649af7e10b129c6ae0f5 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 20 Jun 2019 21:56:02 -0700 Subject: Fix gcc invalidation behaviour for write_aiger --- backends/aiger/aiger.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index d685c5638..6863b40fa 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -89,7 +89,8 @@ struct AigerWriter aig_map[bit] = mkgate(a0, a1); } else if (alias_map.count(bit)) { - aig_map[bit] = bit2aig(alias_map.at(bit)); + int a = bit2aig(alias_map.at(bit)); + aig_map[bit] = a; } if (bit == State::Sx || bit == State::Sz) -- cgit v1.2.3 From 32f8014e121cd3338d6786269455c8b3fe9f1631 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 20 Jun 2019 21:55:08 -0700 Subject: Fix gcc error, due to dict invalidation during recursion --- backends/aiger/xaiger.cc | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 82f0f24b2..32c3f9045 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -101,12 +101,13 @@ struct XAigerWriter aig_map[bit] = mkgate(a0, a1); } else if (alias_map.count(bit)) { - aig_map[bit] = bit2aig(alias_map.at(bit)); + int a = bit2aig(alias_map.at(bit)); + aig_map[bit] = a; } if (bit == State::Sx || bit == State::Sz) { log_debug("Bit '%s' contains 'x' or 'z' bits. Treating as 1'b0.\n", log_signal(bit)); - aig_map[bit] = 0; + aig_map[bit] = aig_map.at(State::S0); } } -- cgit v1.2.3 From 4422b7311b8d672df386f993b413d32baad8550b Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 20 Jun 2019 21:56:02 -0700 Subject: Fix gcc invalidation behaviour for write_aiger --- backends/aiger/aiger.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 4c2ea511a..4fb47f0d6 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -89,7 +89,8 @@ struct AigerWriter aig_map[bit] = mkgate(a0, a1); } else if (alias_map.count(bit)) { - aig_map[bit] = bit2aig(alias_map.at(bit)); + int a = bit2aig(alias_map.at(bit)); + aig_map[bit] = a; } if (bit == State::Sx || bit == State::Sz) -- cgit v1.2.3 From e21f01d9380607ba0fb10466273d2dfc3d806282 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 20 Jun 2019 22:09:13 -0700 Subject: Refactor bit2aig for less lookups --- backends/aiger/xaiger.cc | 51 +++++++++++++++++++++++++----------------------- 1 file changed, 27 insertions(+), 24 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 32c3f9045..48e902666 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -86,33 +86,36 @@ struct XAigerWriter int bit2aig(SigBit bit) { - if (aig_map.count(bit) == 0) - { - aig_map[bit] = -1; - - if (not_map.count(bit)) { - int a = bit2aig(not_map.at(bit)) ^ 1; - aig_map[bit] = a; - } else - if (and_map.count(bit)) { - auto args = and_map.at(bit); - int a0 = bit2aig(args.first); - int a1 = bit2aig(args.second); - aig_map[bit] = mkgate(a0, a1); - } else - if (alias_map.count(bit)) { - int a = bit2aig(alias_map.at(bit)); - aig_map[bit] = a; - } + // NB: Cannot use iterator returned from aig_map.insert() + // since this function is called recursively + auto it = aig_map.find(bit); + if (it != aig_map.end()) { + log_assert(it->second >= 0); + return it->second; + } - if (bit == State::Sx || bit == State::Sz) { - log_debug("Bit '%s' contains 'x' or 'z' bits. Treating as 1'b0.\n", log_signal(bit)); - aig_map[bit] = aig_map.at(State::S0); - } + int a = -1; + if (not_map.count(bit)) { + a = bit2aig(not_map.at(bit)) ^ 1; + } else + if (and_map.count(bit)) { + auto args = and_map.at(bit); + int a0 = bit2aig(args.first); + int a1 = bit2aig(args.second); + a = mkgate(a0, a1); + } else + if (alias_map.count(bit)) { + a = bit2aig(alias_map.at(bit)); + } + + if (bit == State::Sx || bit == State::Sz) { + log_debug("Bit '%s' contains 'x' or 'z' bits. Treating as 1'b0.\n", log_signal(bit)); + a = aig_map.at(State::S0); } - log_assert(aig_map.at(bit) >= 0); - return aig_map.at(bit); + log_assert(a >= 0); + aig_map[bit] = a; + return a; } XAigerWriter(Module *module, bool holes_mode=false) : module(module), sigmap(module) -- cgit v1.2.3 From 6a336ca23ef5d98b3d68dac2f05de49360237149 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 20 Jun 2019 22:29:40 -0700 Subject: Fix spacing --- backends/aiger/aiger.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 4fb47f0d6..2815abda8 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -89,7 +89,7 @@ struct AigerWriter aig_map[bit] = mkgate(a0, a1); } else if (alias_map.count(bit)) { - int a = bit2aig(alias_map.at(bit)); + int a = bit2aig(alias_map.at(bit)); aig_map[bit] = a; } -- cgit v1.2.3 From f15def325c7f2621cf8299ca61b5eeb3ddd3667e Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 21 Jun 2019 15:22:17 +0200 Subject: Added JSON upto and offset Signed-off-by: Clifford Wolf --- backends/json/json.cc | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'backends') diff --git a/backends/json/json.cc b/backends/json/json.cc index 5022d5da1..1781a28cd 100644 --- a/backends/json/json.cc +++ b/backends/json/json.cc @@ -189,6 +189,10 @@ struct JsonWriter f << stringf(" %s: {\n", get_name(w->name).c_str()); f << stringf(" \"hide_name\": %s,\n", w->name[0] == '$' ? "1" : "0"); f << stringf(" \"bits\": %s,\n", get_bits(w).c_str()); + if (w->start_offset) + f << stringf(" \"offset\": %d,\n", w->start_offset); + if (w->upto) + f << stringf(" \"upto\": 1,\n"); f << stringf(" \"attributes\": {"); write_parameters(w->attributes); f << stringf("\n }\n"); -- cgit v1.2.3 From 50e72210772f3a1c34f5fe80b19c65f6d304b71a Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 21 Jun 2019 19:47:25 +0200 Subject: Add upto and offset to JSON ports --- backends/json/json.cc | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'backends') diff --git a/backends/json/json.cc b/backends/json/json.cc index 1781a28cd..eb59e5eba 100644 --- a/backends/json/json.cc +++ b/backends/json/json.cc @@ -127,6 +127,10 @@ struct JsonWriter f << stringf(" %s: {\n", get_name(n).c_str()); f << stringf(" \"direction\": \"%s\",\n", w->port_input ? w->port_output ? "inout" : "input" : "output"); f << stringf(" \"bits\": %s\n", get_bits(w).c_str()); + if (w->start_offset) + f << stringf(" \"offset\": %d,\n", w->start_offset); + if (w->upto) + f << stringf(" \"upto\": 1,\n"); f << stringf(" }"); first = false; } -- cgit v1.2.3 From fde90f7f8eb4150c7f806ab4baa53057a56bc160 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 21 Jun 2019 20:01:40 +0200 Subject: Fix json formatting --- backends/json/json.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/json/json.cc b/backends/json/json.cc index eb59e5eba..dda4dfedd 100644 --- a/backends/json/json.cc +++ b/backends/json/json.cc @@ -126,11 +126,11 @@ struct JsonWriter f << stringf("%s\n", first ? "" : ","); f << stringf(" %s: {\n", get_name(n).c_str()); f << stringf(" \"direction\": \"%s\",\n", w->port_input ? w->port_output ? "inout" : "input" : "output"); - f << stringf(" \"bits\": %s\n", get_bits(w).c_str()); if (w->start_offset) f << stringf(" \"offset\": %d,\n", w->start_offset); if (w->upto) f << stringf(" \"upto\": 1,\n"); + f << stringf(" \"bits\": %s\n", get_bits(w).c_str()); f << stringf(" }"); first = false; } -- cgit v1.2.3 From 70c93ea0c4ce023d61553df11198aa0b7e518455 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 21 Jun 2019 12:43:20 -0700 Subject: Move comment --- backends/aiger/xaiger.cc | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 48e902666..aa10aa55e 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -86,14 +86,15 @@ struct XAigerWriter int bit2aig(SigBit bit) { - // NB: Cannot use iterator returned from aig_map.insert() - // since this function is called recursively auto it = aig_map.find(bit); if (it != aig_map.end()) { log_assert(it->second >= 0); return it->second; } + // NB: Cannot use iterator returned from aig_map.insert() + // since this function is called recursively + int a = -1; if (not_map.count(bit)) { a = bit2aig(not_map.at(bit)) ^ 1; -- cgit v1.2.3 From bd7ec673dd5b542031698074e1043dcc32af2168 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 21 Jun 2019 12:46:55 -0700 Subject: No point logging constant bit --- backends/aiger/xaiger.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index aa10aa55e..6718e4f2c 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -110,7 +110,7 @@ struct XAigerWriter } if (bit == State::Sx || bit == State::Sz) { - log_debug("Bit '%s' contains 'x' or 'z' bits. Treating as 1'b0.\n", log_signal(bit)); + log_debug("Design contains 'x' or 'z' bits. Treating as 1'b0.\n"); a = aig_map.at(State::S0); } -- cgit v1.2.3 From 65c1199acd52f90de86106652dbbca86d4ac5ebc Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 21 Jun 2019 14:35:58 -0700 Subject: One more workaround for gcc-4.8 --- backends/aiger/xaiger.cc | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 6718e4f2c..637c54ff9 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -429,12 +429,13 @@ struct XAigerWriter module->connect(new_bit, bit); if (not_map.count(bit)) not_map[new_bit] = not_map.at(bit); - else if (and_map.count(bit)) - and_map[new_bit] = and_map.at(bit); + else if (and_map.count(bit)) { + //and_map[new_bit] = and_map.at(bit); // Breaks gcc-4.8 + and_map.insert(std::make_pair(new_bit, and_map.at(bit))); + } else if (alias_map.count(bit)) alias_map[new_bit] = alias_map.at(bit); else - //log_abort(); alias_map[new_bit] = bit; output_bits.erase(bit); output_bits.insert(new_bit); -- cgit v1.2.3 From 7074ec9cd5d5b5c01e3bbaa8ee45dbae1272f185 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 21 Jun 2019 17:16:38 -0700 Subject: Add log_push()/log_pop() inside write_xaiger --- backends/aiger/xaiger.cc | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 637c54ff9..2070cae8f 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -664,6 +664,8 @@ struct XAigerWriter f.write(buffer_str.data(), buffer_str.size()); if (holes_module) { + log_push(); + // NB: fixup_ports() will sort ports by name //holes_module->fixup_ports(); holes_module->check(); @@ -700,6 +702,8 @@ struct XAigerWriter f.write(reinterpret_cast(&buffer_size_be), sizeof(buffer_size_be)); f.write(buffer_str.data(), buffer_str.size()); holes_module->design->remove(holes_module); + + log_pop(); } } -- cgit v1.2.3 From fddb027cabedff92441b912a6cc472650aa9f74d Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 21 Jun 2019 15:45:51 -0700 Subject: Replace assert with error message --- backends/aiger/xaiger.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 2070cae8f..23132f108 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -244,7 +244,8 @@ struct XAigerWriter if (c.second.is_fully_const()) continue; auto is_input = cell->input(c.first); auto is_output = cell->output(c.first); - log_assert(is_input || is_output); + if (!is_input && !is_output) + log_error("Connection '%s' on cell '%s' (type '%s') not recognised!\n", log_id(c.first), log_id(cell), log_id(cell->type)); if (is_input) { for (auto b : c.second.bits()) { -- cgit v1.2.3 From 7903ebe3e004c03e7870f1b21c4fb478481756eb Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Sat, 22 Jun 2019 14:18:42 -0700 Subject: Carry in/out box ordering now move to end, not swap with end --- backends/aiger/xaiger.cc | 60 +++++++++++++++++++++++++++--------------------- 1 file changed, 34 insertions(+), 26 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 23132f108..7cfe8272c 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -309,38 +309,46 @@ struct XAigerWriter if (box_module->attributes.count("\\abc_carry") && !abc_carry_modules.count(box_module)) { RTLIL::Wire* carry_in = nullptr, *carry_out = nullptr; - RTLIL::Wire* last_in = nullptr, *last_out = nullptr; - for (const auto &port_name : box_module->ports) { - RTLIL::Wire* w = box_module->wire(port_name); + auto &ports = box_module->ports; + for (auto it = ports.begin(); it != ports.end(); ) { + RTLIL::Wire* w = box_module->wire(*it); log_assert(w); - if (w->port_input) { - if (w->attributes.count("\\abc_carry_in")) { - log_assert(!carry_in); - carry_in = w; - } - log_assert(!last_in || last_in->port_id < w->port_id); - last_in = w; + if (w->port_input && w->attributes.count("\\abc_carry_in")) { + if (carry_in) + log_error("More than one port with attribute 'abc_carry_in' found in module '%s'\n", log_id(box_module)); + carry_in = w; + it = ports.erase(it); + continue; } - if (w->port_output) { - if (w->attributes.count("\\abc_carry_out")) { - log_assert(!carry_out); - carry_out = w; - } - log_assert(!last_out || last_out->port_id < w->port_id); - last_out = w; + if (w->port_output && w->attributes.count("\\abc_carry_out")) { + if (carry_out) + log_error("More than one port with attribute 'abc_carry_out' found in module '%s'\n", log_id(box_module)); + carry_out = w; + it = ports.erase(it); + continue; } + ++it; } - if (carry_in) { - log_assert(last_in); - std::swap(box_module->ports[carry_in->port_id-1], box_module->ports[last_in->port_id-1]); - std::swap(carry_in->port_id, last_in->port_id); - } - if (carry_out) { - log_assert(last_out); - std::swap(box_module->ports[carry_out->port_id-1], box_module->ports[last_out->port_id-1]); - std::swap(carry_out->port_id, last_out->port_id); + if (!carry_in) + log_error("Port with attribute 'abc_carry_in' not found in module '%s'\n", log_id(box_module)); + if (!carry_out) + log_error("Port with attribute 'abc_carry_out' not found in module '%s'\n", log_id(box_module)); + + for (const auto port_name : ports) { + RTLIL::Wire* w = box_module->wire(port_name); + log_assert(w); + if (w->port_id > carry_in->port_id) + --w->port_id; + if (w->port_id > carry_out->port_id) + --w->port_id; + log_assert(w->port_input || w->port_output); + log_assert(ports[w->port_id-1] == w->name); } + ports.push_back(carry_in->name); + carry_in->port_id = ports.size(); + ports.push_back(carry_out->name); + carry_out->port_id = ports.size(); } // Fully pad all unused input connections of this box cell with S0 -- cgit v1.2.3 From 080a5ca536bcd7140ea3dc12483e49a8f076cd92 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 26 Jun 2019 20:02:38 -0700 Subject: Improve debugging message for comb loops --- backends/aiger/xaiger.cc | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 7cfe8272c..92df899c2 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -293,10 +293,12 @@ struct XAigerWriter #if 0 unsigned i = 0; for (auto &it : toposort.loops) { - log(" loop %d", i++); - for (auto cell : it) - log(" %s", log_id(cell)); - log("\n"); + log(" loop %d\n", i++); + for (auto cell_name : it) { + auto cell = module->cell(cell_name); + log_assert(cell); + log("\t%s (%s @ %s)\n", log_id(cell), log_id(cell->type), cell->get_src_attribute().c_str()); + } } #endif log_assert(no_loops); -- cgit v1.2.3 From 6c256b8cda66e2ba128d5fa3ba344fe4717711f8 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 27 Jun 2019 11:20:15 -0700 Subject: Merge origin/master --- backends/btor/btor.cc | 30 +++++++++++++++++++++++++++--- backends/smt2/smtio.py | 5 ++++- 2 files changed, 31 insertions(+), 4 deletions(-) (limited to 'backends') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 511a11942..a507b120b 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -17,6 +17,11 @@ * */ +// [[CITE]] Btor2 , BtorMC and Boolector 3.0 +// Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere +// Computer Aided Verification - 30th International Conference, CAV 2018 +// https://cs.stanford.edu/people/niemetz/publication/2018/niemetzpreinerwolfbiere-cav18/ + #include "kernel/rtlil.h" #include "kernel/register.h" #include "kernel/sigtools.h" @@ -875,9 +880,28 @@ struct BtorWorker else { if (bit_cell.count(bit) == 0) - log_error("No driver for signal bit %s.\n", log_signal(bit)); - export_cell(bit_cell.at(bit)); - log_assert(bit_nid.count(bit)); + { + SigSpec s = bit; + + while (i+GetSize(s) < GetSize(sig) && sig[i+GetSize(s)].wire != nullptr && + bit_cell.count(sig[i+GetSize(s)]) == 0) + s.append(sig[i+GetSize(s)]); + + log_warning("No driver for signal %s.\n", log_signal(s)); + + int sid = get_bv_sid(GetSize(s)); + int nid = next_nid++; + btorf("%d input %d %s\n", nid, sid); + nid_width[nid] = GetSize(s); + + i += GetSize(s)-1; + continue; + } + else + { + export_cell(bit_cell.at(bit)); + log_assert(bit_nid.count(bit)); + } } } diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index cea0fc56c..ae7968a1b 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -1043,7 +1043,10 @@ class MkVcd: scope = scope[:-1] while uipath[:-1] != scope: - print("$scope module %s $end" % uipath[len(scope)], file=self.f) + scopename = uipath[len(scope)] + if scopename.startswith("$"): + scopename = "\\" + scopename + print("$scope module %s $end" % scopename, file=self.f) scope.append(uipath[len(scope)]) if path in self.clocks and self.clocks[path][1] == "event": -- cgit v1.2.3 From 9398921af1d21b47aa291d240a1f274418adcaf2 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 27 Jun 2019 16:07:14 -0700 Subject: Refactor for one "abc_carry" attribute on module --- backends/aiger/xaiger.cc | 82 +++++++++++++++++++++++------------------------- 1 file changed, 40 insertions(+), 42 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 92df899c2..ae690ec49 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -284,8 +284,6 @@ struct XAigerWriter for (auto user_cell : it.second) toposort.edge(driver_cell, user_cell); - pool abc_carry_modules; - #if 0 toposort.analyze_loops = true; #endif @@ -303,54 +301,54 @@ struct XAigerWriter #endif log_assert(no_loops); + pool seen_boxes; for (auto cell_name : toposort.sorted) { RTLIL::Cell *cell = module->cell(cell_name); + log_assert(cell); + RTLIL::Module* box_module = module->design->module(cell->type); if (!box_module || !box_module->attributes.count("\\abc_box_id")) continue; - if (box_module->attributes.count("\\abc_carry") && !abc_carry_modules.count(box_module)) { - RTLIL::Wire* carry_in = nullptr, *carry_out = nullptr; - auto &ports = box_module->ports; - for (auto it = ports.begin(); it != ports.end(); ) { - RTLIL::Wire* w = box_module->wire(*it); - log_assert(w); - if (w->port_input && w->attributes.count("\\abc_carry_in")) { - if (carry_in) - log_error("More than one port with attribute 'abc_carry_in' found in module '%s'\n", log_id(box_module)); - carry_in = w; - it = ports.erase(it); - continue; - } - if (w->port_output && w->attributes.count("\\abc_carry_out")) { - if (carry_out) - log_error("More than one port with attribute 'abc_carry_out' found in module '%s'\n", log_id(box_module)); - carry_out = w; - it = ports.erase(it); - continue; + if (seen_boxes.insert(cell->type).second) { + auto it = box_module->attributes.find("\\abc_carry"); + if (it != box_module->attributes.end()) { + RTLIL::Wire *carry_in = nullptr, *carry_out = nullptr; + auto carry_in_out = it->second.decode_string(); + auto pos = carry_in_out.find(','); + if (pos == std::string::npos) + log_error("'abc_carry' attribute on module '%s' does not contain ','.\n", log_id(cell->type)); + auto carry_in_name = RTLIL::escape_id(carry_in_out.substr(0, pos)); + carry_in = box_module->wire(carry_in_name); + if (!carry_in || !carry_in->port_input) + log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an input port.\n", log_id(cell->type), carry_in_name.c_str()); + + auto carry_out_name = RTLIL::escape_id(carry_in_out.substr(pos+1)); + carry_out = box_module->wire(carry_out_name); + if (!carry_out || !carry_out->port_output) + log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an output port.\n", log_id(cell->type), carry_out_name.c_str()); + + auto &ports = box_module->ports; + for (auto jt = ports.begin(); jt != ports.end(); ) { + RTLIL::Wire* w = box_module->wire(*jt); + log_assert(w); + if (w == carry_in || w == carry_out) { + jt = ports.erase(jt); + continue; + } + if (w->port_id > carry_in->port_id) + --w->port_id; + if (w->port_id > carry_out->port_id) + --w->port_id; + log_assert(w->port_input || w->port_output); + log_assert(ports[w->port_id-1] == w->name); + ++jt; } - ++it; - } - - if (!carry_in) - log_error("Port with attribute 'abc_carry_in' not found in module '%s'\n", log_id(box_module)); - if (!carry_out) - log_error("Port with attribute 'abc_carry_out' not found in module '%s'\n", log_id(box_module)); - - for (const auto port_name : ports) { - RTLIL::Wire* w = box_module->wire(port_name); - log_assert(w); - if (w->port_id > carry_in->port_id) - --w->port_id; - if (w->port_id > carry_out->port_id) - --w->port_id; - log_assert(w->port_input || w->port_output); - log_assert(ports[w->port_id-1] == w->name); + ports.push_back(carry_in->name); + carry_in->port_id = ports.size(); + ports.push_back(carry_out->name); + carry_out->port_id = ports.size(); } - ports.push_back(carry_in->name); - carry_in->port_id = ports.size(); - ports.push_back(carry_out->name); - carry_out->port_id = ports.size(); } // Fully pad all unused input connections of this box cell with S0 -- cgit v1.2.3 From 36e2eb06bb63714d852b758062471222022930c3 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 28 Jun 2019 09:51:43 -0700 Subject: Fix more potential for undefined behaviour due to container invalidation --- backends/aiger/xaiger.cc | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index ae690ec49..d373ca77e 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -436,14 +436,18 @@ struct XAigerWriter new_wire = module->addWire(wire_name, GetSize(wire)); SigBit new_bit(new_wire, bit.offset); module->connect(new_bit, bit); - if (not_map.count(bit)) - not_map[new_bit] = not_map.at(bit); + if (not_map.count(bit)) { + auto a = not_map.at(bit); + not_map[new_bit] = a; + } else if (and_map.count(bit)) { - //and_map[new_bit] = and_map.at(bit); // Breaks gcc-4.8 - and_map.insert(std::make_pair(new_bit, and_map.at(bit))); + auto a = and_map.at(bit); + and_map[new_bit] = a; + } + else if (alias_map.count(bit)) { + auto a = alias_map.at(bit); + alias_map[new_bit] = a; } - else if (alias_map.count(bit)) - alias_map[new_bit] = alias_map.at(bit); else alias_map[new_bit] = bit; output_bits.erase(bit); -- cgit v1.2.3 From 524af2131741ae2c74a810cab3b925d5ce950e6e Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 28 Jun 2019 09:55:07 -0700 Subject: Also fix write_aiger for UB --- backends/aiger/aiger.cc | 52 ++++++++++++++++++++++++------------------------- 1 file changed, 26 insertions(+), 26 deletions(-) (limited to 'backends') diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 2815abda8..7c851bb91 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -70,35 +70,35 @@ struct AigerWriter int bit2aig(SigBit bit) { - if (aig_map.count(bit) == 0) - { - aig_map[bit] = -1; - - if (initstate_bits.count(bit)) { - log_assert(initstate_ff > 0); - aig_map[bit] = initstate_ff; - } else - if (not_map.count(bit)) { - int a = bit2aig(not_map.at(bit)) ^ 1; - aig_map[bit] = a; - } else - if (and_map.count(bit)) { - auto args = and_map.at(bit); - int a0 = bit2aig(args.first); - int a1 = bit2aig(args.second); - aig_map[bit] = mkgate(a0, a1); - } else - if (alias_map.count(bit)) { - int a = bit2aig(alias_map.at(bit)); - aig_map[bit] = a; - } + auto it = aig_map.find(bit); + if (it != aig_map.end()) { + log_assert(it->second >= 0); + return it->second; + } - if (bit == State::Sx || bit == State::Sz) - log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n"); + // NB: Cannot use iterator returned from aig_map.insert() + // since this function is called recursively + + int a = -1; + if (not_map.count(bit)) { + a = bit2aig(not_map.at(bit)) ^ 1; + } else + if (and_map.count(bit)) { + auto args = and_map.at(bit); + int a0 = bit2aig(args.first); + int a1 = bit2aig(args.second); + a = mkgate(a0, a1); + } else + if (alias_map.count(bit)) { + a = bit2aig(alias_map.at(bit)); } - log_assert(aig_map.at(bit) >= 0); - return aig_map.at(bit); + if (bit == State::Sx || bit == State::Sz) + log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n"); + + log_assert(a >= 0); + aig_map[bit] = a; + return a; } AigerWriter(Module *module, bool zinit_mode, bool imode, bool omode, bool bmode) : module(module), zinit_mode(zinit_mode), sigmap(module) -- cgit v1.2.3 From 38d8806bd74b9bb448c7488ec571e197fe2f96d6 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 28 Jun 2019 09:59:47 -0700 Subject: Add generic __builtin_bswap32 function --- backends/aiger/xaiger.cc | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index d373ca77e..eb3d47569 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -25,6 +25,21 @@ #elif defined(__APPLE__) #include #define __builtin_bswap32 OSSwapInt32 +#elif !defined(__GNUC__) +#include +inline uint32_t __builtin_bswap32(uint32_t x) +{ + // https://stackoverflow.com/a/27796212 + register uint32_t value = number_to_be_reversed; + uint8_t lolo = (value >> 0) & 0xFF; + uint8_t lohi = (value >> 8) & 0xFF; + uint8_t hilo = (value >> 16) & 0xFF; + uint8_t hihi = (value >> 24) & 0xFF; + return (hihi << 24) + | (hilo << 16) + | (lohi << 8) + | (lolo << 0); +} #endif #include "kernel/yosys.h" -- cgit v1.2.3