aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--backends/btor/btor.cc7
-rw-r--r--misc/py_wrap_generator.py292
-rw-r--r--passes/cmds/Makefile.inc1
-rw-r--r--passes/cmds/autoname.cc134
-rw-r--r--passes/fsm/fsm_detect.cc16
-rw-r--r--passes/techmap/flowmap.cc5
-rw-r--r--techlibs/common/cmp2lut.v2
-rw-r--r--techlibs/ecp5/synth_ecp5.cc1
-rw-r--r--techlibs/ice40/cells_sim.v450
-rw-r--r--techlibs/ice40/synth_ice40.cc1
-rw-r--r--tests/arch/anlogic/fsm.ys11
-rw-r--r--tests/arch/ecp5/fsm.ys13
-rw-r--r--tests/arch/efinix/fsm.ys8
-rw-r--r--tests/arch/ice40/fsm.ys13
-rw-r--r--tests/arch/xilinx/fsm.ys6
15 files changed, 913 insertions, 47 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 9e316a055..c1da4b127 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -1070,7 +1070,12 @@ struct BtorWorker
bad_properties.push_back(nid_en_and_not_a);
} else {
int nid = next_nid++;
- btorf("%d bad %d\n", nid, nid_en_and_not_a);
+ string infostr = log_id(cell);
+ if (infostr[0] == '$' && cell->attributes.count("\\src")) {
+ infostr = cell->attributes.at("\\src").decode_string().c_str();
+ std::replace(infostr.begin(), infostr.end(), ' ', '_');
+ }
+ btorf("%d bad %d %s\n", nid, nid_en_and_not_a, infostr.c_str());
}
btorf_pop(log_id(cell));
diff --git a/misc/py_wrap_generator.py b/misc/py_wrap_generator.py
index 4ce8e947e..c58c3f66a 100644
--- a/misc/py_wrap_generator.py
+++ b/misc/py_wrap_generator.py
@@ -253,6 +253,8 @@ class WContainer:
candidate = WType.from_string(arg.strip(), containing_file, line_number)
if candidate == None:
return None
+ if candidate.name == "void":
+ return None
cont.args.append(candidate)
return cont
@@ -880,11 +882,8 @@ class WClass:
text += fun.gen_def_virtual()
return text
- def gen_boost_py(self):
- text = "\n\t\tclass_<" + self.name
- if self.link_type == link_types.derive:
- text += "Wrap, boost::noncopyable"
- text += ">(\"" + self.name + "\""
+ def gen_boost_py_body(self):
+ text = ""
if self.printable_constrs() == 0 or not self.contains_default_constr():
text += ", no_init"
text += ")"
@@ -907,6 +906,21 @@ class WClass:
text += "\n\t\t\t;\n"
return text
+ def gen_boost_py(self):
+ body = self.gen_boost_py_body()
+ if self.link_type == link_types.derive:
+ text = "\n\t\tclass_<" + self.name + ">(\"Cpp" + self.name + "\""
+ text += body
+ text += "\n\t\tclass_<" + self.name
+ text += "Wrap, boost::noncopyable"
+ text += ">(\"" + self.name + "\""
+ text += body
+ else:
+ text = "\n\t\tclass_<" + self.name + ">(\"" + self.name + "\""
+ text += body
+ return text
+
+
def contains_default_constr(self):
for c in self.found_constrs:
if len(c.args) == 0:
@@ -974,6 +988,7 @@ blacklist_methods = ["YOSYS_NAMESPACE::Pass::run_register", "YOSYS_NAMESPACE::Mo
enum_names = ["State","SyncType","ConstFlags"]
enums = [] #Do not edit
+glbls = []
unowned_functions = []
@@ -1723,6 +1738,159 @@ class WMember:
text += ")"
return text
+class WGlobal:
+ orig_text = None
+ wtype = attr_types.default
+ name = None
+ containing_file = None
+ namespace = ""
+ is_const = False
+
+ def from_string(str_def, containing_file, line_number, namespace):
+ glbl = WGlobal()
+ glbl.orig_text = str_def
+ glbl.wtype = None
+ glbl.name = ""
+ glbl.containing_file = containing_file
+ glbl.namespace = namespace
+ glbl.is_const = False
+
+ if not str.startswith(str_def, "extern"):
+ return None
+ str_def = str_def[7:]
+
+ if str.startswith(str_def, "const "):
+ glbl.is_const = True
+ str_def = str_def[6:]
+
+ if str_def.count(" ") == 0:
+ return None
+
+ parts = split_list(str_def.strip(), " ")
+
+ prefix = ""
+ i = 0
+ for part in parts:
+ if part in ["unsigned", "long", "short"]:
+ prefix += part + " "
+ i += 1
+ else:
+ break
+ parts = parts[i:]
+
+ if len(parts) <= 1:
+ return None
+
+ glbl.wtype = WType.from_string(prefix + parts[0], containing_file, line_number)
+
+ if glbl.wtype == None:
+ return None
+
+ str_def = parts[1]
+ for part in parts[2:]:
+ str_def = str_def + " " + part
+
+ if str_def.find("(") != -1 or str_def.find(")") != -1 or str_def.find("{") != -1 or str_def.find("}") != -1:
+ return None
+
+ found = str_def.find(";")
+ if found == -1:
+ return None
+
+ found_eq = str_def.find("=")
+ if found_eq != -1:
+ found = found_eq
+
+ glbl.name = str_def[:found]
+ str_def = str_def[found+1:]
+ if glbl.name.find("*") == 0:
+ glbl.name = glbl.name.replace("*", "")
+ glbl.wtype.attr_type = attr_types.star
+ if glbl.name.find("&&") == 0:
+ glbl.name = glbl.name.replace("&&", "")
+ glbl.wtype.attr_type = attr_types.ampamp
+ if glbl.name.find("&") == 0:
+ glbl.name = glbl.name.replace("&", "")
+ glbl.wtype.attr_type = attr_types.amp
+
+ if(len(str_def.strip()) != 0):
+ return None
+
+ if len(glbl.name.split(",")) > 1:
+ glbl_list = []
+ for name in glbl.name.split(","):
+ name = name.strip();
+ glbl_list.append(WGlobal())
+ glbl_list[-1].orig_text = glbl.orig_text
+ glbl_list[-1].wtype = glbl.wtype
+ glbl_list[-1].name = name
+ glbl_list[-1].containing_file = glbl.containing_file
+ glbl_list[-1].namespace = glbl.namespace
+ glbl_list[-1].is_const = glbl.is_const
+ return glbl_list
+
+ return glbl
+
+ def gen_def(self):
+ text = "\n\t"
+ if self.is_const:
+ text += "const "
+ text += self.wtype.gen_text() + " get_var_py_" + self.name + "()"
+ text += "\n\t{\n\t\t"
+ if self.wtype.attr_type == attr_types.star:
+ text += "if(" + self.namespace + "::" + self.name + " == NULL)\n\t\t\t"
+ text += "throw std::runtime_error(\"" + self.namespace + "::" + self.name + " is NULL\");\n\t\t"
+ if self.wtype.name in known_containers:
+ text += self.wtype.gen_text_cpp()
+ else:
+ if self.is_const:
+ text += "const "
+ text += self.wtype.gen_text()
+
+ if self.wtype.name in classnames or (self.wtype.name in known_containers and self.wtype.attr_type == attr_types.star):
+ text += "*"
+ text += " ret_ = "
+ if self.wtype.name in classnames:
+ text += self.wtype.name + "::get_py_obj("
+ if self.wtype.attr_type != attr_types.star:
+ text += "&"
+ text += self.namespace + "::" + self.name
+ if self.wtype.name in classnames:
+ text += ")"
+ text += ";"
+
+ if self.wtype.name in classnames:
+ text += "\n\t\treturn *ret_;"
+ elif self.wtype.name in known_containers:
+ text += known_containers[self.wtype.name].translate_cpp("ret_", self.wtype.cont.args, "\n\t\t", self.wtype.attr_type == attr_types.star)
+ text += "\n\t\treturn ret____tmp;"
+ else:
+ text += "\n\t\treturn ret_;"
+ text += "\n\t}\n"
+
+ if self.is_const:
+ return text
+
+ ret = Attribute(self.wtype, "rhs");
+
+ if self.wtype.name in classnames:
+ text += "\n\tvoid set_var_py_" + self.name + "(" + self.wtype.gen_text() + " *rhs)"
+ else:
+ text += "\n\tvoid set_var_py_" + self.name + "(" + self.wtype.gen_text() + " rhs)"
+ text += "\n\t{"
+ text += ret.gen_translation()
+ text += "\n\t\t" + self.namespace + "::" + self.name + " = " + ret.gen_call() + ";"
+ text += "\n\t}\n"
+
+ return text;
+
+ def gen_boost_py(self):
+ text = "\n\t\t\t.add_static_property(\"" + self.name + "\", &" + "YOSYS_PYTHON::get_var_py_" + self.name
+ if not self.is_const:
+ text += ", &YOSYS_PYTHON::set_var_py_" + self.name
+ text += ")"
+ return text
+
def concat_namespace(tuple_list):
if len(tuple_list) == 0:
return ""
@@ -1859,6 +2027,16 @@ def parse_header(source):
else:
debug("\t\tFound member \"" + candidate.name + "\" of class \"" + class_[0].name + "\" of type \"" + candidate.wtype.name + "\"", 2)
class_[0].found_vars.append(candidate)
+ if candidate == None and class_ == None:
+ candidate = WGlobal.from_string(ugly_line, source.name, i, concat_namespace(namespaces))
+ if candidate != None:
+ if type(candidate) == list:
+ for c in candidate:
+ glbls.append(c)
+ debug("\tFound global \"" + c.name + "\" in namespace " + concat_namespace(namespaces), 2)
+ else:
+ glbls.append(candidate)
+ debug("\tFound global \"" + candidate.name + "\" in namespace " + concat_namespace(namespaces), 2)
j = i
line = unpretty_string(line)
@@ -1888,6 +2066,17 @@ def parse_header(source):
debug("\t\tFound constructor of class \"" + class_[0].name + "\" in namespace " + concat_namespace(namespaces),2)
class_[0].found_constrs.append(candidate)
continue
+ if class_ == None:
+ candidate = WGlobal.from_string(line, source.name, i, concat_namespace(namespaces))
+ if candidate != None:
+ if type(candidate) == list:
+ for c in candidate:
+ glbls.append(c)
+ debug("\tFound global \"" + c.name + "\" in namespace " + concat_namespace(namespaces), 2)
+ else:
+ glbls.append(candidate)
+ debug("\tFound global \"" + candidate.name + "\" in namespace " + concat_namespace(namespaces), 2)
+ continue
if candidate != None:
while i < j:
i += 1
@@ -1990,6 +2179,7 @@ def gen_wrappers(filename, debug_level_ = 0):
if len(class_.found_constrs) == 0:
class_.found_constrs.append(WConstructor(source.name, class_))
debug(str(len(unowned_functions)) + " functions are unowned", 1)
+ debug(str(len(unowned_functions)) + " global variables", 1)
for enum in enums:
debug("Enum " + assure_length(enum.name, len(max(enum_names, key=len)), True) + " contains " + assure_length(str(len(enum.values)), 2, False) + " values", 1)
debug("-"*col, 1)
@@ -2025,10 +2215,15 @@ def gen_wrappers(filename, debug_level_ = 0):
#include <boost/python/wrapper.hpp>
#include <boost/python/call.hpp>
#include <boost/python.hpp>
-
+#include <iosfwd> // std::streamsize
+#include <iostream>
+#include <boost/iostreams/concepts.hpp> // boost::iostreams::sink
+#include <boost/iostreams/stream.hpp>
USING_YOSYS_NAMESPACE
namespace YOSYS_PYTHON {
+
+ struct YosysStatics{};
""")
for source in sources:
@@ -2050,6 +2245,9 @@ namespace YOSYS_PYTHON {
for fun in unowned_functions:
wrapper_file.write(fun.gen_def())
+ for glbl in glbls:
+ wrapper_file.write(glbl.gen_def())
+
wrapper_file.write(""" struct Initializer
{
Initializer() {
@@ -2068,12 +2266,89 @@ namespace YOSYS_PYTHON {
}
};
+
+ /// source: https://stackoverflow.com/questions/26033781/converting-python-io-object-to-stdostream-when-using-boostpython?noredirect=1&lq=1
+ /// @brief Type that implements the Boost.IOStream's Sink and Flushable
+ /// concept for writing data to Python object that support:
+ /// n = object.write(str) # n = None or bytes written
+ /// object.flush() # if flush exists, then it is callable
+ class PythonOutputDevice
+ {
+ public:
+
+ // This class models both the Sink and Flushable concepts.
+ struct category
+ : boost::iostreams::sink_tag,
+ boost::iostreams::flushable_tag
+ {};
+
+ explicit
+ PythonOutputDevice(boost::python::object object)
+ : object_(object)
+ {}
+
+ // Sink concept.
+ public:
+
+ typedef char char_type;
+
+ std::streamsize write(const char* buffer, std::streamsize buffer_size)
+ {
+ namespace python = boost::python;
+ // Copy the buffer to a python string.
+ python::str data(buffer, buffer_size);
+
+ // Invoke write on the python object, passing in the data. The following
+ // is equivalent to:
+ // n = object_.write(data)
+ python::extract<std::streamsize> bytes_written(
+ object_.attr("write")(data));
+
+ // Per the Sink concept, return the number of bytes written. If the
+ // Python return value provides a numeric result, then use it. Otherwise,
+ // such as the case of a File object, use the buffer_size.
+ return bytes_written.check()
+ ? bytes_written
+ : buffer_size;
+ }
+
+ // Flushable concept.
+ public:
+
+ bool flush()
+ {
+ // If flush exists, then call it.
+ boost::python::object flush = object_.attr("flush");
+ if (!flush.is_none())
+ {
+ flush();
+ }
+
+ // Always return true. If an error occurs, an exception should be thrown.
+ return true;
+ }
+
+ private:
+ boost::python::object object_;
+ };
+
+ /// @brief Use an auxiliary function to adapt the legacy function.
+ void log_to_stream(boost::python::object object)
+ {
+ // Create an ostream that delegates to the python object.
+ boost::iostreams::stream<PythonOutputDevice>* output = new boost::iostreams::stream<PythonOutputDevice>(object);
+ Yosys::log_streams.insert(Yosys::log_streams.begin(), output);
+ };
+
+
BOOST_PYTHON_MODULE(libyosys)
{
using namespace boost::python;
class_<Initializer>("Initializer");
scope().attr("_hidden") = new Initializer();
+
+ def("log_to_stream", &log_to_stream);
""")
for enum in enums:
@@ -2086,6 +2361,11 @@ namespace YOSYS_PYTHON {
for fun in unowned_functions:
wrapper_file.write(fun.gen_boost_py())
+ wrapper_file.write("\n\n\t\tclass_<YosysStatics>(\"Yosys\")\n")
+ for glbl in glbls:
+ wrapper_file.write(glbl.gen_boost_py())
+ wrapper_file.write("\t\t;\n")
+
wrapper_file.write("\n\t}\n}\n#endif")
def print_includes():
diff --git a/passes/cmds/Makefile.inc b/passes/cmds/Makefile.inc
index cf9663d1d..c7edc30fb 100644
--- a/passes/cmds/Makefile.inc
+++ b/passes/cmds/Makefile.inc
@@ -5,6 +5,7 @@ OBJS += passes/cmds/design.o
OBJS += passes/cmds/select.o
OBJS += passes/cmds/show.o
OBJS += passes/cmds/rename.o
+OBJS += passes/cmds/autoname.o
OBJS += passes/cmds/connect.o
OBJS += passes/cmds/scatter.o
OBJS += passes/cmds/setundef.o
diff --git a/passes/cmds/autoname.cc b/passes/cmds/autoname.cc
new file mode 100644
index 000000000..4614a8153
--- /dev/null
+++ b/passes/cmds/autoname.cc
@@ -0,0 +1,134 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/yosys.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+int autoname_worker(Module *module)
+{
+ dict<Cell*, pair<int, IdString>> proposed_cell_names;
+ dict<Wire*, pair<int, IdString>> proposed_wire_names;
+ dict<Wire*, int> wire_score;
+ int best_score = -1;
+
+ for (auto cell : module->selected_cells())
+ for (auto &conn : cell->connections())
+ for (auto bit : conn.second)
+ if (bit.wire != nullptr)
+ wire_score[bit.wire]++;
+
+ for (auto cell : module->selected_cells()) {
+ if (cell->name[0] == '$') {
+ for (auto &conn : cell->connections()) {
+ string suffix = stringf("_%s_%s", log_id(cell->type), log_id(conn.first));
+ for (auto bit : conn.second)
+ if (bit.wire != nullptr && bit.wire->name[0] != '$') {
+ IdString new_name(bit.wire->name.str() + suffix);
+ int score = wire_score.at(bit.wire);
+ if (cell->output(conn.first)) score = 0;
+ score = 10000*score + new_name.size();
+ if (!proposed_cell_names.count(cell) || score < proposed_cell_names.at(cell).first) {
+ if (best_score < 0 || score < best_score)
+ best_score = score;
+ proposed_cell_names[cell] = make_pair(score, new_name);
+ }
+ }
+ }
+ } else {
+ for (auto &conn : cell->connections()) {
+ string suffix = stringf("_%s", log_id(conn.first));
+ for (auto bit : conn.second)
+ if (bit.wire != nullptr && bit.wire->name[0] == '$') {
+ IdString new_name(cell->name.str() + suffix);
+ int score = wire_score.at(bit.wire);
+ if (cell->output(conn.first)) score = 0;
+ score = 10000*score + new_name.size();
+ if (!proposed_wire_names.count(bit.wire) || score < proposed_wire_names.at(bit.wire).first) {
+ if (best_score < 0 || score < best_score)
+ best_score = score;
+ proposed_wire_names[bit.wire] = make_pair(score, new_name);
+ }
+ }
+ }
+ }
+ }
+
+ for (auto &it : proposed_cell_names) {
+ if (best_score*2 < it.second.first)
+ continue;
+ IdString n = module->uniquify(it.second.second);
+ log_debug("Rename cell %s in %s to %s.\n", log_id(it.first), log_id(module), log_id(n));
+ module->rename(it.first, n);
+ }
+
+ for (auto &it : proposed_wire_names) {
+ if (best_score*2 < it.second.first)
+ continue;
+ IdString n = module->uniquify(it.second.second);
+ log_debug("Rename wire %s in %s to %s.\n", log_id(it.first), log_id(module), log_id(n));
+ module->rename(it.first, n);
+ }
+
+ return proposed_cell_names.size() + proposed_wire_names.size();
+}
+
+struct AutonamePass : public Pass {
+ AutonamePass() : Pass("autoname", "automatically assign names to objects") { }
+ void help() YS_OVERRIDE
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" autoname [selection]\n");
+ log("\n");
+ log("Assign auto-generated public names to objects with private names (the ones\n");
+ log("with $-prefix).\n");
+ log("\n");
+ }
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+ {
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ // if (args[argidx] == "-foo") {
+ // foo = true;
+ // continue;
+ // }
+ break;
+ }
+
+ log_header(design, "Executing AUTONAME pass.\n");
+
+ for (auto module : design->selected_modules())
+ {
+ int count = 0, iter = 0;
+ while (1) {
+ iter++;
+ int n = autoname_worker(module);
+ if (!n) break;
+ count += n;
+ }
+ if (count > 0)
+ log("Renamed %d objects in module %s (%d iterations).\n", count, log_id(module), iter);
+ }
+ }
+} AutonamePass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc
index 5ae991b28..fb3896669 100644
--- a/passes/fsm/fsm_detect.cc
+++ b/passes/fsm/fsm_detect.cc
@@ -158,22 +158,25 @@ static void detect_fsm(RTLIL::Wire *wire)
std::set<sig2driver_entry_t> cellport_list;
sig2user.find(sig_q, cellport_list);
+ auto sig_q_bits = sig_q.to_sigbit_pool();
+
for (auto &cellport : cellport_list)
{
RTLIL::Cell *cell = cellport.first;
bool set_output = false, clr_output = false;
- if (cell->type == "$ne")
+ if (cell->type.in("$ne", "$reduce_or", "$reduce_bool"))
set_output = true;
- if (cell->type == "$eq")
+ if (cell->type.in("$eq", "$logic_not", "$reduce_and"))
clr_output = true;
- if (!set_output && !clr_output) {
- clr_output = true;
+ if (set_output || clr_output) {
for (auto &port_it : cell->connections())
- if (port_it.first != "\\A" || port_it.first != "\\Y")
- clr_output = false;
+ if (cell->input(port_it.first))
+ for (auto bit : assign_map(port_it.second))
+ if (bit.wire != nullptr && !sig_q_bits.count(bit))
+ goto next_cellport;
}
if (set_output || clr_output) {
@@ -184,6 +187,7 @@ static void detect_fsm(RTLIL::Wire *wire)
ce.set(sig, val);
}
}
+ next_cellport:;
}
SigSpec sig_y = sig_d, sig_undef;
diff --git a/passes/techmap/flowmap.cc b/passes/techmap/flowmap.cc
index 5807178dd..a2ad87f7d 100644
--- a/passes/techmap/flowmap.cc
+++ b/passes/techmap/flowmap.cc
@@ -394,7 +394,7 @@ struct FlowGraph
pair<pool<RTLIL::SigBit>, pool<RTLIL::SigBit>> edge_cut()
{
- pool<RTLIL::SigBit> x, xi;
+ pool<RTLIL::SigBit> x = {source}, xi; // X and X̅ in the paper
NodePrime source_prime = {source, true};
pool<NodePrime> visited;
@@ -437,6 +437,7 @@ struct FlowGraph
for (auto collapsed_node : collapsed[sink])
xi.insert(collapsed_node);
+ log_assert(x[source] && !xi[source]);
log_assert(!x[sink] && xi[sink]);
return {x, xi};
}
@@ -1050,7 +1051,7 @@ struct FlowmapWorker
auto cut_inputs = cut_lut_at_gate(lut, lut_gate);
pool<RTLIL::SigBit> gate_inputs = cut_inputs.first, other_inputs = cut_inputs.second;
- if (gate_inputs.empty() && (int)other_inputs.size() == order)
+ if (gate_inputs.empty() && (int)other_inputs.size() >= order)
{
if (debug_relax)
log(" Breaking would result in a (k+1)-LUT.\n");
diff --git a/techlibs/common/cmp2lut.v b/techlibs/common/cmp2lut.v
index 0d0757767..1c8192b85 100644
--- a/techlibs/common/cmp2lut.v
+++ b/techlibs/common/cmp2lut.v
@@ -7,7 +7,7 @@
// with n <= k inputs should be techmapped in this way, because this shortens the critical path
// from n to 1 by avoiding carry chains.
-(* techmap_celltype = "$eq $ne $lt $le $gt $ge" *)
+(* techmap_celltype = "$lt $le $gt $ge" *)
module _90_lut_cmp_ (A, B, Y);
parameter A_SIGNED = 0;
diff --git a/techlibs/ecp5/synth_ecp5.cc b/techlibs/ecp5/synth_ecp5.cc
index 800a8ce22..4cbb56ea1 100644
--- a/techlibs/ecp5/synth_ecp5.cc
+++ b/techlibs/ecp5/synth_ecp5.cc
@@ -339,6 +339,7 @@ struct SynthEcp5Pass : public ScriptPass
if (check_label("check"))
{
+ run("autoname");
run("hierarchy -check");
run("stat");
run("check -noinit");
diff --git a/techlibs/ice40/cells_sim.v b/techlibs/ice40/cells_sim.v
index f9e79a61d..7d1b37fd6 100644
--- a/techlibs/ice40/cells_sim.v
+++ b/techlibs/ice40/cells_sim.v
@@ -1,4 +1,4 @@
-
+`timescale 1ps / 1ps
`define SB_DFF_REG reg Q = 0
// `define SB_DFF_REG reg Q
@@ -81,6 +81,37 @@ module SB_IO (
if (PIN_TYPE[5:4] == 2'b11) assign PACKAGE_PIN = outena_q ? dout : 1'bz;
endgenerate
`endif
+`ifdef TIMING
+specify
+ (INPUT_CLK => D_IN_0) = (0:0:0, 0:0:0);
+ (INPUT_CLK => D_IN_1) = (0:0:0, 0:0:0);
+ (PACKAGE_PIN => D_IN_0) = (0:0:0, 0:0:0);
+ (OUTPUT_CLK => PACKAGE_PIN) = (0:0:0, 0:0:0);
+ (D_OUT_0 => PACKAGE_PIN) = (0:0:0, 0:0:0);
+ (OUTPUT_ENABLE => PACKAGE_PIN) = (0:0:0, 0:0:0);
+
+ $setuphold(posedge OUTPUT_CLK, posedge D_OUT_0, 0:0:0, 0:0:0);
+ $setuphold(posedge OUTPUT_CLK, negedge D_OUT_0, 0:0:0, 0:0:0);
+ $setuphold(negedge OUTPUT_CLK, posedge D_OUT_1, 0:0:0, 0:0:0);
+ $setuphold(negedge OUTPUT_CLK, negedge D_OUT_1, 0:0:0, 0:0:0);
+ $setuphold(negedge OUTPUT_CLK, posedge D_OUT_0, 0:0:0, 0:0:0);
+ $setuphold(negedge OUTPUT_CLK, negedge D_OUT_0, 0:0:0, 0:0:0);
+ $setuphold(posedge OUTPUT_CLK, posedge D_OUT_1, 0:0:0, 0:0:0);
+ $setuphold(posedge OUTPUT_CLK, negedge D_OUT_1, 0:0:0, 0:0:0);
+ $setuphold(posedge INPUT_CLK, posedge CLOCK_ENABLE, 0:0:0, 0:0:0);
+ $setuphold(posedge INPUT_CLK, negedge CLOCK_ENABLE, 0:0:0, 0:0:0);
+ $setuphold(posedge OUTPUT_CLK, posedge CLOCK_ENABLE, 0:0:0, 0:0:0);
+ $setuphold(posedge OUTPUT_CLK, negedge CLOCK_ENABLE, 0:0:0, 0:0:0);
+ $setuphold(posedge INPUT_CLK, posedge PACKAGE_PIN, 0:0:0, 0:0:0);
+ $setuphold(posedge INPUT_CLK, negedge PACKAGE_PIN, 0:0:0, 0:0:0);
+ $setuphold(negedge INPUT_CLK, posedge PACKAGE_PIN, 0:0:0, 0:0:0);
+ $setuphold(negedge INPUT_CLK, negedge PACKAGE_PIN, 0:0:0, 0:0:0);
+ $setuphold(posedge OUTPUT_CLK, posedge OUTPUT_ENABLE, 0:0:0, 0:0:0);
+ $setuphold(posedge OUTPUT_CLK, negedge OUTPUT_ENABLE, 0:0:0, 0:0:0);
+ $setuphold(negedge OUTPUT_CLK, posedge OUTPUT_ENABLE, 0:0:0, 0:0:0);
+ $setuphold(negedge OUTPUT_CLK, negedge OUTPUT_ENABLE, 0:0:0, 0:0:0);
+endspecify
+`endif
endmodule
module SB_GB_IO (
@@ -127,6 +158,11 @@ module SB_GB (
output GLOBAL_BUFFER_OUTPUT
);
assign GLOBAL_BUFFER_OUTPUT = USER_SIGNAL_TO_GLOBAL_BUFFER;
+`ifdef TIMING
+specify
+ (USER_SIGNAL_TO_GLOBAL_BUFFER => GLOBAL_BUFFER_OUTPUT) = (0:0:0, 0:0:0);
+endspecify
+`endif
endmodule
// SiliconBlue Logic Cells
@@ -830,33 +866,81 @@ module ICESTORM_LC (
parameter [0:0] CIN_CONST = 0;
parameter [0:0] CIN_SET = 0;
+ wire I0_pd = (I0 === 1'bz) ? 1'b0 : I0;
+ wire I1_pd = (I1 === 1'bz) ? 1'b0 : I1;
+ wire I2_pd = (I2 === 1'bz) ? 1'b0 : I2;
+ wire I3_pd = (I3 === 1'bz) ? 1'b0 : I3;
+ wire SR_pd = (SR === 1'bz) ? 1'b0 : SR;
+ wire CEN_pu = (CEN === 1'bz) ? 1'b1 : CEN;
+
wire mux_cin = CIN_CONST ? CIN_SET : CIN;
- assign COUT = CARRY_ENABLE ? (I1 && I2) || ((I1 || I2) && mux_cin) : 1'bx;
+ assign COUT = CARRY_ENABLE ? (I1_pd && I2_pd) || ((I1_pd || I2_pd) && mux_cin) : 1'bx;
- wire [7:0] lut_s3 = I3 ? LUT_INIT[15:8] : LUT_INIT[7:0];
- wire [3:0] lut_s2 = I2 ? lut_s3[ 7:4] : lut_s3[3:0];
- wire [1:0] lut_s1 = I1 ? lut_s2[ 3:2] : lut_s2[1:0];
- wire lut_o = I0 ? lut_s1[ 1] : lut_s1[ 0];
+ wire [7:0] lut_s3 = I3_pd ? LUT_INIT[15:8] : LUT_INIT[7:0];
+ wire [3:0] lut_s2 = I2_pd ? lut_s3[ 7:4] : lut_s3[3:0];
+ wire [1:0] lut_s1 = I1_pd ? lut_s2[ 3:2] : lut_s2[1:0];
+ wire lut_o = I0_pd ? lut_s1[ 1] : lut_s1[ 0];
assign LO = lut_o;
wire polarized_clk;
assign polarized_clk = CLK ^ NEG_CLK;
- reg o_reg;
+ reg o_reg = 1'b0;
always @(posedge polarized_clk)
- if (CEN)
- o_reg <= SR ? SET_NORESET : lut_o;
+ if (CEN_pu)
+ o_reg <= SR_pd ? SET_NORESET : lut_o;
- reg o_reg_async;
+ reg o_reg_async = 1'b0;
always @(posedge polarized_clk, posedge SR)
- if (SR)
- o_reg <= SET_NORESET;
- else if (CEN)
- o_reg <= lut_o;
+ if (SR_pd)
+ o_reg_async <= SET_NORESET;
+ else if (CEN_pu)
+ o_reg_async <= lut_o;
assign O = DFF_ENABLE ? ASYNC_SR ? o_reg_async : o_reg : lut_o;
+`ifdef TIMING
+specify
+ (I0 => O) = (0:0:0, 0:0:0);
+ (I1 => O) = (0:0:0, 0:0:0);
+ (I2 => O) = (0:0:0, 0:0:0);
+ (I3 => O) = (0:0:0, 0:0:0);
+ (I0 => LO) = (0:0:0, 0:0:0);
+ (I1 => LO) = (0:0:0, 0:0:0);
+ (I2 => LO) = (0:0:0, 0:0:0);
+ (I3 => LO) = (0:0:0, 0:0:0);
+ (I1 => COUT) = (0:0:0, 0:0:0);
+ (I2 => COUT) = (0:0:0, 0:0:0);
+ (CIN => COUT) = (0:0:0, 0:0:0);
+ (CLK => O) = (0:0:0, 0:0:0);
+ (SR => O) = (0:0:0, 0:0:0);
+ $setuphold(posedge CLK, posedge I0, 0:0:0, 0:0:0);
+ $setuphold(posedge CLK, negedge I0, 0:0:0, 0:0:0);
+ $setuphold(negedge CLK, posedge I0, 0:0:0, 0:0:0);
+ $setuphold(negedge CLK, negedge I0, 0:0:0, 0:0:0);
+ $setuphold(posedge CLK, posedge I1, 0:0:0, 0:0:0);
+ $setuphold(posedge CLK, negedge I1, 0:0:0, 0:0:0);
+ $setuphold(negedge CLK, posedge I1, 0:0:0, 0:0:0);
+ $setuphold(negedge CLK, negedge I1, 0:0:0, 0:0:0);
+ $setuphold(posedge CLK, posedge I2, 0:0:0, 0:0:0);
+ $setuphold(posedge CLK, negedge I2, 0:0:0, 0:0:0);
+ $setuphold(negedge CLK, posedge I2, 0:0:0, 0:0:0);
+ $setuphold(negedge CLK, negedge I2, 0:0:0, 0:0:0);
+ $setuphold(posedge CLK, posedge I3, 0:0:0, 0:0:0);
+ $setuphold(posedge CLK, negedge I3, 0:0:0, 0:0:0);
+ $setuphold(negedge CLK, posedge I3, 0:0:0, 0:0:0);
+ $setuphold(negedge CLK, negedge I3, 0:0:0, 0:0:0);
+ $setuphold(posedge CLK, posedge CEN, 0:0:0, 0:0:0);
+ $setuphold(posedge CLK, negedge CEN, 0:0:0, 0:0:0);
+ $setuphold(negedge CLK, posedge CEN, 0:0:0, 0:0:0);
+ $setuphold(negedge CLK, negedge CEN, 0:0:0, 0:0:0);
+ $setuphold(posedge CLK, posedge SR, 0:0:0, 0:0:0);
+ $setuphold(posedge CLK, negedge SR, 0:0:0, 0:0:0);
+ $setuphold(negedge CLK, posedge SR, 0:0:0, 0:0:0);
+ $setuphold(negedge CLK, negedge SR, 0:0:0, 0:0:0);
+endspecify
+`endif
endmodule
// SiliconBlue PLL Cells
@@ -1576,3 +1660,341 @@ module SB_MAC16 (
assign LCI = (BOTADDSUB_CARRYSELECT == 0) ? 1'b0 : (BOTADDSUB_CARRYSELECT == 1) ? 1'b1 : (BOTADDSUB_CARRYSELECT == 2) ? ACCUMCI : CI;
assign O = {Oh, Ol};
endmodule
+
+// Post-place-and-route RAM model
+module ICESTORM_RAM(
+ output RDATA_15, RDATA_14, RDATA_13, RDATA_12, RDATA_11, RDATA_10, RDATA_9, RDATA_8, RDATA_7, RDATA_6, RDATA_5, RDATA_4, RDATA_3, RDATA_2, RDATA_1, RDATA_0,
+ input RCLK, RCLKE, RE,
+ input RADDR_10, RADDR_9, RADDR_8, RADDR_7, RADDR_6, RADDR_5, RADDR_4, RADDR_3, RADDR_2, RADDR_1, RADDR_0,
+ input WCLK, WCLKE, WE,
+ input WADDR_10, WADDR_9, WADDR_8, WADDR_7, WADDR_6, WADDR_5, WADDR_4, WADDR_3, WADDR_2, WADDR_1, WADDR_0,
+ input MASK_15, MASK_14, MASK_13, MASK_12, MASK_11, MASK_10, MASK_9, MASK_8, MASK_7, MASK_6, MASK_5, MASK_4, MASK_3, MASK_2, MASK_1, MASK_0,
+ input WDATA_15, WDATA_14, WDATA_13, WDATA_12, WDATA_11, WDATA_10, WDATA_9, WDATA_8, WDATA_7, WDATA_6, WDATA_5, WDATA_4, WDATA_3, WDATA_2, WDATA_1, WDATA_0
+);
+ parameter WRITE_MODE = 0;
+ parameter READ_MODE = 0;
+
+ parameter NEG_CLK_R = 1'b0;
+ parameter NEG_CLK_W = 1'b0;
+
+ parameter INIT_0 = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+ parameter INIT_1 = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+ parameter INIT_2 = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+ parameter INIT_3 = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+ parameter INIT_4 = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+ parameter INIT_5 = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+ parameter INIT_6 = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+ parameter INIT_7 = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+ parameter INIT_8 = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+ parameter INIT_9 = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+ parameter INIT_A = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+ parameter INIT_B = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+ parameter INIT_C = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+ parameter INIT_D = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+ parameter INIT_E = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+ parameter INIT_F = 256'h0000000000000000000000000000000000000000000000000000000000000000;
+
+ // Pull-down and pull-up functions
+ function pd;
+ input x;
+ begin
+ pd = (x === 1'bz) ? 1'b0 : x;
+ end
+ endfunction
+
+ function pu;
+ input x;
+ begin
+ pu = (x === 1'bz) ? 1'b1 : x;
+ end
+ endfunction
+
+ SB_RAM40_4K #(
+ .WRITE_MODE(WRITE_MODE),
+ .READ_MODE (READ_MODE ),
+ .INIT_0 (INIT_0 ),
+ .INIT_1 (INIT_1 ),
+ .INIT_2 (INIT_2 ),
+ .INIT_3 (INIT_3 ),
+ .INIT_4 (INIT_4 ),
+ .INIT_5 (INIT_5 ),
+ .INIT_6 (INIT_6 ),
+ .INIT_7 (INIT_7 ),
+ .INIT_8 (INIT_8 ),
+ .INIT_9 (INIT_9 ),
+ .INIT_A (INIT_A ),
+ .INIT_B (INIT_B ),
+ .INIT_C (INIT_C ),
+ .INIT_D (INIT_D ),
+ .INIT_E (INIT_E ),
+ .INIT_F (INIT_F )
+ ) RAM (
+ .RDATA({RDATA_15, RDATA_14, RDATA_13, RDATA_12, RDATA_11, RDATA_10, RDATA_9, RDATA_8, RDATA_7, RDATA_6, RDATA_5, RDATA_4, RDATA_3, RDATA_2, RDATA_1, RDATA_0}),
+ .RCLK (pd(RCLK) ^ NEG_CLK_R),
+ .RCLKE(pu(RCLKE)),
+ .RE (pd(RE)),
+ .RADDR({pd(RADDR_10), pd(RADDR_9), pd(RADDR_8), pd(RADDR_7), pd(RADDR_6), pd(RADDR_5), pd(RADDR_4), pd(RADDR_3), pd(RADDR_2), pd(RADDR_1), pd(RADDR_0)}),
+ .WCLK (pd(WCLK) ^ NEG_CLK_W),
+ .WCLKE(pu(WCLKE)),
+ .WE (pd(WE)),
+ .WADDR({pd(WADDR_10), pd(WADDR_9), pd(WADDR_8), pd(WADDR_7), pd(WADDR_6), pd(WADDR_5), pd(WADDR_4), pd(WADDR_3), pd(WADDR_2), pd(WADDR_1), pd(WADDR_0)}),
+ .MASK ({pd(MASK_15), pd(MASK_14), pd(MASK_13), pd(MASK_12), pd(MASK_11), pd(MASK_10), pd(MASK_9), pd(MASK_8),
+ pd(MASK_7), pd(MASK_6), pd(MASK_5), pd(MASK_4), pd(MASK_3), pd(MASK_2), pd(MASK_1), pd(MASK_0)}),
+ .WDATA({pd(WDATA_15), pd(WDATA_14), pd(WDATA_13), pd(WDATA_12), pd(WDATA_11), pd(WDATA_10), pd(WDATA_9), pd(WDATA_8),
+ pd(WDATA_7), pd(WDATA_6), pd(WDATA_5), pd(WDATA_4), pd(WDATA_3), pd(WDATA_2), pd(WDATA_1), pd(WDATA_0)})
+ );
+
+`ifdef TIMING
+specify
+ (RCLK => RDATA_15) = (0:0:0, 0:0:0);
+ (RCLK => RDATA_14) = (0:0:0, 0:0:0);
+ (RCLK => RDATA_13) = (0:0:0, 0:0:0);
+ (RCLK => RDATA_12) = (0:0:0, 0:0:0);
+ (RCLK => RDATA_11) = (0:0:0, 0:0:0);
+ (RCLK => RDATA_10) = (0:0:0, 0:0:0);
+ (RCLK => RDATA_9) = (0:0:0, 0:0:0);
+ (RCLK => RDATA_8) = (0:0:0, 0:0:0);
+ (RCLK => RDATA_7) = (0:0:0, 0:0:0);
+ (RCLK => RDATA_6) = (0:0:0, 0:0:0);
+ (RCLK => RDATA_5) = (0:0:0, 0:0:0);
+ (RCLK => RDATA_4) = (0:0:0, 0:0:0);
+ (RCLK => RDATA_3) = (0:0:0, 0:0:0);
+ (RCLK => RDATA_2) = (0:0:0, 0:0:0);
+ (RCLK => RDATA_1) = (0:0:0, 0:0:0);
+ (RCLK => RDATA_0) = (0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, posedge RCLKE, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, negedge RCLKE, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, posedge RCLKE, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, negedge RCLKE, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, posedge RE, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, negedge RE, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, posedge RE, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, negedge RE, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, posedge RADDR_10, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, negedge RADDR_10, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, posedge RADDR_10, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, negedge RADDR_10, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, posedge RADDR_9, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, negedge RADDR_9, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, posedge RADDR_9, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, negedge RADDR_9, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, posedge RADDR_8, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, negedge RADDR_8, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, posedge RADDR_8, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, negedge RADDR_8, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, posedge RADDR_7, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, negedge RADDR_7, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, posedge RADDR_7, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, negedge RADDR_7, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, posedge RADDR_6, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, negedge RADDR_6, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, posedge RADDR_6, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, negedge RADDR_6, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, posedge RADDR_5, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, negedge RADDR_5, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, posedge RADDR_5, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, negedge RADDR_5, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, posedge RADDR_4, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, negedge RADDR_4, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, posedge RADDR_4, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, negedge RADDR_4, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, posedge RADDR_3, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, negedge RADDR_3, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, posedge RADDR_3, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, negedge RADDR_3, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, posedge RADDR_2, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, negedge RADDR_2, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, posedge RADDR_2, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, negedge RADDR_2, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, posedge RADDR_1, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, negedge RADDR_1, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, posedge RADDR_1, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, negedge RADDR_1, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, posedge RADDR_0, 0:0:0, 0:0:0);
+ $setuphold(posedge RCLK, negedge RADDR_0, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, posedge RADDR_0, 0:0:0, 0:0:0);
+ $setuphold(negedge RCLK, negedge RADDR_0, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WCLKE, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WCLKE, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WCLKE, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WCLKE, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WE, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WE, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WE, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WE, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WADDR_10, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WADDR_10, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WADDR_10, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WADDR_10, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WADDR_9, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WADDR_9, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WADDR_9, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WADDR_9, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WADDR_8, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WADDR_8, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WADDR_8, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WADDR_8, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WADDR_7, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WADDR_7, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WADDR_7, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WADDR_7, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WADDR_6, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WADDR_6, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WADDR_6, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WADDR_6, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WADDR_5, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WADDR_5, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WADDR_5, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WADDR_5, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WADDR_4, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WADDR_4, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WADDR_4, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WADDR_4, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WADDR_3, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WADDR_3, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WADDR_3, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WADDR_3, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WADDR_2, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WADDR_2, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WADDR_2, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WADDR_2, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WADDR_1, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WADDR_1, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WADDR_1, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WADDR_1, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WADDR_0, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WADDR_0, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WADDR_0, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WADDR_0, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_15, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_15, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_15, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_15, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_14, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_14, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_14, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_14, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_13, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_13, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_13, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_13, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_12, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_12, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_12, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_12, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_11, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_11, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_11, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_11, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_10, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_10, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_10, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_10, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_9, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_9, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_9, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_9, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_8, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_8, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_8, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_8, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_7, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_7, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_7, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_7, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_6, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_6, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_6, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_6, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_5, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_5, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_5, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_5, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_4, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_4, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_4, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_4, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_3, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_3, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_3, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_3, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_2, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_2, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_2, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_2, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_1, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_1, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_1, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_1, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge MASK_0, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge MASK_0, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge MASK_0, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge MASK_0, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_15, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_15, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_15, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_15, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_14, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_14, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_14, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_14, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_13, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_13, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_13, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_13, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_12, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_12, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_12, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_12, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_11, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_11, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_11, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_11, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_10, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_10, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_10, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_10, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_9, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_9, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_9, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_9, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_8, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_8, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_8, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_8, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_7, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_7, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_7, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_7, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_6, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_6, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_6, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_6, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_5, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_5, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_5, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_5, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_4, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_4, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_4, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_4, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_3, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_3, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_3, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_3, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_2, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_2, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_2, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_2, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_1, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_1, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_1, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_1, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, posedge WDATA_0, 0:0:0, 0:0:0);
+ $setuphold(posedge WCLK, negedge WDATA_0, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, posedge WDATA_0, 0:0:0, 0:0:0);
+ $setuphold(negedge WCLK, negedge WDATA_0, 0:0:0, 0:0:0);
+
+endspecify
+`endif
+endmodule
diff --git a/techlibs/ice40/synth_ice40.cc b/techlibs/ice40/synth_ice40.cc
index c942126e1..901194b06 100644
--- a/techlibs/ice40/synth_ice40.cc
+++ b/techlibs/ice40/synth_ice40.cc
@@ -380,6 +380,7 @@ struct SynthIce40Pass : public ScriptPass
if (check_label("check"))
{
+ run("autoname");
run("hierarchy -check");
run("stat");
run("check -noinit");
diff --git a/tests/arch/anlogic/fsm.ys b/tests/arch/anlogic/fsm.ys
index f45951b13..0bcc4e011 100644
--- a/tests/arch/anlogic/fsm.ys
+++ b/tests/arch/anlogic/fsm.ys
@@ -1,12 +1,15 @@
read_verilog ../common/fsm.v
hierarchy -top fsm
proc
-#flatten
-#ERROR: Found 4 unproven $equiv cells in 'equiv_status -assert'.
-#equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # equivalency check
-equiv_opt -map +/anlogic/cells_sim.v synth_anlogic # equivalency check
+flatten
+
+equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
+
select -assert-count 1 t:AL_MAP_LUT2
select -assert-count 5 t:AL_MAP_LUT5
select -assert-count 1 t:AL_MAP_LUT6
diff --git a/tests/arch/ecp5/fsm.ys b/tests/arch/ecp5/fsm.ys
index f834a4c6b..ba91e5fc0 100644
--- a/tests/arch/ecp5/fsm.ys
+++ b/tests/arch/ecp5/fsm.ys
@@ -2,11 +2,16 @@ read_verilog ../common/fsm.v
hierarchy -top fsm
proc
flatten
-equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
+
+equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
+
select -assert-count 1 t:L6MUX21
-select -assert-count 13 t:LUT4
-select -assert-count 5 t:PFUMX
-select -assert-count 5 t:TRELLIS_FF
+select -assert-count 15 t:LUT4
+select -assert-count 6 t:PFUMX
+select -assert-count 6 t:TRELLIS_FF
select -assert-none t:L6MUX21 t:LUT4 t:PFUMX t:TRELLIS_FF %% t:* %D
diff --git a/tests/arch/efinix/fsm.ys b/tests/arch/efinix/fsm.ys
index a8ba70fdb..a2db2ad98 100644
--- a/tests/arch/efinix/fsm.ys
+++ b/tests/arch/efinix/fsm.ys
@@ -2,9 +2,11 @@ read_verilog ../common/fsm.v
hierarchy -top fsm
proc
flatten
-#ERROR: Found 4 unproven $equiv cells in 'equiv_status -assert'.
-#equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check
-equiv_opt -map +/efinix/cells_sim.v synth_efinix # equivalency check
+
+equiv_opt -run :prove -map +/efinix/cells_sim.v synth_efinix
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
diff --git a/tests/arch/ice40/fsm.ys b/tests/arch/ice40/fsm.ys
index 5aacc6c73..223ba070e 100644
--- a/tests/arch/ice40/fsm.ys
+++ b/tests/arch/ice40/fsm.ys
@@ -2,12 +2,15 @@ read_verilog ../common/fsm.v
hierarchy -top fsm
proc
flatten
-equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
+
+equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
+select -assert-count 4 t:SB_DFF
select -assert-count 2 t:SB_DFFESR
-select -assert-count 2 t:SB_DFFSR
-select -assert-count 1 t:SB_DFFSS
-select -assert-count 13 t:SB_LUT4
-select -assert-none t:SB_DFFESR t:SB_DFFSR t:SB_DFFSS t:SB_LUT4 %% t:* %D
+select -assert-count 15 t:SB_LUT4
+select -assert-none t:SB_DFFESR t:SB_DFF t:SB_LUT4 %% t:* %D
diff --git a/tests/arch/xilinx/fsm.ys b/tests/arch/xilinx/fsm.ys
index d2b481421..2a72c34e8 100644
--- a/tests/arch/xilinx/fsm.ys
+++ b/tests/arch/xilinx/fsm.ys
@@ -2,7 +2,11 @@ read_verilog ../common/fsm.v
hierarchy -top fsm
proc
flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module