aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile19
-rw-r--r--backends/aiger/aiger.cc2
-rw-r--r--backends/aiger/xaiger.cc2
-rw-r--r--backends/edif/edif.cc8
-rw-r--r--backends/smt2/smt2.cc4
-rw-r--r--backends/verilog/verilog_backend.cc60
-rw-r--r--frontends/verific/verific.cc20
-rw-r--r--kernel/rtlil.h2
-rw-r--r--passes/cmds/rename.cc4
-rw-r--r--passes/cmds/show.cc2
-rw-r--r--passes/cmds/splice.cc2
-rw-r--r--passes/cmds/stat.cc2
-rw-r--r--passes/equiv/equiv_make.cc8
-rw-r--r--passes/equiv/equiv_purge.cc4
-rw-r--r--passes/hierarchy/hierarchy.cc12
-rw-r--r--passes/opt/opt_clean.cc4
-rw-r--r--passes/sat/mutate.cc6
-rw-r--r--passes/sat/sat.cc2
-rw-r--r--techlibs/xilinx/cells_sim.v81
-rw-r--r--techlibs/xilinx/xc7_dsp_map.v1
-rwxr-xr-xtests/aiger/run-test.sh2
-rw-r--r--tests/arch/xilinx/dsp_abc9.ys37
-rw-r--r--tests/verilog/.gitignore2
-rw-r--r--tests/verilog/const_arst.ys24
-rw-r--r--tests/verilog/const_sr.ys25
25 files changed, 268 insertions, 67 deletions
diff --git a/Makefile b/Makefile
index e4eec8abe..e22bc9bc3 100644
--- a/Makefile
+++ b/Makefile
@@ -123,7 +123,7 @@ LDFLAGS += -rdynamic
LDLIBS += -lrt
endif
-YOSYS_VER := 0.9+3578
+YOSYS_VER := 0.9+3599
GIT_REV := $(shell cd $(YOSYS_SRC) && git rev-parse --short HEAD 2> /dev/null || echo UNKNOWN)
OBJS = kernel/version_$(GIT_REV).o
@@ -171,8 +171,7 @@ else
PYTHON_CONFIG := $(PYTHON_EXECUTABLE)-config
endif
-PYTHON_PREFIX := $(shell $(PYTHON_CONFIG) --prefix)
-PYTHON_DESTDIR := $(PYTHON_PREFIX)/lib/python$(PYTHON_VERSION)/site-packages
+PYTHON_DESTDIR := $(shell $(PYTHON_EXECUTABLE) -c "import site; print(site.getsitepackages()[-1]);")
# Reload Makefile.conf to override python specific variables if defined
ifneq ($(wildcard Makefile.conf),)
@@ -686,7 +685,7 @@ endif
%.pyh: %.h
$(Q) mkdir -p $(dir $@)
- $(P) cat $< | grep -E -v "#[ ]*(include|error)" | $(LD) -x c++ -o $@ -E -P -
+ $(P) cat $< | grep -E -v "#[ ]*(include|error)" | $(LD) $(CXXFLAGS) -x c++ -o $@ -E -P -
ifeq ($(ENABLE_PYOSYS),1)
$(PY_WRAPPER_FILE).cc: misc/$(PY_GEN_SCRIPT).py $(PY_WRAP_INCLUDES)
@@ -846,9 +845,9 @@ ifeq ($(ENABLE_LIBYOSYS),1)
$(INSTALL_SUDO) cp libyosys.so $(DESTDIR)$(LIBDIR)/
$(INSTALL_SUDO) $(STRIP) -S $(DESTDIR)$(LIBDIR)/libyosys.so
ifeq ($(ENABLE_PYOSYS),1)
- $(INSTALL_SUDO) mkdir -p $(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys
- $(INSTALL_SUDO) cp libyosys.so $(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/libyosys.so
- $(INSTALL_SUDO) cp misc/__init__.py $(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/
+ $(INSTALL_SUDO) mkdir -p $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys
+ $(INSTALL_SUDO) cp libyosys.so $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/libyosys.so
+ $(INSTALL_SUDO) cp misc/__init__.py $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/
endif
endif
@@ -858,9 +857,9 @@ uninstall:
ifeq ($(ENABLE_LIBYOSYS),1)
$(INSTALL_SUDO) rm -vf $(DESTDIR)$(LIBDIR)/libyosys.so
ifeq ($(ENABLE_PYOSYS),1)
- $(INSTALL_SUDO) rm -vf $(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/libyosys.so
- $(INSTALL_SUDO) rm -vf $(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/__init__.py
- $(INSTALL_SUDO) rmdir $(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys
+ $(INSTALL_SUDO) rm -vf $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/libyosys.so
+ $(INSTALL_SUDO) rm -vf $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/__init__.py
+ $(INSTALL_SUDO) rmdir $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys
endif
endif
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 81a3f483b..476b30488 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -111,7 +111,7 @@ struct AigerWriter
// promote public wires
for (auto wire : module->wires())
- if (wire->name[0] == '\\')
+ if (wire->name.isPublic())
sigmap.add(wire);
// promote input wires
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index ef0103c17..27499b64a 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -146,7 +146,7 @@ struct XAigerWriter
// promote public wires
for (auto wire : module->wires())
- if (wire->name[0] == '\\')
+ if (wire->name.isPublic())
sigmap.add(wire);
// promote input wires
diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc
index 5e6becfd0..e0013238c 100644
--- a/backends/edif/edif.cc
+++ b/backends/edif/edif.cc
@@ -330,7 +330,7 @@ struct EdifBackend : public Backend {
}
*f << stringf("\n (property %s (string \"%d'h%s\"))", EDIF_DEF(name), GetSize(val.bits), hex_string.c_str());
}
- };
+ };
for (auto module : sorted_modules)
{
if (module->get_blackbox_attribute())
@@ -373,8 +373,8 @@ struct EdifBackend : public Backend {
}
{
- int c1 = w1->name[0] == '\\';
- int c2 = w2->name[0] == '\\';
+ int c1 = w1->name.isPublic();
+ int c2 = w2->name.isPublic();
if (c1 > c2) goto promote;
if (c1 < c2) goto nopromote;
@@ -524,7 +524,7 @@ struct EdifBackend : public Backend {
*f << stringf(" (portRef %c (instanceRef GND))\n", gndvccy ? 'Y' : 'G');
if (sig == RTLIL::State::S1)
*f << stringf(" (portRef %c (instanceRef VCC))\n", gndvccy ? 'Y' : 'P');
- }
+ }
*f << stringf(" )");
if (attr_properties && sig.wire != NULL)
for (auto &p : sig.wire->attributes)
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 4a53ce6d5..0b4e20ac6 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -822,7 +822,7 @@ struct Smt2Worker
for (auto bit : SigSpec(wire))
if (reg_bits.count(bit))
is_register = true;
- if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) {
+ if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) {
RTLIL::SigSpec sig = sigmap(wire);
std::vector<std::string> comments;
if (wire->port_input)
@@ -831,7 +831,7 @@ struct Smt2Worker
comments.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width));
if (is_register)
comments.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
- if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\'))
+ if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic()))
comments.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 372f68ea5..bf980129d 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -926,7 +926,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
{
SigSpec sig_d;
Const val_arst, val_srst;
- std::string reg_bit_name;
+ std::string reg_bit_name, sig_set_name, sig_clr_name, sig_arst_name;
if (chunky) {
reg_bit_name = stringf("%s[%d]", reg_name.c_str(), i);
if (ff.has_d)
@@ -941,6 +941,32 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
if (ff.has_srst)
val_srst = chunky ? ff.val_srst[i] : ff.val_srst;
+ // If there are constants in the sensitivity list, replace them with an intermediate wire
+ if (ff.has_sr) {
+ if (ff.sig_set[i].wire == NULL)
+ {
+ sig_set_name = next_auto_id();
+ f << stringf("%s" "wire %s = ", indent.c_str(), sig_set_name.c_str());
+ dump_const(f, ff.sig_set[i].data);
+ f << stringf(";\n");
+ }
+ if (ff.sig_clr[i].wire == NULL)
+ {
+ sig_clr_name = next_auto_id();
+ f << stringf("%s" "wire %s = ", indent.c_str(), sig_clr_name.c_str());
+ dump_const(f, ff.sig_clr[i].data);
+ f << stringf(";\n");
+ }
+ } else if (ff.has_arst) {
+ if (ff.sig_arst[i].wire == NULL)
+ {
+ sig_arst_name = next_auto_id();
+ f << stringf("%s" "wire %s = ", indent.c_str(), sig_arst_name.c_str());
+ dump_const(f, ff.sig_arst[i].data);
+ f << stringf(";\n");
+ }
+ }
+
dump_attributes(f, indent, cell->attributes);
if (ff.has_clk)
{
@@ -949,27 +975,47 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
dump_sigspec(f, ff.sig_clk);
if (ff.has_sr) {
f << stringf(", %sedge ", ff.pol_set ? "pos" : "neg");
- dump_sigspec(f, ff.sig_set[i]);
+ if (ff.sig_set[i].wire == NULL)
+ f << stringf("%s", sig_set_name.c_str());
+ else
+ dump_sigspec(f, ff.sig_set[i]);
+
f << stringf(", %sedge ", ff.pol_clr ? "pos" : "neg");
- dump_sigspec(f, ff.sig_clr[i]);
+ if (ff.sig_clr[i].wire == NULL)
+ f << stringf("%s", sig_clr_name.c_str());
+ else
+ dump_sigspec(f, ff.sig_clr[i]);
+
} else if (ff.has_arst) {
f << stringf(", %sedge ", ff.pol_arst ? "pos" : "neg");
- dump_sigspec(f, ff.sig_arst);
+ if (ff.sig_arst[i].wire == NULL)
+ f << stringf("%s", sig_arst_name.c_str());
+ else
+ dump_sigspec(f, ff.sig_arst);
}
f << stringf(")\n");
f << stringf("%s" " ", indent.c_str());
if (ff.has_sr) {
f << stringf("if (%s", ff.pol_clr ? "" : "!");
- dump_sigspec(f, ff.sig_clr[i]);
+ if (ff.sig_clr[i].wire == NULL)
+ f << stringf("%s", sig_clr_name.c_str());
+ else
+ dump_sigspec(f, ff.sig_clr[i]);
f << stringf(") %s <= 1'b0;\n", reg_bit_name.c_str());
f << stringf("%s" " else if (%s", indent.c_str(), ff.pol_set ? "" : "!");
- dump_sigspec(f, ff.sig_set[i]);
+ if (ff.sig_set[i].wire == NULL)
+ f << stringf("%s", sig_set_name.c_str());
+ else
+ dump_sigspec(f, ff.sig_set[i]);
f << stringf(") %s <= 1'b1;\n", reg_bit_name.c_str());
f << stringf("%s" " else ", indent.c_str());
} else if (ff.has_arst) {
f << stringf("if (%s", ff.pol_arst ? "" : "!");
- dump_sigspec(f, ff.sig_arst);
+ if (ff.sig_arst[i].wire == NULL)
+ f << stringf("%s", sig_arst_name.c_str());
+ else
+ dump_sigspec(f, ff.sig_arst);
f << stringf(") %s <= ", reg_bit_name.c_str());
dump_sigspec(f, val_arst);
f << stringf(";\n");
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 7bbda9d49..acb854a4d 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -21,6 +21,7 @@
#include "kernel/sigtools.h"
#include "kernel/celltypes.h"
#include "kernel/log.h"
+#include "libs/sha1/sha1.h"
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
@@ -864,6 +865,21 @@ void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates)
merge_past_ffs_clock(it.second, it.first.first, it.first.second);
}
+static std::string sha1_if_contain_spaces(std::string str)
+{
+ if(str.find_first_of(' ') != std::string::npos) {
+ std::size_t open = str.find_first_of('(');
+ std::size_t closed = str.find_last_of(')');
+ if (open != std::string::npos && closed != std::string::npos) {
+ std::string content = str.substr(open + 1, closed - open - 1);
+ return str.substr(0, open + 1) + sha1(content) + str.substr(closed);
+ } else {
+ return sha1(str);
+ }
+ }
+ return str;
+}
+
void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool norename)
{
std::string netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name();
@@ -877,7 +893,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
module_name += nl->Name();
module_name += ")";
}
- module_name = "\\" + module_name;
+ module_name = "\\" + sha1_if_contain_spaces(module_name);
}
netlist = nl;
@@ -1512,7 +1528,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
inst_type += inst->View()->Name();
inst_type += ")";
}
- inst_type = "\\" + inst_type;
+ inst_type = "\\" + sha1_if_contain_spaces(inst_type);
}
RTLIL::Cell *cell = module->addCell(inst_name, inst_type);
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index 6c561cb85..a03e8933c 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -375,6 +375,8 @@ namespace RTLIL
bool in(const char *rhs) const { return *this == rhs; }
bool in(const std::string &rhs) const { return *this == rhs; }
bool in(const pool<IdString> &rhs) const { return rhs.count(*this) != 0; }
+
+ bool isPublic() { return begins_with("\\"); }
};
namespace ID {
diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc
index 6326b4b15..f8fe715c8 100644
--- a/passes/cmds/rename.cc
+++ b/passes/cmds/rename.cc
@@ -290,11 +290,11 @@ struct RenamePass : public Pass {
dict<RTLIL::Cell *, IdString> new_cell_names;
for (auto wire : module->selected_wires())
- if (wire->name[0] == '\\' && wire->port_id == 0)
+ if (wire->name.isPublic() && wire->port_id == 0)
new_wire_names[wire] = NEW_ID;
for (auto cell : module->selected_cells())
- if (cell->name[0] == '\\')
+ if (cell->name.isPublic())
new_cell_names[cell] = NEW_ID;
for (auto &it : new_wire_names)
diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc
index a4ad861f6..0c96f8c5d 100644
--- a/passes/cmds/show.cc
+++ b/passes/cmds/show.cc
@@ -368,7 +368,7 @@ struct ShowWorker
const char *shape = "diamond";
if (wire->port_input || wire->port_output)
shape = "octagon";
- if (wire->name[0] == '\\') {
+ if (wire->name.isPublic()) {
fprintf(f, "n%d [ shape=%s, label=\"%s\", %s, fontcolor=\"black\" ];\n",
id2num(wire->name), shape, findLabel(wire->name.str()),
nextColor(RTLIL::SigSpec(wire), "color=\"black\"").c_str());
diff --git a/passes/cmds/splice.cc b/passes/cmds/splice.cc
index 20627d601..0f63b91c5 100644
--- a/passes/cmds/splice.cc
+++ b/passes/cmds/splice.cc
@@ -211,7 +211,7 @@ struct SpliceWorker
std::vector<Wire*> mod_wires = module->wires();
for (auto wire : mod_wires)
- if ((!no_outputs && wire->port_output) || (do_wires && wire->name[0] == '\\')) {
+ if ((!no_outputs && wire->port_output) || (do_wires && wire->name.isPublic())) {
if (!design->selected(module, wire))
continue;
RTLIL::SigSpec sig = sigmap(wire);
diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc
index ed51fdc24..0d84c73db 100644
--- a/passes/cmds/stat.cc
+++ b/passes/cmds/stat.cc
@@ -81,7 +81,7 @@ struct statdata_t
for (auto wire : mod->selected_wires())
{
- if (wire->name[0] == '\\') {
+ if (wire->name.isPublic()) {
num_pub_wires++;
num_pub_wire_bits += wire->width;
}
diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc
index 51b4ad0f1..6923ae3d0 100644
--- a/passes/equiv/equiv_make.cc
+++ b/passes/equiv/equiv_make.cc
@@ -114,25 +114,25 @@ struct EquivMakeWorker
Module *gate_clone = gate_mod->clone();
for (auto it : gold_clone->wires().to_vector()) {
- if ((it->name[0] == '\\' || inames) && blacklist_names.count(it->name) == 0)
+ if ((it->name.isPublic() || inames) && blacklist_names.count(it->name) == 0)
wire_names.insert(it->name);
gold_clone->rename(it, it->name.str() + "_gold");
}
for (auto it : gold_clone->cells().to_vector()) {
- if ((it->name[0] == '\\' || inames) && blacklist_names.count(it->name) == 0)
+ if ((it->name.isPublic() || inames) && blacklist_names.count(it->name) == 0)
cell_names.insert(it->name);
gold_clone->rename(it, it->name.str() + "_gold");
}
for (auto it : gate_clone->wires().to_vector()) {
- if ((it->name[0] == '\\' || inames) && blacklist_names.count(it->name) == 0)
+ if ((it->name.isPublic() || inames) && blacklist_names.count(it->name) == 0)
wire_names.insert(it->name);
gate_clone->rename(it, it->name.str() + "_gate");
}
for (auto it : gate_clone->cells().to_vector()) {
- if ((it->name[0] == '\\' || inames) && blacklist_names.count(it->name) == 0)
+ if ((it->name.isPublic() || inames) && blacklist_names.count(it->name) == 0)
cell_names.insert(it->name);
gate_clone->rename(it, it->name.str() + "_gate");
}
diff --git a/passes/equiv/equiv_purge.cc b/passes/equiv/equiv_purge.cc
index d15c8d183..a43ecec5a 100644
--- a/passes/equiv/equiv_purge.cc
+++ b/passes/equiv/equiv_purge.cc
@@ -35,7 +35,7 @@ struct EquivPurgeWorker
{
if (sig.is_wire()) {
Wire *wire = sig.as_wire();
- if (wire->name[0] == '\\') {
+ if (wire->name.isPublic()) {
if (!wire->port_output) {
log(" Module output: %s (%s)\n", log_signal(wire), log_id(cellname));
wire->port_output = true;
@@ -62,7 +62,7 @@ struct EquivPurgeWorker
{
if (sig.is_wire()) {
Wire *wire = sig.as_wire();
- if (wire->name[0] == '\\') {
+ if (wire->name.isPublic()) {
if (!wire->port_output) {
log(" Module input: %s\n", log_signal(wire));
wire->port_input = true;
diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index 90b25949d..225e1feae 100644
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -765,11 +765,13 @@ struct HierarchyPass : public Pass {
top_mod = design->module(top_name);
dict<RTLIL::IdString, RTLIL::Const> top_parameters;
- for (auto &para : parameters) {
- SigSpec sig_value;
- if (!RTLIL::SigSpec::parse(sig_value, NULL, para.second))
- log_cmd_error("Can't decode value '%s'!\n", para.second.c_str());
- top_parameters[RTLIL::escape_id(para.first)] = sig_value.as_const();
+ if ((top_mod == nullptr && design->module(abstract_id)) || top_mod != nullptr) {
+ for (auto &para : parameters) {
+ SigSpec sig_value;
+ if (!RTLIL::SigSpec::parse(sig_value, NULL, para.second))
+ log_cmd_error("Can't decode value '%s'!\n", para.second.c_str());
+ top_parameters[RTLIL::escape_id(para.first)] = sig_value.as_const();
+ }
}
if (top_mod == nullptr && design->module(abstract_id))
diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc
index 5370881d3..bd9856e81 100644
--- a/passes/opt/opt_clean.cc
+++ b/passes/opt/opt_clean.cc
@@ -207,7 +207,7 @@ bool compare_signals(RTLIL::SigBit &s1, RTLIL::SigBit &s2, SigPool &regs, SigPoo
if ((w1->port_input && w1->port_output) != (w2->port_input && w2->port_output))
return !(w2->port_input && w2->port_output);
- if (w1->name[0] == '\\' && w2->name[0] == '\\') {
+ if (w1->name.isPublic() && w2->name.isPublic()) {
if (regs.check(s1) != regs.check(s2))
return regs.check(s2);
if (direct_wires.count(w1) != direct_wires.count(w2))
@@ -220,7 +220,7 @@ bool compare_signals(RTLIL::SigBit &s1, RTLIL::SigBit &s2, SigPool &regs, SigPoo
return w2->port_output;
if (w1->name[0] != w2->name[0])
- return w2->name[0] == '\\';
+ return w2->name.isPublic();
int attrs1 = count_nontrivial_wire_attrs(w1);
int attrs2 = count_nontrivial_wire_attrs(w2);
diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc
index 15abee73e..95e0e0944 100644
--- a/passes/sat/mutate.cc
+++ b/passes/sat/mutate.cc
@@ -439,7 +439,7 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena
dict<SigBit, int> bit_user_cnt;
for (auto wire : module->wires()) {
- if (wire->name[0] == '\\' && wire->attributes.count(ID::src))
+ if (wire->name.isPublic() && wire->attributes.count(ID::src))
sigmap.add(wire);
}
@@ -468,7 +468,7 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena
}
if (!bit.wire->name[0] != !sigbit.wire->name[0]) {
- if (bit.wire->name[0] == '\\')
+ if (bit.wire->name.isPublic())
sigmap.add(bit);
continue;
}
@@ -493,7 +493,7 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena
entry.src.insert(s);
SigBit bit = sigmap(conn.second[i]);
- if (bit.wire && bit.wire->name[0] == '\\' && (cell->output(conn.first) || bit_user_cnt[bit] == 1)) {
+ if (bit.wire && bit.wire->name.isPublic() && (cell->output(conn.first) || bit_user_cnt[bit] == 1)) {
for (auto &s : bit.wire->get_strpool_attribute(ID::src))
entry.src.insert(s);
entry.wire = bit.wire->name;
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index d7bf125d1..9fdac6147 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -1365,7 +1365,7 @@ struct SatPass : public Pass {
if (show_public) {
for (auto wire : module->wires())
- if (wire->name[0] == '\\')
+ if (wire->name.isPublic())
shows.push_back(wire->name.str());
}
diff --git a/techlibs/xilinx/cells_sim.v b/techlibs/xilinx/cells_sim.v
index a04587e87..40804c367 100644
--- a/techlibs/xilinx/cells_sim.v
+++ b/techlibs/xilinx/cells_sim.v
@@ -3014,8 +3014,12 @@ endmodule
// Virtex 6, Series 7.
`ifdef YOSYS
-(* abc9_box=!(PREG || AREG || ADREG || BREG || CREG || DREG || MREG),
- lib_whitebox=!(PREG || AREG || ADREG || BREG || CREG || DREG || MREG) *)
+(* abc9_box=!(PREG || AREG || ADREG || BREG || CREG || DREG || MREG)
+`ifdef ALLOW_WHITEBOX_DSP48E1
+ // Do not make DSP48E1 a whitebox for ABC9 even if fully combinatorial, since it is a big complex block
+ , lib_whitebox=!(PREG || AREG || ADREG || BREG || CREG || DREG || MREG || INMODEREG || OPMODEREG || ALUMODEREG || CARRYINREG || CARRYINSELREG)
+`endif
+*)
`endif
module DSP48E1 (
output [29:0] ACOUT,
@@ -3503,11 +3507,15 @@ module DSP48E1 (
if (OPMODEr[3:2] != 2'b01) $fatal(1, "OPMODEr[3:2] must be 2'b01 when OPMODEr[1:0] is 2'b01");
`endif
end
- 2'b10: begin X = P;
+ 2'b10:
+ if (PREG == 1)
+ X = P;
+ else begin
+ X = 48'bx;
`ifndef YOSYS
- if (PREG != 1) $fatal(1, "PREG must be 1 when OPMODEr[1:0] is 2'b10");
+ $fatal(1, "PREG must be 1 when OPMODEr[1:0] is 2'b10");
`endif
- end
+ end
2'b11: X = $signed({Ar2, Br2});
default: X = 48'bx;
endcase
@@ -3529,20 +3537,36 @@ module DSP48E1 (
case (OPMODEr[6:4])
3'b000: Z = 48'b0;
3'b001: Z = PCIN;
- 3'b010: begin Z = P;
+ 3'b010:
+ if (PREG == 1)
+ Z = P;
+ else begin
+ Z = 48'bx;
`ifndef YOSYS
- if (PREG != 1) $fatal(1, "PREG must be 1 when OPMODEr[6:4] i0s 3'b010");
+ $fatal(1, "PREG must be 1 when OPMODEr[6:4] is 3'b010");
`endif
- end
+ end
3'b011: Z = Cr;
- 3'b100: begin Z = P;
+ 3'b100:
+ if (PREG == 1 && OPMODEr[3:0] === 4'b1000)
+ Z = P;
+ else begin
+ Z = 48'bx;
`ifndef YOSYS
- if (PREG != 1) $fatal(1, "PREG must be 1 when OPMODEr[6:4] is 3'b100");
- if (OPMODEr[3:0] != 4'b1000) $fatal(1, "OPMODEr[3:0] must be 4'b1000 when OPMODEr[6:4] i0s 3'b100");
+ if (PREG != 1) $fatal(1, "PREG must be 1 when OPMODEr[6:4] is 3'b100");
+ if (OPMODEr[3:0] != 4'b1000) $fatal(1, "OPMODEr[3:0] must be 4'b1000 when OPMODEr[6:4] i0s 3'b100");
`endif
- end
+ end
3'b101: Z = $signed(PCIN[47:17]);
- 3'b110: Z = $signed(P[47:17]);
+ 3'b110:
+ if (PREG == 1)
+ Z = $signed(P[47:17]);
+ else begin
+ Z = 48'bx;
+`ifndef YOSYS
+ $fatal(1, "PREG must be 1 when OPMODEr[6:4] is 3'b110");
+`endif
+ end
default: Z = 48'bx;
endcase
end
@@ -3568,10 +3592,34 @@ module DSP48E1 (
3'b001: cin_muxed = ~PCIN[47];
3'b010: cin_muxed = CARRYCASCIN;
3'b011: cin_muxed = PCIN[47];
- 3'b100: cin_muxed = CARRYCASCOUT;
- 3'b101: cin_muxed = ~P[47];
+ 3'b100:
+ if (PREG == 1)
+ cin_muxed = CARRYCASCOUT;
+ else begin
+ cin_muxed = 1'bx;
+`ifndef YOSYS
+ $fatal(1, "PREG must be 1 when CARRYINSEL is 3'b100");
+`endif
+ end
+ 3'b101:
+ if (PREG == 1)
+ cin_muxed = ~P[47];
+ else begin
+ cin_muxed = 1'bx;
+`ifndef YOSYS
+ $fatal(1, "PREG must be 1 when CARRYINSEL is 3'b101");
+`endif
+ end
3'b110: cin_muxed = A24_xnor_B17;
- 3'b111: cin_muxed = P[47];
+ 3'b111:
+ if (PREG == 1)
+ cin_muxed = P[47];
+ else begin
+ cin_muxed = 1'bx;
+`ifndef YOSYS
+ $fatal(1, "PREG must be 1 when CARRYINSEL is 3'b111");
+`endif
+ end
default: cin_muxed = 1'bx;
endcase
end
@@ -4163,4 +4211,3 @@ module RAMB36E1 (
if (|DOB_REG) (posedge CLKBWRCLK => (DOPBDOP : 4'bx)) = 882;
endspecify
endmodule
-
diff --git a/techlibs/xilinx/xc7_dsp_map.v b/techlibs/xilinx/xc7_dsp_map.v
index a4256eb92..58df977ec 100644
--- a/techlibs/xilinx/xc7_dsp_map.v
+++ b/techlibs/xilinx/xc7_dsp_map.v
@@ -33,6 +33,7 @@ module \$__MUL25X18 (input [24:0] A, input [17:0] B, output [42:0] Y);
.B(B),
.C(48'b0),
.D(25'b0),
+ .CARRYIN(1'b0),
.P(P_48),
.INMODE(5'b00000),
diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh
index de7bc68cf..bcf2b964a 100755
--- a/tests/aiger/run-test.sh
+++ b/tests/aiger/run-test.sh
@@ -55,5 +55,5 @@ done
for y in *.ys; do
echo "Running $y."
- ../../yosys $y -ql ${y%.*}.log
+ ../../yosys -ql ${y%.*}.log $y
done
diff --git a/tests/arch/xilinx/dsp_abc9.ys b/tests/arch/xilinx/dsp_abc9.ys
new file mode 100644
index 000000000..909e54149
--- /dev/null
+++ b/tests/arch/xilinx/dsp_abc9.ys
@@ -0,0 +1,37 @@
+read_verilog <<EOT
+module top(input [24:0] A, input [17:0] B, output [47:0] P);
+DSP48E1 #(.PREG(0)) dsp(.A(A), .B(B), .P(P));
+endmodule
+EOT
+techmap -autoproc -wb -map +/xilinx/cells_sim.v
+opt
+scc -expect 0
+
+
+design -reset
+read_verilog <<EOT
+module top(input signed [24:0] A, input signed [17:0] B, output [47:0] P);
+assign P = A * B;
+endmodule
+EOT
+synth_xilinx -abc9
+techmap -autoproc -wb -map +/xilinx/cells_sim.v
+opt -full -fine
+select -assert-count 1 t:$mul
+select -assert-count 0 t:* t:$mul %D
+
+
+design -reset
+read_verilog -icells -formal <<EOT
+module top(output [42:0] P);
+\$__MUL25X18 mul (.A(42), .B(42), .Y(P));
+assert property (P == 42*42);
+endmodule
+EOT
+techmap -map +/xilinx/xc7_dsp_map.v
+verilog_defaults -add -D ALLOW_WHITEBOX_DSP48E1
+synth_xilinx -abc9
+techmap -autoproc -wb -map +/xilinx/cells_sim.v
+opt -full -fine
+select -assert-count 0 t:* t:$assert %d
+sat -verify -prove-asserts
diff --git a/tests/verilog/.gitignore b/tests/verilog/.gitignore
index b48f808a1..34da23437 100644
--- a/tests/verilog/.gitignore
+++ b/tests/verilog/.gitignore
@@ -1,3 +1,5 @@
/*.log
/*.out
/run-test.mk
+/const_arst.v
+/const_sr.v
diff --git a/tests/verilog/const_arst.ys b/tests/verilog/const_arst.ys
new file mode 100644
index 000000000..df720575c
--- /dev/null
+++ b/tests/verilog/const_arst.ys
@@ -0,0 +1,24 @@
+read_verilog <<EOT
+module test (
+ input clk, d,
+ output reg q
+);
+wire nop = 1'h0;
+always @(posedge clk, posedge nop) begin
+ if (nop) q <= 1'b0;
+ else q <= d;
+end
+endmodule
+EOT
+prep -top test
+write_verilog const_arst.v
+design -stash gold
+read_verilog const_arst.v
+prep -top test
+design -stash gate
+design -copy-from gold -as gold A:top
+design -copy-from gate -as gate A:top
+miter -equiv -flatten -make_assert gold gate miter
+prep -top miter
+clk2fflogic
+sat -set-init-zero -tempinduct -prove-asserts -verify
diff --git a/tests/verilog/const_sr.ys b/tests/verilog/const_sr.ys
new file mode 100644
index 000000000..c1406b0a0
--- /dev/null
+++ b/tests/verilog/const_sr.ys
@@ -0,0 +1,25 @@
+read_verilog <<EOT
+module test (
+ input clk, rst, d,
+ output reg q
+);
+wire nop = 1'h0;
+always @(posedge clk, posedge nop, posedge rst) begin
+ if (rst) q <= 1'b0;
+ else if (nop) q <= 1'b1;
+ else q <= d;
+end
+endmodule
+EOT
+prep -top test
+write_verilog const_sr.v
+design -stash gold
+read_verilog const_sr.v
+prep -top test
+design -stash gate
+design -copy-from gold -as gold A:top
+design -copy-from gate -as gate A:top
+miter -equiv -flatten -make_assert gold gate miter
+prep -top miter
+clk2fflogic
+sat -set-init-zero -tempinduct -prove-asserts -verify
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-28 15:56:37 +0000