From 738af17a26587f6f9438bfa2452e65a5911e58e8 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 7 Jan 2020 11:21:45 -0800 Subject: [PATCH 1/6] read_aiger: default -clk_name to be empty --- frontends/aiger/aigerparse.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index f030933ec..d7367479b 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -1018,7 +1018,7 @@ struct AigerFrontend : public Frontend { { log_header(design, "Executing AIGER frontend.\n"); - RTLIL::IdString clk_name = "\\clk"; + RTLIL::IdString clk_name; RTLIL::IdString module_name; std::string map_filename; bool wideports = false; From baba33fbd391d31187695a8d0d9937249a472b2e Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 7 Jan 2020 11:22:48 -0800 Subject: [PATCH 2/6] read_aiger: cope with latches and POs with same name --- frontends/aiger/aigerparse.cc | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index d7367479b..04530e562 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -271,14 +271,23 @@ end_of_header: if ((c == 'i' && l1 > inputs.size()) || (c == 'l' && l1 > latches.size()) || (c == 'o' && l1 > outputs.size())) log_error("Line %u has invalid symbol position!\n", line_count); + RTLIL::IdString escaped_s = stringf("\\%s", s.c_str()); RTLIL::Wire* wire; if (c == 'i') wire = inputs[l1]; else if (c == 'l') wire = latches[l1]; - else if (c == 'o') wire = outputs[l1]; + else if (c == 'o') { + wire = module->wire(escaped_s); + if (wire) { + // Could have been renamed by a latch + module->swap_names(wire, outputs[l1]); + goto next; + } + wire = outputs[l1]; + } else if (c == 'b') wire = bad_properties[l1]; else log_abort(); - module->rename(wire, stringf("\\%s", s.c_str())); + module->rename(wire, escaped_s); } else if (c == 'j' || c == 'f') { // TODO @@ -293,6 +302,7 @@ end_of_header: } else log_error("Line %u: cannot interpret first character '%c'!\n", line_count, c); +next: std::getline(f, line); // Ignore up to start of next line } From b94cf0c1266f6f3daea809323f0bba0dc5d69e1a Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 7 Jan 2020 11:43:28 -0800 Subject: [PATCH 3/6] read_aiger: connect identical signals together --- frontends/aiger/aigerparse.cc | 1 + 1 file changed, 1 insertion(+) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 04530e562..f7b9146ce 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -280,6 +280,7 @@ end_of_header: if (wire) { // Could have been renamed by a latch module->swap_names(wire, outputs[l1]); + module->connect(outputs[l1], wire); goto next; } wire = outputs[l1]; From 7c878bf39741ca8889425932063918d837b8ac9b Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 7 Jan 2020 11:44:03 -0800 Subject: [PATCH 4/6] tests/aiger: write Yosys output --- tests/aiger/run-test.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh index deaf48a3d..8e932b091 100755 --- a/tests/aiger/run-test.sh +++ b/tests/aiger/run-test.sh @@ -33,7 +33,7 @@ design -import gold -as gold design -import gate -as gate miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -verify -prove-asserts -show-ports -seq 16 miter -" +" -l ${aag}.log done for aig in *.aig; do @@ -50,5 +50,5 @@ design -import gold -as gold design -import gate -as gate miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -verify -prove-asserts -show-ports -seq 16 miter -" +" -l ${aig}.log done From 0d3f10d3cc55e83ae6a39881227feb843769d6b1 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 7 Jan 2020 11:44:20 -0800 Subject: [PATCH 5/6] Add testcases --- tests/aiger/symbols.aag | 9 +++++++++ tests/aiger/symbols.aig | 8 ++++++++ 2 files changed, 17 insertions(+) create mode 100644 tests/aiger/symbols.aag create mode 100644 tests/aiger/symbols.aig diff --git a/tests/aiger/symbols.aag b/tests/aiger/symbols.aag new file mode 100644 index 000000000..93f8989f2 --- /dev/null +++ b/tests/aiger/symbols.aag @@ -0,0 +1,9 @@ +aag 2 1 1 1 0 +2 +4 2 1 +4 +i0 d +l0 q +o0 q +c +Generated by Yosys 0.9+932 (git sha1 baba33fb, clang 9.0.0-2 -fPIC -Os) diff --git a/tests/aiger/symbols.aig b/tests/aiger/symbols.aig new file mode 100644 index 000000000..a7922ab46 --- /dev/null +++ b/tests/aiger/symbols.aig @@ -0,0 +1,8 @@ +aig 2 1 1 1 0 +2 1 +4 +i0 d +l0 q +o0 q +c +Generated by Yosys 0.9+932 (git sha1 baba33fb, clang 9.0.0-2 -fPIC -Os) From 2ac36031d4da8d2e99d89f16cb69871c9e3c59aa Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 7 Jan 2020 13:30:31 -0800 Subject: [PATCH 6/6] read_aiger: consistency between ascii and binary; also name latches --- frontends/aiger/aigerparse.cc | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index f7b9146ce..8a114b18c 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -507,13 +507,15 @@ void AigerReader::parse_aiger_ascii() unsigned l1, l2, l3; // Parse inputs + int digits = ceil(log10(I)); for (unsigned i = 1; i <= I; ++i, ++line_count) { if (!(f >> l1)) log_error("Line %u cannot be interpreted as an input!\n", line_count); log_debug2("%d is an input\n", l1); log_assert(!(l1 & 1)); // Inputs can't be inverted - RTLIL::Wire *wire = createWireIfNotExists(module, l1); + RTLIL::Wire *wire = module->addWire(stringf("$i%0*d", digits, l1 >> 1)); wire->port_input = true; + module->connect(createWireIfNotExists(module, l1), wire); inputs.push_back(wire); } @@ -527,12 +529,14 @@ void AigerReader::parse_aiger_ascii() clk_wire->port_input = true; clk_wire->port_output = false; } + digits = ceil(log10(L)); for (unsigned i = 0; i < L; ++i, ++line_count) { if (!(f >> l1 >> l2)) log_error("Line %u cannot be interpreted as a latch!\n", line_count); log_debug2("%d %d is a latch\n", l1, l2); log_assert(!(l1 & 1)); - RTLIL::Wire *q_wire = createWireIfNotExists(module, l1); + RTLIL::Wire *q_wire = module->addWire(stringf("$l%0*d", digits, l1 >> 1)); + module->connect(createWireIfNotExists(module, l1), q_wire); RTLIL::Wire *d_wire = createWireIfNotExists(module, l2); if (clk_wire) @@ -655,12 +659,14 @@ void AigerReader::parse_aiger_binary() clk_wire->port_input = true; clk_wire->port_output = false; } + digits = ceil(log10(L)); l1 = (I+1) * 2; for (unsigned i = 0; i < L; ++i, ++line_count, l1 += 2) { if (!(f >> l2)) log_error("Line %u cannot be interpreted as a latch!\n", line_count); log_debug("%d %d is a latch\n", l1, l2); - RTLIL::Wire *q_wire = createWireIfNotExists(module, l1); + RTLIL::Wire *q_wire = module->addWire(stringf("$l%0*d", digits, l1 >> 1)); + module->connect(createWireIfNotExists(module, l1), q_wire); RTLIL::Wire *d_wire = createWireIfNotExists(module, l2); if (clk_wire)