riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

read_aiger: Fix incorrect read of binary Aiger without outputs 

* Also makes all ascii parsing finish reading lines and adds a small
  test
This commit is contained in:
George Rennie 2024-04-26 19:16:01 +01:00
parent 34d9a7451e
commit 4e6deb53b6
3 changed files with 18 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
frontends/aiger/aigerparse.cc
View File

@ -590,6 +590,7 @@ void AigerReader::parse_aiger_ascii()
for (unsigned i = 0; i < O; ++i, ++line_count) { for (unsigned i = 0; i < O; ++i, ++line_count) {
if (!(f >> l1)) if (!(f >> l1))
log_error("Line %u cannot be interpreted as an output!\n", line_count); 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); log_debug2("%d is an output\n", l1);
RTLIL::Wire *wire = module->addWire(stringf("$o%0*d", digits, i)); 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)); module->connect(wire, createWireIfNotExists(module, l1));
outputs.push_back(wire); outputs.push_back(wire);
} }
//std::getline(f, line); // Ignore up to start of next line
// Parse bad properties // Parse bad properties
for (unsigned i = 0; i < B; ++i, ++line_count) { for (unsigned i = 0; i < B; ++i, ++line_count) {
if (!(f >> l1)) if (!(f >> l1))
log_error("Line %u cannot be interpreted as a bad state property!\n", line_count); 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); log_debug2("%d is a bad state property\n", l1);
RTLIL::Wire *wire = createWireIfNotExists(module, l1); RTLIL::Wire *wire = createWireIfNotExists(module, l1);
wire->port_output = true; wire->port_output = true;
bad_properties.push_back(wire); bad_properties.push_back(wire);
} }
//if (B > 0)
// std::getline(f, line); // Ignore up to start of next line
// TODO: Parse invariant constraints // TODO: Parse invariant constraints
for (unsigned i = 0; i < C; ++i, ++line_count) 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) { for (unsigned i = 0; i < A; ++i) {
if (!(f >> l1 >> l2 >> l3)) if (!(f >> l1 >> l2 >> l3))
log_error("Line %u cannot be interpreted as an AND!\n", line_count); 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_debug2("%d %d %d is an AND\n", l1, l2, l3);
log_assert(!(l1 & 1)); log_assert(!(l1 & 1));
@ -636,7 +636,6 @@ void AigerReader::parse_aiger_ascii()
RTLIL::Wire *i2_wire = createWireIfNotExists(module, l3); RTLIL::Wire *i2_wire = createWireIfNotExists(module, l3);
module->addAndGate("$and" + o_wire->name.str(), i1_wire, i2_wire, o_wire); 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) 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) { for (unsigned i = 0; i < O; ++i, ++line_count) {
if (!(f >> l1)) if (!(f >> l1))
log_error("Line %u cannot be interpreted as an output!\n", line_count); 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); log_debug2("%d is an output\n", l1);
RTLIL::Wire *wire = module->addWire(stringf("$o%0*d", digits, i)); 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)); module->connect(wire, createWireIfNotExists(module, l1));
outputs.push_back(wire); outputs.push_back(wire);
} }
std::getline(f, line); // Ignore up to start of next line
// Parse bad properties // Parse bad properties
for (unsigned i = 0; i < B; ++i, ++line_count) { for (unsigned i = 0; i < B; ++i, ++line_count) {
if (!(f >> l1)) if (!(f >> l1))
log_error("Line %u cannot be interpreted as a bad state property!\n", line_count); 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); log_debug2("%d is a bad state property\n", l1);
RTLIL::Wire *wire = createWireIfNotExists(module, l1); RTLIL::Wire *wire = createWireIfNotExists(module, l1);
wire->port_output = true; wire->port_output = true;
bad_properties.push_back(wire); bad_properties.push_back(wire);
} }
if (B > 0)
std::getline(f, line); // Ignore up to start of next line
// TODO: Parse invariant constraints // TODO: Parse invariant constraints
for (unsigned i = 0; i < C; ++i, ++line_count) for (unsigned i = 0; i < C; ++i, ++line_count)

8
tests/aiger/and_to_bad_out.aag Normal file
View File

@ -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

5
tests/aiger/and_to_bad_out.aig Normal file
View File

@ -0,0 +1,5 @@
aig 3 2 0 0 1 1
6
i0 pi0
i1 pi1
b0 b0