Skip to content

Commit

Permalink
read_aiger: Fix incorrect read of binary Aiger without outputs
Browse files Browse the repository at this point in the history
  • Loading branch information
georgerennie committed Apr 29, 2024
1 parent 34d9a74 commit 8e20c64
Showing 1 changed file with 4 additions and 6 deletions.
10 changes: 4 additions & 6 deletions frontends/aiger/aigerparse.cc
Original file line number Diff line number Diff line change
Expand Up @@ -590,27 +590,26 @@ 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));
wire->port_output = true;
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)
Expand Down Expand Up @@ -715,27 +714,26 @@ 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));
wire->port_output = true;
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)
Expand Down

0 comments on commit 8e20c64

Please sign in to comment.