From 4e6deb53b64d4acd2046d2826ede02c5cd35d22f Mon Sep 17 00:00:00 2001 From: George Rennie Date: Fri, 26 Apr 2024 19:16:01 +0100 Subject: [PATCH 1/2] read_aiger: Fix incorrect read of binary Aiger without outputs * Also makes all ascii parsing finish reading lines and adds a small test --- frontends/aiger/aigerparse.cc | 12 +++++------- tests/aiger/and_to_bad_out.aag | 8 ++++++++ tests/aiger/and_to_bad_out.aig | 5 +++++ 3 files changed, 18 insertions(+), 7 deletions(-) create mode 100644 tests/aiger/and_to_bad_out.aag create mode 100644 tests/aiger/and_to_bad_out.aig diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index cb19b8413a5..0178514e1cd 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -590,6 +590,7 @@ void AigerReader::parse_aiger_ascii() for (unsigned i = 0; i < O; ++i, ++line_count) { if (!(f >> l1)) log_error("Line %u cannot be interpreted as an output!\n", line_count); + std::getline(f, line); // Ignore up to start of next line log_debug2("%d is an output\n", l1); RTLIL::Wire *wire = module->addWire(stringf("$o%0*d", digits, i)); @@ -597,20 +598,18 @@ void AigerReader::parse_aiger_ascii() module->connect(wire, createWireIfNotExists(module, l1)); outputs.push_back(wire); } - //std::getline(f, line); // Ignore up to start of next line // Parse bad properties for (unsigned i = 0; i < B; ++i, ++line_count) { if (!(f >> l1)) log_error("Line %u cannot be interpreted as a bad state property!\n", line_count); + std::getline(f, line); // Ignore up to start of next line log_debug2("%d is a bad state property\n", l1); RTLIL::Wire *wire = createWireIfNotExists(module, l1); wire->port_output = true; bad_properties.push_back(wire); } - //if (B > 0) - // std::getline(f, line); // Ignore up to start of next line // TODO: Parse invariant constraints for (unsigned i = 0; i < C; ++i, ++line_count) @@ -628,6 +627,7 @@ void AigerReader::parse_aiger_ascii() for (unsigned i = 0; i < A; ++i) { if (!(f >> l1 >> l2 >> l3)) log_error("Line %u cannot be interpreted as an AND!\n", line_count); + std::getline(f, line); // Ignore up to start of next line log_debug2("%d %d %d is an AND\n", l1, l2, l3); log_assert(!(l1 & 1)); @@ -636,7 +636,6 @@ void AigerReader::parse_aiger_ascii() RTLIL::Wire *i2_wire = createWireIfNotExists(module, l3); module->addAndGate("$and" + o_wire->name.str(), i1_wire, i2_wire, o_wire); } - std::getline(f, line); // Ignore up to start of next line } static unsigned parse_next_delta_literal(std::istream &f, unsigned ref) @@ -715,6 +714,7 @@ void AigerReader::parse_aiger_binary() for (unsigned i = 0; i < O; ++i, ++line_count) { if (!(f >> l1)) log_error("Line %u cannot be interpreted as an output!\n", line_count); + std::getline(f, line); // Ignore up to start of next line log_debug2("%d is an output\n", l1); RTLIL::Wire *wire = module->addWire(stringf("$o%0*d", digits, i)); @@ -722,20 +722,18 @@ void AigerReader::parse_aiger_binary() module->connect(wire, createWireIfNotExists(module, l1)); outputs.push_back(wire); } - std::getline(f, line); // Ignore up to start of next line // Parse bad properties for (unsigned i = 0; i < B; ++i, ++line_count) { if (!(f >> l1)) log_error("Line %u cannot be interpreted as a bad state property!\n", line_count); + std::getline(f, line); // Ignore up to start of next line log_debug2("%d is a bad state property\n", l1); RTLIL::Wire *wire = createWireIfNotExists(module, l1); wire->port_output = true; bad_properties.push_back(wire); } - if (B > 0) - std::getline(f, line); // Ignore up to start of next line // TODO: Parse invariant constraints for (unsigned i = 0; i < C; ++i, ++line_count) diff --git a/tests/aiger/and_to_bad_out.aag b/tests/aiger/and_to_bad_out.aag new file mode 100644 index 00000000000..96f1e7cad12 --- /dev/null +++ b/tests/aiger/and_to_bad_out.aag @@ -0,0 +1,8 @@ +aag 3 2 0 0 1 1 0 0 0 +2 +4 +6 +6 2 4 +i0 pi0 +i1 pi1 +b0 b0 diff --git a/tests/aiger/and_to_bad_out.aig b/tests/aiger/and_to_bad_out.aig new file mode 100644 index 00000000000..3be65ae895b --- /dev/null +++ b/tests/aiger/and_to_bad_out.aig @@ -0,0 +1,5 @@ +aig 3 2 0 0 1 1 +6 +i0 pi0 +i1 pi1 +b0 b0 From dd2195543b095cce108dcd9b94fe2f0a80660491 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 30 Apr 2024 00:17:14 +0000 Subject: [PATCH 2/2] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 22fe373a68a..2dbce272dc6 100644 --- a/Makefile +++ b/Makefile @@ -142,7 +142,7 @@ LIBS += -lrt endif endif -YOSYS_VER := 0.40+33 +YOSYS_VER := 0.40+45 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo