aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/aiger/xaiger.cc92
-rw-r--r--backends/edif/edif.cc43
-rw-r--r--backends/firrtl/firrtl.cc1
-rw-r--r--backends/json/json.cc6
-rw-r--r--backends/smt2/smt2.cc20
-rw-r--r--backends/smt2/smtbmc.py14
-rw-r--r--backends/smt2/smtio.py16
-rw-r--r--backends/verilog/verilog_backend.cc13
8 files changed, 125 insertions, 80 deletions
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index 76b7efbfc..cde6d066a 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -47,6 +47,7 @@ inline static uint32_t bswap32(uint32_t x)
#include "kernel/yosys.h"
#include "kernel/sigtools.h"
#include "kernel/utils.h"
+#include "kernel/timinginfo.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
@@ -173,20 +174,21 @@ struct XAigerWriter
undriven_bits.insert(bit);
unused_bits.insert(bit);
- bool keep = wire->get_bool_attribute(ID::keep);
- if (wire->port_input || keep)
+ bool scc = wire->attributes.count(ID(abc9_scc));
+ if (wire->port_input || scc)
input_bits.insert(bit);
- if (wire->port_output || keep) {
+ bool keep = wire->get_bool_attribute(ID::keep);
+ if (wire->port_output || keep || scc) {
if (bit != wirebit)
alias_map[wirebit] = bit;
output_bits.insert(wirebit);
}
}
- dict<IdString,dict<IdString,std::vector<int>>> arrivals_cache;
+ TimingInfo timing;
+
for (auto cell : module->cells()) {
- RTLIL::Module* inst_module = module->design->module(cell->type);
if (!cell->has_keep_attr()) {
if (cell->type == "$_NOT_")
{
@@ -222,13 +224,21 @@ struct XAigerWriter
alias_map[Q] = D;
auto r YS_ATTRIBUTE(unused) = ff_bits.insert(std::make_pair(D, cell));
log_assert(r.second);
- if (input_bits.erase(Q))
- log_assert(Q.wire->attributes.count(ID::keep));
continue;
}
- if (inst_module) {
- bool abc9_flop = false;
+ if (cell->type.in("$specify2", "$specify3", "$specrule"))
+ continue;
+ }
+
+ RTLIL::Module* inst_module = module->design->module(cell->type);
+ if (inst_module) {
+ IdString derived_type = inst_module->derive(module->design, cell->parameters);
+ inst_module = module->design->module(derived_type);
+ log_assert(inst_module);
+
+ bool abc9_flop = false;
+ if (!cell->has_keep_attr()) {
auto it = cell->attributes.find("\\abc9_box_seq");
if (it != cell->attributes.end()) {
int abc9_box_seq = it->second.as_int();
@@ -241,50 +251,34 @@ struct XAigerWriter
if (!abc9_flop)
continue;
}
+ }
- auto &cell_arrivals = arrivals_cache[cell->type];
- for (const auto &conn : cell->connections()) {
- auto port_wire = inst_module->wire(conn.first);
- if (!port_wire->port_output)
- continue;
-
- auto r = cell_arrivals.insert(conn.first);
- auto &arrivals = r.first->second;
- if (r.second) {
- auto it = port_wire->attributes.find("\\abc9_arrival");
- if (it == port_wire->attributes.end())
- continue;
- if (it->second.flags == 0)
- arrivals.emplace_back(it->second.as_int());
- else
- for (const auto &tok : split_tokens(it->second.decode_string()))
- arrivals.push_back(atoi(tok.c_str()));
- }
+ if (!timing.count(derived_type))
+ timing.setup_module(inst_module);
+ auto &t = timing.at(derived_type).arrival;
+ for (const auto &conn : cell->connections()) {
+ auto port_wire = inst_module->wire(conn.first);
+ if (!port_wire->port_output)
+ continue;
- if (arrivals.empty())
+ for (int i = 0; i < GetSize(conn.second); i++) {
+ auto d = t.at(TimingInfo::NameBit(conn.first,i), 0);
+ if (d == 0)
continue;
- if (GetSize(arrivals) > 1 && GetSize(arrivals) != GetSize(port_wire))
- log_error("%s.%s is %d bits wide but abc9_arrival = %s has %d value(s)!\n", log_id(cell->type), log_id(conn.first),
- GetSize(port_wire), log_signal(it->second), GetSize(arrivals));
-
- auto jt = arrivals.begin();
#ifndef NDEBUG
if (ys_debug(1)) {
- static std::set<std::pair<IdString,IdString>> seen;
- if (seen.emplace(cell->type, conn.first).second) log("%s.%s abc9_arrival = %d\n", log_id(cell->type), log_id(conn.first), *jt);
+ static std::set<std::tuple<IdString,IdString,int>> seen;
+ if (seen.emplace(derived_type, conn.first, i).second) log("%s.%s[%d] abc9_arrival = %d\n",
+ log_id(cell->type), log_id(conn.first), i, d);
}
#endif
- for (auto bit : sigmap(conn.second)) {
- arrival_times[bit] = *jt;
- if (arrivals.size() > 1)
- jt++;
- }
+ arrival_times[conn.second[i]] = d;
}
-
- if (abc9_flop)
- continue;
}
+
+ if (abc9_flop)
+ continue;
}
bool cell_known = inst_module || cell->known();
@@ -383,11 +377,6 @@ struct XAigerWriter
alias_map[O] = b;
ci_bits.emplace_back(b);
undriven_bits.erase(O);
- // If PI and CI, then must be a (* keep *) wire
- if (input_bits.erase(O)) {
- log_assert(output_bits.count(O));
- log_assert(O.wire->get_bool_attribute(ID::keep));
- }
}
}
@@ -472,8 +461,8 @@ struct XAigerWriter
for (const auto &bit : output_bits) {
ordered_outputs[bit] = aig_o++;
int aig;
- // Unlike bit2aig() which checks aig_map first, for
- // inout/keep bits, since aig_map will point to
+ // Unlike bit2aig() which checks aig_map first for
+ // inout/scc bits, since aig_map will point to
// the PI, first attempt to find the NOT/AND driver
// before resorting to an aig_map lookup (which
// could be another PO)
@@ -650,7 +639,7 @@ struct XAigerWriter
log_assert(mergeability > 0);
write_r_buffer(mergeability);
- Const init = cell->attributes.at(ID(abc9_init));
+ Const init = cell->attributes.at(ID(abc9_init), State::Sx);
log_assert(GetSize(init) == 1);
if (init == State::S1)
write_s_buffer(1);
@@ -661,6 +650,7 @@ struct XAigerWriter
write_s_buffer(0);
}
+ // Use arrival time from output of flop box
write_i_buffer(arrival_times.at(d, 0));
//write_o_buffer(0);
}
diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc
index 616b754ce..199560ad0 100644
--- a/backends/edif/edif.cc
+++ b/backends/edif/edif.cc
@@ -246,19 +246,25 @@ struct EdifBackend : public Backend {
else if (!ct.cell_input(cell_it.first, port_it.first))
dir = "OUTPUT";
}
- if (port_it.second == 1)
+ int width = port_it.second;
+ int start = 0;
+ bool upto = false;
+ auto m = design->module(cell_it.first);
+ if (m) {
+ auto w = m->wire(port_it.first);
+ if (w) {
+ width = GetSize(w);
+ start = w->start_offset;
+ upto = w->upto;
+ }
+ }
+ if (width == 1)
*f << stringf(" (port %s (direction %s))\n", EDIF_DEF(port_it.first), dir);
else {
- int b[2] = {port_it.second-1, 0};
- auto m = design->module(cell_it.first);
- if (m) {
- auto w = m->wire(port_it.first);
- if (w) {
- b[w->upto ? 0 : 1] = w->start_offset;
- b[w->upto ? 1 : 0] = w->start_offset+GetSize(w)-1;
- }
- }
- *f << stringf(" (port (array %s %d) (direction %s))\n", EDIF_DEFR(port_it.first, port_rename, b[0], b[1]), port_it.second, dir);
+ int b[2];
+ b[upto ? 0 : 1] = start;
+ b[upto ? 1 : 0] = start+width-1;
+ *f << stringf(" (port (array %s %d) (direction %s))\n", EDIF_DEFR(port_it.first, port_rename, b[0], b[1]), width, dir);
}
}
*f << stringf(" )\n");
@@ -390,18 +396,23 @@ struct EdifBackend : public Backend {
if (sig[i].wire == NULL && sig[i] != RTLIL::State::S0 && sig[i] != RTLIL::State::S1)
log_warning("Bit %d of cell port %s.%s.%s driven by %s will be left unconnected in EDIF output.\n",
i, log_id(module), log_id(cell), log_id(p.first), log_signal(sig[i]));
- else if (sig.size() == 1)
- net_join_db[sig[i]].insert(make_pair(stringf("(portRef %s (instanceRef %s))", EDIF_REF(p.first), EDIF_REF(cell->name)), cell->output(p.first)));
else {
int member_idx = GetSize(sig)-i-1;
auto m = design->module(cell->type);
+ int width = sig.size();
if (m) {
auto w = m->wire(p.first);
- if (w)
+ if (w) {
member_idx = GetSize(w)-i-1;
+ width = GetSize(w);
+ }
+ }
+ if (width == 1)
+ net_join_db[sig[i]].insert(make_pair(stringf("(portRef %s (instanceRef %s))", EDIF_REF(p.first), EDIF_REF(cell->name)), cell->output(p.first)));
+ else {
+ net_join_db[sig[i]].insert(make_pair(stringf("(portRef (member %s %d) (instanceRef %s))",
+ EDIF_REF(p.first), member_idx, EDIF_REF(cell->name)), cell->output(p.first)));
}
- net_join_db[sig[i]].insert(make_pair(stringf("(portRef (member %s %d) (instanceRef %s))",
- EDIF_REF(p.first), member_idx, EDIF_REF(cell->name)), cell->output(p.first)));
}
}
}
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index 87db0edf7..22aa686a7 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -25,7 +25,6 @@
#include "kernel/log.h"
#include <algorithm>
#include <string>
-#include <regex>
#include <vector>
#include <cmath>
diff --git a/backends/json/json.cc b/backends/json/json.cc
index 5c67cb857..6c924ff99 100644
--- a/backends/json/json.cc
+++ b/backends/json/json.cc
@@ -104,7 +104,7 @@ struct JsonWriter
if (state < 2)
str += " ";
f << get_string(str);
- } else if (compat_int_mode && GetSize(value) == 32 && value.is_fully_def()) {
+ } else if (compat_int_mode && GetSize(value) <= 32 && value.is_fully_def()) {
if ((value.flags & RTLIL::ConstFlags::CONST_FLAG_SIGNED) != 0)
f << stringf("%d", value.as_int());
else
@@ -296,7 +296,7 @@ struct JsonBackend : public Backend {
log(" include AIG models for the different gate types\n");
log("\n");
log(" -compat-int\n");
- log(" emit 32-bit fully-defined parameter values directly\n");
+ log(" emit 32-bit or smaller fully-defined parameter values directly\n");
log(" as JSON numbers (for compatibility with old parsers)\n");
log("\n");
log("\n");
@@ -540,7 +540,7 @@ struct JsonPass : public Pass {
log(" also include AIG models for the different gate types\n");
log("\n");
log(" -compat-int\n");
- log(" emit 32-bit fully-defined parameter values directly\n");
+ log(" emit 32-bit or smaller fully-defined parameter values directly\n");
log(" as JSON numbers (for compatibility with old parsers)\n");
log("\n");
log("See 'help write_json' for a description of the JSON format used.\n");
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 081dcda99..628765831 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -536,6 +536,14 @@ struct Smt2Worker
if (cell->attributes.count("\\reg"))
infostr += " " + cell->attributes.at("\\reg").decode_string();
decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort("\\Y")), infostr.c_str()));
+ if (cell->getPort("\\Y").is_wire() && cell->getPort("\\Y").as_wire()->get_bool_attribute("\\maximize")){
+ decls.push_back(stringf("; yosys-smt2-maximize %s#%d\n", get_id(module), idcounter));
+ log("Wire %s is maximized\n", cell->getPort("\\Y").as_wire()->name.str().c_str());
+ }
+ else if (cell->getPort("\\Y").is_wire() && cell->getPort("\\Y").as_wire()->get_bool_attribute("\\minimize")){
+ decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter));
+ log("Wire %s is minimized\n", cell->getPort("\\Y").as_wire()->name.str().c_str());
+ }
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y")));
if (cell->type == "$anyseq")
ex_input_eq.push_back(stringf(" (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter));
@@ -1386,7 +1394,7 @@ struct Smt2Backend : public Backend {
log("\n");
log("For this proof we create the following template (test.tpl).\n");
log("\n");
- log(" ; we need QF_UFBV for this poof\n");
+ log(" ; we need QF_UFBV for this proof\n");
log(" (set-logic QF_UFBV)\n");
log("\n");
log(" ; insert the auto-generated code here\n");
@@ -1500,11 +1508,11 @@ struct Smt2Backend : public Backend {
// extract module dependencies
std::map<RTLIL::Module*, std::set<RTLIL::Module*>> module_deps;
- for (auto &mod_it : design->modules_) {
- module_deps[mod_it.second] = std::set<RTLIL::Module*>();
- for (auto &cell_it : mod_it.second->cells_)
- if (design->modules_.count(cell_it.second->type) > 0)
- module_deps[mod_it.second].insert(design->modules_.at(cell_it.second->type));
+ for (auto mod : design->modules()) {
+ module_deps[mod] = std::set<RTLIL::Module*>();
+ for (auto cell : mod->cells())
+ if (design->has(cell->type))
+ module_deps[mod].insert(design->module(cell->type));
}
// simple good-enough topological sort
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 3d6d3e1b3..630464419 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -1158,6 +1158,8 @@ def smt_forall_assert():
global asserts_cache_dirty
asserts_cache_dirty = False
+ assert (len(smt.modinfo[topmod].maximize) + len(smt.modinfo[topmod].minimize) <= 1)
+
def make_assert_expr(asserts_cache):
expr = list()
for lst in asserts_cache:
@@ -1236,6 +1238,18 @@ def smt_forall_assert():
smt.write("".join(assert_expr))
+ if len(smt.modinfo[topmod].maximize) > 0:
+ for s in states:
+ if s in used_states_db:
+ smt.write("(maximize (|%s| %s))\n" % (smt.modinfo[topmod].maximize.copy().pop(), s))
+ break
+
+ if len(smt.modinfo[topmod].minimize) > 0:
+ for s in states:
+ if s in used_states_db:
+ smt.write("(minimize (|%s| %s))\n" % (smt.modinfo[topmod].minimize.copy().pop(), s))
+ break
+
def smt_push():
global asserts_cache_dirty
asserts_cache_dirty = True
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 34bf7ef38..69f59df79 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -101,6 +101,8 @@ class SmtModInfo:
self.cells = dict()
self.asserts = dict()
self.covers = dict()
+ self.maximize = set()
+ self.minimize = set()
self.anyconsts = dict()
self.anyseqs = dict()
self.allconsts = dict()
@@ -502,6 +504,12 @@ class SmtIo:
if fields[1] == "yosys-smt2-cover":
self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
+ if fields[1] == "yosys-smt2-maximize":
+ self.modinfo[self.curmod].maximize.add(fields[2])
+
+ if fields[1] == "yosys-smt2-minimize":
+ self.modinfo[self.curmod].minimize.add(fields[2])
+
if fields[1] == "yosys-smt2-anyconst":
self.modinfo[self.curmod].anyconsts[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
@@ -696,7 +704,13 @@ class SmtIo:
if msg is not None:
print("%s waiting for solver (%s)" % (self.timestamp(), msg), flush=True)
- result = self.read()
+ if self.forall:
+ result = self.read()
+ while result not in ["sat", "unsat", "unknown"]:
+ print("%s %s: %s" % (self.timestamp(), self.solver, result))
+ result = self.read()
+ else:
+ result = self.read()
if self.debug_file:
print("(set-info :status %s)" % result, file=self.debug_file)
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 54d0f6148..19541f1c4 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -1066,6 +1066,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
// initial begin
// memid[0] = ...
// end
+ dump_attributes(f, indent.c_str(), cell->attributes);
f << stringf("%s" "reg [%d:%d] %s [%d:%d];\n", indent.c_str(), width-1, 0, mem_id.c_str(), size+offset-1, offset);
if (use_init)
{
@@ -1416,11 +1417,19 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
decimal = 1;
f << ", ";
- dump_const(f, cell->getParam("\\T_LIMIT"));
+ dump_const(f, cell->getParam("\\T_LIMIT_MIN"));
+ f << ": ";
+ dump_const(f, cell->getParam("\\T_LIMIT_TYP"));
+ f << ": ";
+ dump_const(f, cell->getParam("\\T_LIMIT_MAX"));
if (spec_type == "$setuphold" || spec_type == "$recrem" || spec_type == "$fullskew") {
f << ", ";
- dump_const(f, cell->getParam("\\T_LIMIT2"));
+ dump_const(f, cell->getParam("\\T_LIMIT2_MIN"));
+ f << ": ";
+ dump_const(f, cell->getParam("\\T_LIMIT2_TYP"));
+ f << ": ";
+ dump_const(f, cell->getParam("\\T_LIMIT2_MAX"));
}
f << ");\n";
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-08 05:28:30 +0000