mirror of https://github.com/YosysHQ/yosys.git
Merge branch 'master' of https://github.com/YosysHQ/yosys into gowin
This commit is contained in:
Pepijn de Vos
commit
32f0296df1
|
|
@ -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));
|
||||
|
|
|
|||
|
|
@ -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():
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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");
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -339,6 +339,7 @@ struct SynthEcp5Pass : public ScriptPass
|
|||
|
||||
if (check_label("check"))
|
||||
{
|
||||
run("autoname");
|
||||
run("hierarchy -check");
|
||||
run("stat");
|
||||
run("check -noinit");
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -380,6 +380,7 @@ struct SynthIce40Pass : public ScriptPass
|
|||
|
||||
if (check_label("check"))
|
||||
{
|
||||
run("autoname");
|
||||
run("hierarchy -check");
|
||||
run("stat");
|
||||
run("check -noinit");
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue