mirror of https://github.com/YosysHQ/yosys.git
Fix read_aiger -- create zero driver, fix init width, parse 'b'
This commit is contained in:
parent
abc40924ed
commit
a04521c6b7
|
@ -81,11 +81,26 @@ end_of_header:
|
||||||
else
|
else
|
||||||
log_abort();
|
log_abort();
|
||||||
|
|
||||||
|
RTLIL::Wire* n0 = module->wire("\\n0");
|
||||||
|
if (n0)
|
||||||
|
module->connect(n0, RTLIL::S0);
|
||||||
|
|
||||||
|
for (unsigned i = 0; i < outputs.size(); ++i) {
|
||||||
|
RTLIL::Wire *wire = outputs[i];
|
||||||
|
if (wire->port_input) {
|
||||||
|
RTLIL::Wire *o_wire = module->addWire(wire->name.str() + "_o");
|
||||||
|
o_wire->port_output = true;
|
||||||
|
wire->port_output = false;
|
||||||
|
module->connect(o_wire, wire);
|
||||||
|
outputs[i] = o_wire;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
// Parse footer (symbol table, comments, etc.)
|
// Parse footer (symbol table, comments, etc.)
|
||||||
unsigned l1;
|
unsigned l1;
|
||||||
std::string s;
|
std::string s;
|
||||||
for (int c = f.peek(); c != EOF; c = f.peek(), ++line_count) {
|
for (int c = f.peek(); c != EOF; c = f.peek(), ++line_count) {
|
||||||
if (c == 'i' || c == 'l' || c == 'o') {
|
if (c == 'i' || c == 'l' || c == 'o' || c == 'b') {
|
||||||
f.ignore(1);
|
f.ignore(1);
|
||||||
if (!(f >> l1 >> s))
|
if (!(f >> l1 >> s))
|
||||||
log_error("Line %u cannot be interpreted as a symbol entry!\n", line_count);
|
log_error("Line %u cannot be interpreted as a symbol entry!\n", line_count);
|
||||||
|
@ -97,11 +112,12 @@ end_of_header:
|
||||||
if (c == 'i') wire = inputs[l1];
|
if (c == 'i') wire = inputs[l1];
|
||||||
else if (c == 'l') wire = latches[l1];
|
else if (c == 'l') wire = latches[l1];
|
||||||
else if (c == 'o') wire = outputs[l1];
|
else if (c == 'o') wire = outputs[l1];
|
||||||
|
else if (c == 'b') wire = bad_properties[l1];
|
||||||
else log_abort();
|
else log_abort();
|
||||||
|
|
||||||
module->rename(wire, stringf("\\%s", s.c_str()));
|
module->rename(wire, stringf("\\%s", s.c_str()));
|
||||||
}
|
}
|
||||||
else if (c == 'b' || c == 'j' || c == 'f') {
|
else if (c == 'j' || c == 'f') {
|
||||||
// TODO
|
// TODO
|
||||||
}
|
}
|
||||||
else if (c == 'c') {
|
else if (c == 'c') {
|
||||||
|
@ -153,7 +169,7 @@ void AigerReader::parse_aiger_ascii()
|
||||||
unsigned l1, l2, l3;
|
unsigned l1, l2, l3;
|
||||||
|
|
||||||
// Parse inputs
|
// Parse inputs
|
||||||
for (unsigned i = 0; i < I; ++i, ++line_count) {
|
for (unsigned i = 1; i <= I; ++i, ++line_count) {
|
||||||
if (!(f >> l1))
|
if (!(f >> l1))
|
||||||
log_error("Line %u cannot be interpreted as an input!\n", line_count);
|
log_error("Line %u cannot be interpreted as an input!\n", line_count);
|
||||||
log_debug("%d is an input\n", l1);
|
log_debug("%d is an input\n", l1);
|
||||||
|
@ -187,8 +203,10 @@ void AigerReader::parse_aiger_ascii()
|
||||||
if (!(f >> l3))
|
if (!(f >> l3))
|
||||||
log_error("Line %u cannot be interpreted as a latch!\n", line_count);
|
log_error("Line %u cannot be interpreted as a latch!\n", line_count);
|
||||||
|
|
||||||
if (l3 == 0 || l3 == 1)
|
if (l3 == 0)
|
||||||
q_wire->attributes["\\init"] = RTLIL::Const(l3);
|
q_wire->attributes["\\init"] = RTLIL::S0;
|
||||||
|
else if (l3 == 1)
|
||||||
|
q_wire->attributes["\\init"] = RTLIL::S1;
|
||||||
else if (l3 == l1) {
|
else if (l3 == l1) {
|
||||||
//q_wire->attributes["\\init"] = RTLIL::Const(RTLIL::State::Sx);
|
//q_wire->attributes["\\init"] = RTLIL::Const(RTLIL::State::Sx);
|
||||||
}
|
}
|
||||||
|
@ -197,7 +215,7 @@ void AigerReader::parse_aiger_ascii()
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
// AIGER latches are assumed to be initialized to zero
|
// AIGER latches are assumed to be initialized to zero
|
||||||
q_wire->attributes["\\init"] = RTLIL::Const(0);
|
q_wire->attributes["\\init"] = RTLIL::S0;
|
||||||
}
|
}
|
||||||
latches.push_back(q_wire);
|
latches.push_back(q_wire);
|
||||||
}
|
}
|
||||||
|
@ -214,8 +232,17 @@ void AigerReader::parse_aiger_ascii()
|
||||||
}
|
}
|
||||||
std::getline(f, line); // Ignore up to start of next line
|
std::getline(f, line); // Ignore up to start of next line
|
||||||
|
|
||||||
// TODO: Parse bad state 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))
|
||||||
|
log_error("Line %u cannot be interpreted as a bad state property!\n", line_count);
|
||||||
|
|
||||||
|
log_debug("%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
|
std::getline(f, line); // Ignore up to start of next line
|
||||||
|
|
||||||
// TODO: Parse invariant constraints
|
// TODO: Parse invariant constraints
|
||||||
|
@ -290,8 +317,10 @@ void AigerReader::parse_aiger_binary()
|
||||||
if (!(f >> l3))
|
if (!(f >> l3))
|
||||||
log_error("Line %u cannot be interpreted as a latch!\n", line_count);
|
log_error("Line %u cannot be interpreted as a latch!\n", line_count);
|
||||||
|
|
||||||
if (l3 == 0 || l3 == 1)
|
if (l3 == 0)
|
||||||
q_wire->attributes["\\init"] = RTLIL::Const(l3);
|
q_wire->attributes["\\init"] = RTLIL::S0;
|
||||||
|
else if (l3 == 1)
|
||||||
|
q_wire->attributes["\\init"] = RTLIL::S1;
|
||||||
else if (l3 == l1) {
|
else if (l3 == l1) {
|
||||||
//q_wire->attributes["\\init"] = RTLIL::Const(RTLIL::State::Sx);
|
//q_wire->attributes["\\init"] = RTLIL::Const(RTLIL::State::Sx);
|
||||||
}
|
}
|
||||||
|
@ -300,7 +329,7 @@ void AigerReader::parse_aiger_binary()
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
// AIGER latches are assumed to be initialized to zero
|
// AIGER latches are assumed to be initialized to zero
|
||||||
q_wire->attributes["\\init"] = RTLIL::Const(0);
|
q_wire->attributes["\\init"] = RTLIL::S0;
|
||||||
}
|
}
|
||||||
latches.push_back(q_wire);
|
latches.push_back(q_wire);
|
||||||
}
|
}
|
||||||
|
@ -317,8 +346,17 @@ void AigerReader::parse_aiger_binary()
|
||||||
}
|
}
|
||||||
std::getline(f, line); // Ignore up to start of next line
|
std::getline(f, line); // Ignore up to start of next line
|
||||||
|
|
||||||
// TODO: Parse bad state 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))
|
||||||
|
log_error("Line %u cannot be interpreted as a bad state property!\n", line_count);
|
||||||
|
|
||||||
|
log_debug("%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
|
std::getline(f, line); // Ignore up to start of next line
|
||||||
|
|
||||||
// TODO: Parse invariant constraints
|
// TODO: Parse invariant constraints
|
||||||
|
|
|
@ -39,6 +39,7 @@ struct AigerReader
|
||||||
std::vector<RTLIL::Wire*> inputs;
|
std::vector<RTLIL::Wire*> inputs;
|
||||||
std::vector<RTLIL::Wire*> latches;
|
std::vector<RTLIL::Wire*> latches;
|
||||||
std::vector<RTLIL::Wire*> outputs;
|
std::vector<RTLIL::Wire*> outputs;
|
||||||
|
std::vector<RTLIL::Wire*> bad_properties;
|
||||||
|
|
||||||
AigerReader(RTLIL::Design *design, std::istream &f, RTLIL::IdString module_name, RTLIL::IdString clk_name);
|
AigerReader(RTLIL::Design *design, std::istream &f, RTLIL::IdString module_name, RTLIL::IdString clk_name);
|
||||||
void parse_aiger();
|
void parse_aiger();
|
||||||
|
|
Loading…
Reference in New Issue