mirror of https://github.com/YosysHQ/yosys.git
Merge pull request #2013 from YosysHQ/eddie/aiger_fixes
aiger: fixes for ports that have start_offset != 0
This commit is contained in:
commit
7360155459
|
@ -629,30 +629,30 @@ struct AigerWriter
|
||||||
int a = aig_map.at(sig[i]);
|
int a = aig_map.at(sig[i]);
|
||||||
|
|
||||||
if (verbose_map)
|
if (verbose_map)
|
||||||
wire_lines[a] += stringf("wire %d %d %s\n", a, i, log_id(wire));
|
wire_lines[a] += stringf("wire %d %d %s\n", a, wire->start_offset+i, log_id(wire));
|
||||||
|
|
||||||
if (wire->port_input) {
|
if (wire->port_input) {
|
||||||
log_assert((a & 1) == 0);
|
log_assert((a & 1) == 0);
|
||||||
input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, i, log_id(wire));
|
input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, wire->start_offset+i, log_id(wire));
|
||||||
}
|
}
|
||||||
|
|
||||||
if (wire->port_output) {
|
if (wire->port_output) {
|
||||||
int o = ordered_outputs.at(sig[i]);
|
int o = ordered_outputs.at(sig[i]);
|
||||||
output_lines[o] += stringf("output %d %d %s\n", o, i, log_id(wire));
|
output_lines[o] += stringf("output %d %d %s\n", o, wire->start_offset+i, log_id(wire));
|
||||||
}
|
}
|
||||||
|
|
||||||
if (init_inputs.count(sig[i])) {
|
if (init_inputs.count(sig[i])) {
|
||||||
int a = init_inputs.at(sig[i]);
|
int a = init_inputs.at(sig[i]);
|
||||||
log_assert((a & 1) == 0);
|
log_assert((a & 1) == 0);
|
||||||
init_lines[a] += stringf("init %d %d %s\n", (a >> 1)-1, i, log_id(wire));
|
init_lines[a] += stringf("init %d %d %s\n", (a >> 1)-1, wire->start_offset+i, log_id(wire));
|
||||||
}
|
}
|
||||||
|
|
||||||
if (ordered_latches.count(sig[i])) {
|
if (ordered_latches.count(sig[i])) {
|
||||||
int l = ordered_latches.at(sig[i]);
|
int l = ordered_latches.at(sig[i]);
|
||||||
if (zinit_mode && (aig_latchinit.at(l) == 1))
|
if (zinit_mode && (aig_latchinit.at(l) == 1))
|
||||||
latch_lines[l] += stringf("invlatch %d %d %s\n", l, i, log_id(wire));
|
latch_lines[l] += stringf("invlatch %d %d %s\n", l, wire->start_offset+i, log_id(wire));
|
||||||
else
|
else
|
||||||
latch_lines[l] += stringf("latch %d %d %s\n", l, i, log_id(wire));
|
latch_lines[l] += stringf("latch %d %d %s\n", l, wire->start_offset+i, log_id(wire));
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -725,13 +725,12 @@ struct XAigerWriter
|
||||||
if (input_bits.count(b)) {
|
if (input_bits.count(b)) {
|
||||||
int a = aig_map.at(b);
|
int a = aig_map.at(b);
|
||||||
log_assert((a & 1) == 0);
|
log_assert((a & 1) == 0);
|
||||||
input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, i, log_id(wire));
|
input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, wire->start_offset+i, log_id(wire));
|
||||||
}
|
}
|
||||||
|
|
||||||
if (output_bits.count(b)) {
|
if (output_bits.count(b)) {
|
||||||
int o = ordered_outputs.at(b);
|
int o = ordered_outputs.at(b);
|
||||||
int init = 2;
|
output_lines[o] += stringf("output %d %d %s\n", o - GetSize(co_bits), wire->start_offset+i, log_id(wire));
|
||||||
output_lines[o] += stringf("output %d %d %s %d\n", o - GetSize(co_bits), i, log_id(wire), init);
|
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -784,7 +784,7 @@ void AigerReader::post_process()
|
||||||
ff->attributes[ID::abc9_mergeability] = mergeability[i];
|
ff->attributes[ID::abc9_mergeability] = mergeability[i];
|
||||||
}
|
}
|
||||||
|
|
||||||
dict<RTLIL::IdString, int> wideports_cache;
|
dict<RTLIL::IdString, std::pair<int,int>> wideports_cache;
|
||||||
|
|
||||||
if (!map_filename.empty()) {
|
if (!map_filename.empty()) {
|
||||||
std::ifstream mf(map_filename);
|
std::ifstream mf(map_filename);
|
||||||
|
@ -799,11 +799,12 @@ void AigerReader::post_process()
|
||||||
log_assert(wire->port_input);
|
log_assert(wire->port_input);
|
||||||
log_debug("Renaming input %s", log_id(wire));
|
log_debug("Renaming input %s", log_id(wire));
|
||||||
|
|
||||||
|
RTLIL::Wire *existing = nullptr;
|
||||||
if (index == 0) {
|
if (index == 0) {
|
||||||
// Cope with the fact that a CI might be identical
|
// Cope with the fact that a CI might be identical
|
||||||
// to a PI (necessary due to ABC); in those cases
|
// to a PI (necessary due to ABC); in those cases
|
||||||
// simply connect the latter to the former
|
// simply connect the latter to the former
|
||||||
RTLIL::Wire* existing = module->wire(escaped_s);
|
existing = module->wire(escaped_s);
|
||||||
if (!existing)
|
if (!existing)
|
||||||
module->rename(wire, escaped_s);
|
module->rename(wire, escaped_s);
|
||||||
else {
|
else {
|
||||||
|
@ -812,20 +813,29 @@ void AigerReader::post_process()
|
||||||
}
|
}
|
||||||
log_debug(" -> %s\n", log_id(escaped_s));
|
log_debug(" -> %s\n", log_id(escaped_s));
|
||||||
}
|
}
|
||||||
else if (index > 0) {
|
else {
|
||||||
std::string indexed_name = stringf("%s[%d]", escaped_s.c_str(), index);
|
RTLIL::IdString indexed_name = stringf("%s[%d]", escaped_s.c_str(), index);
|
||||||
RTLIL::Wire* existing = module->wire(indexed_name);
|
existing = module->wire(indexed_name);
|
||||||
if (!existing) {
|
if (!existing)
|
||||||
module->rename(wire, indexed_name);
|
module->rename(wire, indexed_name);
|
||||||
if (wideports)
|
|
||||||
wideports_cache[escaped_s] = std::max(wideports_cache[escaped_s], index);
|
|
||||||
}
|
|
||||||
else {
|
else {
|
||||||
module->connect(wire, existing);
|
module->connect(wire, existing);
|
||||||
wire->port_input = false;
|
wire->port_input = false;
|
||||||
}
|
}
|
||||||
log_debug(" -> %s\n", log_id(indexed_name));
|
log_debug(" -> %s\n", log_id(indexed_name));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
if (wideports && !existing) {
|
||||||
|
auto r = wideports_cache.insert(escaped_s);
|
||||||
|
if (r.second) {
|
||||||
|
r.first->second.first = index;
|
||||||
|
r.first->second.second = index;
|
||||||
|
}
|
||||||
|
else {
|
||||||
|
r.first->second.first = std::min(r.first->second.first, index);
|
||||||
|
r.first->second.second = std::max(r.first->second.second, index);
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
else if (type == "output") {
|
else if (type == "output") {
|
||||||
log_assert(static_cast<unsigned>(variable + co_count) < outputs.size());
|
log_assert(static_cast<unsigned>(variable + co_count) < outputs.size());
|
||||||
|
@ -834,14 +844,14 @@ void AigerReader::post_process()
|
||||||
log_assert(wire->port_output);
|
log_assert(wire->port_output);
|
||||||
log_debug("Renaming output %s", log_id(wire));
|
log_debug("Renaming output %s", log_id(wire));
|
||||||
|
|
||||||
|
RTLIL::Wire *existing;
|
||||||
if (index == 0) {
|
if (index == 0) {
|
||||||
// Cope with the fact that a CO might be identical
|
// Cope with the fact that a CO might be identical
|
||||||
// to a PO (necessary due to ABC); in those cases
|
// to a PO (necessary due to ABC); in those cases
|
||||||
// simply connect the latter to the former
|
// simply connect the latter to the former
|
||||||
RTLIL::Wire* existing = module->wire(escaped_s);
|
existing = module->wire(escaped_s);
|
||||||
if (!existing) {
|
if (!existing)
|
||||||
module->rename(wire, escaped_s);
|
module->rename(wire, escaped_s);
|
||||||
}
|
|
||||||
else {
|
else {
|
||||||
wire->port_output = false;
|
wire->port_output = false;
|
||||||
existing->port_output = true;
|
existing->port_output = true;
|
||||||
|
@ -850,14 +860,11 @@ void AigerReader::post_process()
|
||||||
}
|
}
|
||||||
log_debug(" -> %s\n", log_id(escaped_s));
|
log_debug(" -> %s\n", log_id(escaped_s));
|
||||||
}
|
}
|
||||||
else if (index > 0) {
|
else {
|
||||||
std::string indexed_name = stringf("%s[%d]", escaped_s.c_str(), index);
|
RTLIL::IdString indexed_name = stringf("%s[%d]", escaped_s.c_str(), index);
|
||||||
RTLIL::Wire* existing = module->wire(indexed_name);
|
existing = module->wire(indexed_name);
|
||||||
if (!existing) {
|
if (!existing)
|
||||||
module->rename(wire, indexed_name);
|
module->rename(wire, indexed_name);
|
||||||
if (wideports)
|
|
||||||
wideports_cache[escaped_s] = std::max(wideports_cache[escaped_s], index);
|
|
||||||
}
|
|
||||||
else {
|
else {
|
||||||
wire->port_output = false;
|
wire->port_output = false;
|
||||||
existing->port_output = true;
|
existing->port_output = true;
|
||||||
|
@ -865,10 +872,18 @@ void AigerReader::post_process()
|
||||||
}
|
}
|
||||||
log_debug(" -> %s\n", log_id(indexed_name));
|
log_debug(" -> %s\n", log_id(indexed_name));
|
||||||
}
|
}
|
||||||
int init;
|
|
||||||
mf >> init;
|
if (wideports && !existing) {
|
||||||
if (init < 2)
|
auto r = wideports_cache.insert(escaped_s);
|
||||||
wire->attributes[ID::init] = init;
|
if (r.second) {
|
||||||
|
r.first->second.first = index;
|
||||||
|
r.first->second.second = index;
|
||||||
|
}
|
||||||
|
else {
|
||||||
|
r.first->second.first = std::min(r.first->second.first, index);
|
||||||
|
r.first->second.second = std::max(r.first->second.second, index);
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
else if (type == "box") {
|
else if (type == "box") {
|
||||||
RTLIL::Cell* cell = module->cell(stringf("$box%d", variable));
|
RTLIL::Cell* cell = module->cell(stringf("$box%d", variable));
|
||||||
|
@ -882,7 +897,8 @@ void AigerReader::post_process()
|
||||||
|
|
||||||
for (auto &wp : wideports_cache) {
|
for (auto &wp : wideports_cache) {
|
||||||
auto name = wp.first;
|
auto name = wp.first;
|
||||||
int width = wp.second + 1;
|
int min = wp.second.first;
|
||||||
|
int max = wp.second.second;
|
||||||
|
|
||||||
RTLIL::Wire *wire = module->wire(name);
|
RTLIL::Wire *wire = module->wire(name);
|
||||||
if (wire)
|
if (wire)
|
||||||
|
@ -891,7 +907,7 @@ void AigerReader::post_process()
|
||||||
// Do not make ports with a mix of input/output into
|
// Do not make ports with a mix of input/output into
|
||||||
// wide ports
|
// wide ports
|
||||||
bool port_input = false, port_output = false;
|
bool port_input = false, port_output = false;
|
||||||
for (int i = 0; i < width; i++) {
|
for (int i = min; i <= max; i++) {
|
||||||
RTLIL::IdString other_name = name.str() + stringf("[%d]", i);
|
RTLIL::IdString other_name = name.str() + stringf("[%d]", i);
|
||||||
RTLIL::Wire *other_wire = module->wire(other_name);
|
RTLIL::Wire *other_wire = module->wire(other_name);
|
||||||
if (other_wire) {
|
if (other_wire) {
|
||||||
|
@ -900,20 +916,21 @@ void AigerReader::post_process()
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
wire = module->addWire(name, width);
|
wire = module->addWire(name, max-min+1);
|
||||||
|
wire->start_offset = min;
|
||||||
wire->port_input = port_input;
|
wire->port_input = port_input;
|
||||||
wire->port_output = port_output;
|
wire->port_output = port_output;
|
||||||
|
|
||||||
for (int i = 0; i < width; i++) {
|
for (int i = min; i <= max; i++) {
|
||||||
RTLIL::IdString other_name = name.str() + stringf("[%d]", i);
|
RTLIL::IdString other_name = stringf("%s[%d]", name.c_str(), i);
|
||||||
RTLIL::Wire *other_wire = module->wire(other_name);
|
RTLIL::Wire *other_wire = module->wire(other_name);
|
||||||
if (other_wire) {
|
if (other_wire) {
|
||||||
other_wire->port_input = false;
|
other_wire->port_input = false;
|
||||||
other_wire->port_output = false;
|
other_wire->port_output = false;
|
||||||
if (wire->port_input)
|
if (wire->port_input)
|
||||||
module->connect(other_wire, SigSpec(wire, i));
|
module->connect(other_wire, SigSpec(wire, i-min));
|
||||||
else
|
else
|
||||||
module->connect(SigSpec(wire, i), other_wire);
|
module->connect(SigSpec(wire, i-min), other_wire);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -741,8 +741,10 @@ void reintegrate(RTLIL::Module *module)
|
||||||
if (mapped_mod == NULL)
|
if (mapped_mod == NULL)
|
||||||
log_error("ABC output file does not contain a module `%s$abc'.\n", log_id(module));
|
log_error("ABC output file does not contain a module `%s$abc'.\n", log_id(module));
|
||||||
|
|
||||||
for (auto w : mapped_mod->wires())
|
for (auto w : mapped_mod->wires()) {
|
||||||
module->addWire(remap_name(w->name), GetSize(w));
|
auto nw = module->addWire(remap_name(w->name), GetSize(w));
|
||||||
|
nw->start_offset = w->start_offset;
|
||||||
|
}
|
||||||
|
|
||||||
dict<IdString,std::vector<IdString>> box_ports;
|
dict<IdString,std::vector<IdString>> box_ports;
|
||||||
|
|
||||||
|
@ -989,7 +991,7 @@ void reintegrate(RTLIL::Module *module)
|
||||||
wire->attributes.erase(ID::abc9_scc);
|
wire->attributes.erase(ID::abc9_scc);
|
||||||
|
|
||||||
RTLIL::Wire *remap_wire = module->wire(remap_name(port));
|
RTLIL::Wire *remap_wire = module->wire(remap_name(port));
|
||||||
RTLIL::SigSpec signal(wire, 0, GetSize(remap_wire));
|
RTLIL::SigSpec signal(wire, remap_wire->start_offset-wire->start_offset, GetSize(remap_wire));
|
||||||
log_assert(GetSize(signal) >= GetSize(remap_wire));
|
log_assert(GetSize(signal) >= GetSize(remap_wire));
|
||||||
|
|
||||||
RTLIL::SigSig conn;
|
RTLIL::SigSig conn;
|
||||||
|
|
|
@ -0,0 +1,36 @@
|
||||||
|
read_verilog <<EOT
|
||||||
|
module top(input [31:-32] a, input [-65:-128] b, output [128:65] c);
|
||||||
|
assign c = a & b;
|
||||||
|
endmodule
|
||||||
|
EOT
|
||||||
|
select -assert-count 1 i:a
|
||||||
|
select -assert-count 1 i:b
|
||||||
|
select -assert-count 1 o:c
|
||||||
|
select -assert-count 3 x:* s:64 %i
|
||||||
|
design -save read
|
||||||
|
|
||||||
|
!rm -rf neg.out
|
||||||
|
!mkdir neg.out
|
||||||
|
simplemap
|
||||||
|
write_aiger -map neg.out/neg.map neg.out/neg.aig
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
read_aiger -wideports -map neg.out/neg.map neg.out/neg.aig
|
||||||
|
select -assert-count 1 i:a
|
||||||
|
select -assert-count 1 i:b
|
||||||
|
select -assert-count 1 o:c
|
||||||
|
select -assert-count 3 x:* s:64 %i
|
||||||
|
|
||||||
|
|
||||||
|
design -load read
|
||||||
|
!rm -rf neg.out
|
||||||
|
!mkdir neg.out
|
||||||
|
simplemap
|
||||||
|
write_xaiger -map neg.out/neg.map neg.out/neg.aig
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
read_aiger -wideports -map neg.out/neg.map neg.out/neg.aig
|
||||||
|
select -assert-count 1 i:a
|
||||||
|
select -assert-count 1 i:b
|
||||||
|
select -assert-count 1 o:c
|
||||||
|
select -assert-count 3 x:* s:64 %i
|
|
@ -52,3 +52,8 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||||
sat -verify -prove-asserts -show-ports -seq 16 miter
|
sat -verify -prove-asserts -show-ports -seq 16 miter
|
||||||
" -l ${aig}.log
|
" -l ${aig}.log
|
||||||
done
|
done
|
||||||
|
|
||||||
|
for y in *.ys; do
|
||||||
|
echo "Running $y."
|
||||||
|
../../yosys $y -ql ${y%.*}.log
|
||||||
|
done
|
||||||
|
|
Loading…
Reference in New Issue