aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/aiger/aiger.cc23
-rw-r--r--backends/aiger/xaiger.cc147
-rw-r--r--backends/btor/btor.cc22
-rw-r--r--backends/protobuf/protobuf.cc4
-rw-r--r--backends/smt2/Makefile.inc2
-rw-r--r--backends/smt2/smtbmc.py28
6 files changed, 140 insertions, 86 deletions
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 7c851bb91..3e8b14dee 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -101,7 +101,7 @@ struct AigerWriter
return a;
}
- AigerWriter(Module *module, bool zinit_mode, bool imode, bool omode, bool bmode) : module(module), zinit_mode(zinit_mode), sigmap(module)
+ AigerWriter(Module *module, bool zinit_mode, bool imode, bool omode, bool bmode, bool lmode) : module(module), zinit_mode(zinit_mode), sigmap(module)
{
pool<SigBit> undriven_bits;
pool<SigBit> unused_bits;
@@ -367,6 +367,12 @@ struct AigerWriter
aig_latchin.push_back(a);
}
+ if (lmode && aig_l == 0) {
+ aig_m++, aig_l++;
+ aig_latchinit.push_back(0);
+ aig_latchin.push_back(0);
+ }
+
if (!initstate_bits.empty() || !init_inputs.empty())
aig_latchin.push_back(1);
@@ -704,9 +710,9 @@ struct AigerBackend : public Backend {
log(" -vmap <filename>\n");
log(" like -map, but more verbose\n");
log("\n");
- log(" -I, -O, -B\n");
- log(" If the design contains no input/output/assert then create one\n");
- log(" dummy input/output/bad_state pin to make the tools reading the\n");
+ log(" -I, -O, -B, -L\n");
+ log(" If the design contains no input/output/assert/flip-flop then create one\n");
+ log(" dummy input/output/bad_state-pin or latch to make the tools reading the\n");
log(" AIGER file happy.\n");
log("\n");
}
@@ -720,6 +726,7 @@ struct AigerBackend : public Backend {
bool imode = false;
bool omode = false;
bool bmode = false;
+ bool lmode = false;
std::string map_filename;
log_header(design, "Executing AIGER backend.\n");
@@ -764,16 +771,20 @@ struct AigerBackend : public Backend {
bmode = true;
continue;
}
+ if (args[argidx] == "-L") {
+ lmode = true;
+ continue;
+ }
break;
}
- extra_args(f, filename, args, argidx);
+ extra_args(f, filename, args, argidx, !ascii_mode);
Module *top_module = design->top_module();
if (top_module == nullptr)
log_error("Can't find top module in current design!\n");
- AigerWriter writer(top_module, zinit_mode, imode, omode, bmode);
+ AigerWriter writer(top_module, zinit_mode, imode, omode, bmode, lmode);
writer.write_aiger(*f, ascii_mode, miter_mode, symbols_mode);
if (!map_filename.empty()) {
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index e1b84236d..46890b071 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -83,6 +83,7 @@ struct XAigerWriter
dict<SigBit, pair<SigBit, SigBit>> and_map;
vector<std::tuple<SigBit,RTLIL::Cell*,RTLIL::IdString,int>> ci_bits;
vector<std::tuple<SigBit,RTLIL::Cell*,RTLIL::IdString,int,int>> co_bits;
+ dict<SigBit, float> arrival_times;
vector<pair<int, int>> aig_gates;
vector<int> aig_outputs;
@@ -202,7 +203,7 @@ struct XAigerWriter
// box ordering, but not individual AIG cells
dict<SigBit, pool<IdString>> bit_drivers, bit_users;
TopoSort<IdString, RTLIL::sort_by_id_str> toposort;
- bool abc_box_seen = false;
+ bool abc9_box_seen = false;
for (auto cell : module->selected_cells()) {
if (cell->type == "$_NOT_")
@@ -241,20 +242,21 @@ struct XAigerWriter
log_assert(!holes_mode);
RTLIL::Module* inst_module = module->design->module(cell->type);
- if (inst_module && inst_module->attributes.count("\\abc_box_id")) {
- abc_box_seen = true;
+ if (inst_module && inst_module->attributes.count("\\abc9_box_id")) {
+ abc9_box_seen = true;
if (!holes_mode) {
toposort.node(cell->name);
for (const auto &conn : cell->connections()) {
- if (cell->input(conn.first)) {
+ auto port_wire = inst_module->wire(conn.first);
+ if (port_wire->port_input) {
// Ignore inout for the sake of topographical ordering
- if (cell->output(conn.first)) continue;
+ if (port_wire->port_output) continue;
for (auto bit : sigmap(conn.second))
bit_users[bit].insert(cell->name);
}
- if (cell->output(conn.first))
+ if (port_wire->port_output)
for (auto bit : sigmap(conn.second))
bit_drivers[bit].insert(cell->name);
}
@@ -271,7 +273,7 @@ struct XAigerWriter
log_error("Connection '%s' on cell '%s' (type '%s') not recognised!\n", log_id(c.first), log_id(cell), log_id(cell->type));
if (is_input) {
- for (auto b : c.second.bits()) {
+ for (auto b : c.second) {
Wire *w = b.wire;
if (!w) continue;
if (!w->port_output || !cell_known) {
@@ -287,7 +289,17 @@ struct XAigerWriter
}
}
if (is_output) {
- for (auto b : c.second.bits()) {
+ int arrival = 0;
+ if (port_wire) {
+ auto it = port_wire->attributes.find("\\abc9_arrival");
+ if (it != port_wire->attributes.end()) {
+ if (it->second.flags != 0)
+ log_error("Attribute 'abc9_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(port_wire), log_id(cell->type));
+ arrival = it->second.as_int();
+ }
+ }
+
+ for (auto b : c.second) {
Wire *w = b.wire;
if (!w) continue;
input_bits.insert(b);
@@ -295,6 +307,9 @@ struct XAigerWriter
if (O != b)
alias_map[O] = b;
undriven_bits.erase(O);
+
+ if (arrival)
+ arrival_times[b] = arrival;
}
}
}
@@ -303,7 +318,7 @@ struct XAigerWriter
//log_warning("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
}
- if (abc_box_seen) {
+ if (abc9_box_seen) {
for (auto &it : bit_users)
if (bit_drivers.count(it.first))
for (auto driver_cell : bit_drivers.at(it.first))
@@ -332,9 +347,11 @@ struct XAigerWriter
log_assert(cell);
RTLIL::Module* box_module = module->design->module(cell->type);
- if (!box_module || !box_module->attributes.count("\\abc_box_id"))
+ if (!box_module || !box_module->attributes.count("\\abc9_box_id"))
continue;
+ bool blackbox = box_module->get_blackbox_attribute(true /* ignore_wb */);
+
// Fully pad all unused input connections of this box cell with S0
// Fully pad all undriven output connections of this box cell with anonymous wires
// NB: Assume box_module->ports are sorted alphabetically
@@ -379,7 +396,10 @@ struct XAigerWriter
rhs = it->second;
}
else {
- rhs = module->addWire(NEW_ID, GetSize(w));
+ Wire *wire = module->addWire(NEW_ID, GetSize(w));
+ if (blackbox)
+ wire->set_bool_attribute(ID(abc9_padding));
+ rhs = wire;
cell->setPort(port_name, rhs);
}
@@ -390,12 +410,7 @@ struct XAigerWriter
if (O != b)
alias_map[O] = b;
undriven_bits.erase(O);
-
- auto jt = input_bits.find(b);
- if (jt != input_bits.end()) {
- log_assert(keep_bits.count(O));
- input_bits.erase(b);
- }
+ input_bits.erase(b);
}
}
}
@@ -414,7 +429,7 @@ struct XAigerWriter
// inherit existing inout's drivers
if ((wire->port_input && wire->port_output && !undriven_bits.count(bit))
|| keep_bits.count(bit)) {
- RTLIL::IdString wire_name = wire->name.str() + "$inout.out";
+ RTLIL::IdString wire_name = stringf("$%s$inout.out", wire->name.c_str());
RTLIL::Wire *new_wire = module->wire(wire_name);
if (!new_wire)
new_wire = module->addWire(wire_name, GetSize(wire));
@@ -489,16 +504,16 @@ struct XAigerWriter
aig_outputs.push_back(bit2aig(bit));
}
+ if (output_bits.empty()) {
+ output_bits.insert(State::S0);
+ omode = true;
+ }
+
for (auto bit : output_bits) {
ordered_outputs[bit] = aig_o++;
aig_outputs.push_back(bit2aig(bit));
}
- if (output_bits.empty()) {
- aig_o++;
- aig_outputs.push_back(0);
- omode = true;
- }
}
void write_aiger(std::ostream &f, bool ascii_mode)
@@ -560,26 +575,38 @@ struct XAigerWriter
f << "c";
- if (!box_list.empty()) {
- auto write_buffer = [](std::stringstream &buffer, int i32) {
- int32_t i32_be = to_big_endian(i32);
- buffer.write(reinterpret_cast<const char*>(&i32_be), sizeof(i32_be));
- };
-
- std::stringstream h_buffer;
- auto write_h_buffer = std::bind(write_buffer, std::ref(h_buffer), std::placeholders::_1);
- write_h_buffer(1);
- log_debug("ciNum = %d\n", GetSize(input_bits) + GetSize(ci_bits));
- write_h_buffer(input_bits.size() + ci_bits.size());
- log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(co_bits));
- write_h_buffer(output_bits.size() + co_bits.size());
- log_debug("piNum = %d\n", GetSize(input_bits));
- write_h_buffer(input_bits.size());
- log_debug("poNum = %d\n", GetSize(output_bits));
- write_h_buffer(output_bits.size());
- log_debug("boxNum = %d\n", GetSize(box_list));
- write_h_buffer(box_list.size());
+ log_assert(!output_bits.empty());
+ auto write_buffer = [](std::stringstream &buffer, int i32) {
+ int32_t i32_be = to_big_endian(i32);
+ buffer.write(reinterpret_cast<const char*>(&i32_be), sizeof(i32_be));
+ };
+ std::stringstream h_buffer;
+ auto write_h_buffer = std::bind(write_buffer, std::ref(h_buffer), std::placeholders::_1);
+ write_h_buffer(1);
+ log_debug("ciNum = %d\n", GetSize(input_bits) + GetSize(ci_bits));
+ write_h_buffer(input_bits.size() + ci_bits.size());
+ log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(co_bits));
+ write_h_buffer(output_bits.size() + GetSize(co_bits));
+ log_debug("piNum = %d\n", GetSize(input_bits));
+ write_h_buffer(input_bits.size());
+ log_debug("poNum = %d\n", GetSize(output_bits));
+ write_h_buffer(output_bits.size());
+ log_debug("boxNum = %d\n", GetSize(box_list));
+ write_h_buffer(box_list.size());
+
+ auto write_buffer_float = [](std::stringstream &buffer, float f32) {
+ buffer.write(reinterpret_cast<const char*>(&f32), sizeof(f32));
+ };
+ std::stringstream i_buffer;
+ auto write_i_buffer = std::bind(write_buffer_float, std::ref(i_buffer), std::placeholders::_1);
+ for (auto bit : input_bits)
+ write_i_buffer(arrival_times.at(bit, 0));
+ //std::stringstream o_buffer;
+ //auto write_o_buffer = std::bind(write_buffer_float, std::ref(o_buffer), std::placeholders::_1);
+ //for (auto bit : output_bits)
+ // write_o_buffer(0);
+ if (!box_list.empty()) {
RTLIL::Module *holes_module = module->design->addModule("$__holes__");
log_assert(holes_module);
@@ -639,23 +666,16 @@ struct XAigerWriter
write_h_buffer(box_inputs);
write_h_buffer(box_outputs);
- write_h_buffer(box_module->attributes.at("\\abc_box_id").as_int());
+ write_h_buffer(box_module->attributes.at("\\abc9_box_id").as_int());
write_h_buffer(box_count++);
}
- f << "h";
- std::string buffer_str = h_buffer.str();
- int32_t buffer_size_be = to_big_endian(buffer_str.size());
- f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
- f.write(buffer_str.data(), buffer_str.size());
-
std::stringstream r_buffer;
auto write_r_buffer = std::bind(write_buffer, std::ref(r_buffer), std::placeholders::_1);
write_r_buffer(0);
-
f << "r";
- buffer_str = r_buffer.str();
- buffer_size_be = to_big_endian(buffer_str.size());
+ std::string buffer_str = r_buffer.str();
+ int32_t buffer_size_be = to_big_endian(buffer_str.size());
f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
f.write(buffer_str.data(), buffer_str.size());
@@ -709,6 +729,23 @@ struct XAigerWriter
}
}
+ f << "h";
+ std::string buffer_str = h_buffer.str();
+ int32_t buffer_size_be = to_big_endian(buffer_str.size());
+ f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
+ f.write(buffer_str.data(), buffer_str.size());
+
+ f << "i";
+ buffer_str = i_buffer.str();
+ buffer_size_be = to_big_endian(buffer_str.size());
+ f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
+ f.write(buffer_str.data(), buffer_str.size());
+ //f << "o";
+ //buffer_str = o_buffer.str();
+ //buffer_size_be = to_big_endian(buffer_str.size());
+ //f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
+ //f.write(buffer_str.data(), buffer_str.size());
+
f << stringf("Generated by %s\n", yosys_version_str);
}
@@ -760,11 +797,11 @@ struct XAigerWriter
f << stringf("box %d %d %s\n", box_count++, 0, log_id(cell->name));
output_lines.sort();
+ if (omode)
+ output_lines[State::S0] = "output 0 0 $__dummy__\n";
for (auto &it : output_lines)
f << it.second;
log_assert(output_lines.size() == output_bits.size());
- if (omode && output_bits.empty())
- f << "output " << output_lines.size() << " 0 $__dummy__\n";
wire_lines.sort();
for (auto &it : wire_lines)
@@ -819,7 +856,7 @@ struct XAigerBackend : public Backend {
}
break;
}
- extra_args(f, filename, args, argidx);
+ extra_args(f, filename, args, argidx, !ascii_mode);
Module *top_module = design->top_module();
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 7c054d655..9e316a055 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -569,7 +569,7 @@ struct BtorWorker
int nid_init_val = -1;
if (!initval.is_fully_undef())
- nid_init_val = get_sig_nid(initval);
+ nid_init_val = get_sig_nid(initval, -1, false, true);
int sid = get_bv_sid(GetSize(sig_q));
int nid = next_nid++;
@@ -681,11 +681,11 @@ struct BtorWorker
{
if (verbose)
btorf("; initval = %s\n", log_signal(firstword));
- nid_init_val = get_sig_nid(firstword);
+ nid_init_val = get_sig_nid(firstword, -1, false, true);
}
else
{
- int nid_init_val = next_nid++;
+ nid_init_val = next_nid++;
btorf("%d state %d\n", nid_init_val, sid);
for (int i = 0; i < nwords; i++) {
@@ -693,8 +693,8 @@ struct BtorWorker
if (thisword.is_fully_undef())
continue;
Const thisaddr(i, abits);
- int nid_thisword = get_sig_nid(thisword);
- int nid_thisaddr = get_sig_nid(thisaddr);
+ int nid_thisword = get_sig_nid(thisword, -1, false, true);
+ int nid_thisaddr = get_sig_nid(thisaddr, -1, false, true);
int last_nid_init_val = nid_init_val;
nid_init_val = next_nid++;
if (verbose)
@@ -792,7 +792,7 @@ struct BtorWorker
cell_recursion_guard.erase(cell);
}
- int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false)
+ int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false, bool is_init = false)
{
int nid = -1;
sigmap.apply(sig);
@@ -823,7 +823,10 @@ struct BtorWorker
int sid = get_bv_sid(GetSize(sig));
int nid_input = next_nid++;
- btorf("%d input %d\n", nid_input, sid);
+ if (is_init)
+ btorf("%d state %d\n", nid_input, sid);
+ else
+ btorf("%d input %d\n", nid_input, sid);
int nid_masked_input;
if (sig_mask_undef.is_fully_ones()) {
@@ -897,9 +900,12 @@ struct BtorWorker
int sid = get_bv_sid(GetSize(s));
int nid = next_nid++;
- btorf("%d input %d %s\n", nid, sid);
+ btorf("%d input %d\n", nid, sid);
nid_width[nid] = GetSize(s);
+ for (int j = 0; j < GetSize(s); j++)
+ nidbits.push_back(make_pair(nid, j));
+
i += GetSize(s)-1;
continue;
}
diff --git a/backends/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc
index fff110bb0..671686173 100644
--- a/backends/protobuf/protobuf.cc
+++ b/backends/protobuf/protobuf.cc
@@ -266,7 +266,7 @@ struct ProtobufBackend : public Backend {
}
break;
}
- extra_args(f, filename, args, argidx);
+ extra_args(f, filename, args, argidx, !text_mode);
log_header(design, "Executing Protobuf backend.\n");
@@ -338,7 +338,7 @@ struct ProtobufPass : public Pass {
if (!filename.empty()) {
rewrite_filename(filename);
std::ofstream *ff = new std::ofstream;
- ff->open(filename.c_str(), std::ofstream::trunc);
+ ff->open(filename.c_str(), text_mode ? std::ofstream::trunc : (std::ofstream::trunc | std::ofstream::binary));
if (ff->fail()) {
delete ff;
log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno));
diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc
index 92941d4cf..68394a909 100644
--- a/backends/smt2/Makefile.inc
+++ b/backends/smt2/Makefile.inc
@@ -16,7 +16,7 @@ yosys-smtbmc-script.py: backends/smt2/smtbmc.py
-e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
yosys-smtbmc.exe: misc/launcher.c yosys-smtbmc-script.py
- $(P) gcc -DGUI=0 -O -s -o $@ $<
+ $(P) $(CXX) -DGUI=0 -O -s -o $@ $<
# Other targets
else
TARGETS += yosys-smtbmc
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 445a42e0d..3d6d3e1b3 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -1256,7 +1256,7 @@ def smt_check_sat():
return smt.check_sat()
if tempind:
- retstatus = False
+ retstatus = "FAILED"
skip_counter = step_size
for step in range(num_steps, -1, -1):
if smt.forall:
@@ -1303,7 +1303,7 @@ if tempind:
else:
print_msg("Temporal induction successful.")
- retstatus = True
+ retstatus = "PASSED"
break
elif covermode:
@@ -1321,7 +1321,7 @@ elif covermode:
smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr))
step = 0
- retstatus = False
+ retstatus = "FAILED"
found_failed_assert = False
assert step_size == 1
@@ -1365,7 +1365,7 @@ elif covermode:
if smt_check_sat() == "unsat":
print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
found_failed_assert = True
- retstatus = False
+ retstatus = "FAILED"
break
reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
@@ -1400,7 +1400,7 @@ elif covermode:
break
if "1" not in cover_mask:
- retstatus = True
+ retstatus = "PASSED"
break
step += 1
@@ -1412,7 +1412,7 @@ elif covermode:
else: # not tempind, covermode
step = 0
- retstatus = True
+ retstatus = "PASSED"
while step < num_steps:
smt_state(step)
smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
@@ -1459,8 +1459,8 @@ else: # not tempind, covermode
print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step))
if smt_check_sat() == "unsat":
- print("%s Warmup failed!" % smt.timestamp())
- retstatus = False
+ print("%s Assumptions are unsatisfiable!" % smt.timestamp())
+ retstatus = "PREUNSAT"
break
if not final_only:
@@ -1487,13 +1487,13 @@ else: # not tempind, covermode
print_msg("Re-solving with appended steps..")
if smt_check_sat() == "unsat":
print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
- retstatus = False
+ retstatus = "FAILED"
break
print_anyconsts(step)
for i in range(step, last_check_step+1):
print_failed_asserts(i)
write_trace(0, last_check_step+1+append_steps, '%')
- retstatus = False
+ retstatus = "FAILED"
break
smt_pop()
@@ -1519,7 +1519,7 @@ else: # not tempind, covermode
print_anyconsts(i)
print_failed_asserts(i, final=True)
write_trace(0, i+1, '%')
- retstatus = False
+ retstatus = "FAILED"
break
smt_pop()
@@ -1534,7 +1534,7 @@ else: # not tempind, covermode
print_msg("Solving for step %d.." % (last_check_step))
if smt_check_sat() != "sat":
print("%s No solution found!" % smt.timestamp())
- retstatus = False
+ retstatus = "FAILED"
break
elif dumpall:
@@ -1551,5 +1551,5 @@ else: # not tempind, covermode
smt.write("(exit)")
smt.wait()
-print_msg("Status: %s" % ("PASSED" if retstatus else "FAILED (!)"))
-sys.exit(0 if retstatus else 1)
+print_msg("Status: %s" % retstatus)
+sys.exit(0 if retstatus == "PASSED" else 1)
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 11:00:09 +0000