aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--CHANGELOG23
-rw-r--r--Makefile6
-rw-r--r--backends/firrtl/firrtl.cc6
-rw-r--r--backends/rtlil/rtlil_backend.cc2
-rw-r--r--backends/smt2/smt2.cc5
-rw-r--r--backends/verilog/verilog_backend.cc1
-rw-r--r--frontends/ast/simplify.cc6
-rw-r--r--frontends/verific/verific.cc85
-rw-r--r--frontends/verific/verific.h1
-rw-r--r--kernel/rtlil.cc11
-rw-r--r--kernel/rtlil.h1
-rw-r--r--passes/cmds/chformal.cc19
-rw-r--r--passes/cmds/show.cc138
-rw-r--r--passes/equiv/equiv_make.cc92
-rw-r--r--passes/fsm/fsm_detect.cc29
-rw-r--r--passes/techmap/bmuxmap.cc39
-rw-r--r--techlibs/gatemate/cells_bb.v9
-rw-r--r--techlibs/gatemate/cells_sim.v24
-rw-r--r--tests/svinterfaces/resolve_types.sv24
-rw-r--r--tests/svinterfaces/resolve_types.ys6
-rwxr-xr-xtests/svinterfaces/run-test.sh1
-rw-r--r--tests/techmap/bmuxmap_pmux.ys45
-rw-r--r--tests/various/chformal_coverenable.ys25
-rw-r--r--tests/various/equiv_make_make_assert.ys32
-rw-r--r--tests/various/rtlil_z_bits.ys9
-rw-r--r--tests/xprop/generate.py99
-rwxr-xr-xtests/xprop/run-test.sh2
-rw-r--r--tests/xprop/test.py12
28 files changed, 578 insertions, 174 deletions
diff --git a/CHANGELOG b/CHANGELOG
index 5e24e528f..18874a04e 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -2,9 +2,30 @@
List of major changes and improvements between releases
=======================================================
-Yosys 0.25 .. Yosys 0.25-dev
+Yosys 0.26 .. Yosys 0.26-dev
--------------------------
+
+Yosys 0.25 .. Yosys 0.26
+--------------------------
+ * New commands and options
+ - Added "bwmuxmap" pass to replace $bwmux cells with equivalent logic.
+ - Added "xprop" experimental pass for formal x propagation.
+ - Added "splitcells" pass to split up multi-bit cells.
+ - Added "viz" pass to visualize data flow graph.
+ - Added option "-make_cover" to "miter" pass.
+ - Added option "-noparallelcase" to "write_verilog" pass.
+ - Added option "-chain" to "insbuf" pass.
+ - Added options "-hierarchy" and "-assume" to "formalff" pass.
+ - Added options "-append" and "-summary" to "sim" pass.
+ - Added option "-ywmap" to "write_btor" pass.
+ - Added option "-ignore-self-reset" to "fsm_detect" pass.
+
+ * Verilog
+ - Support for struct members of union type.
+ - Support for struct member package types.
+
* Various
+ - Added Yosys witness (.yw) cosimulation.
- GCC 4.8 is deprecated, compiler with full C++11 support is required.
Yosys 0.24 .. Yosys 0.25
diff --git a/Makefile b/Makefile
index 7738e2acd..5a5772d2a 100644
--- a/Makefile
+++ b/Makefile
@@ -141,7 +141,7 @@ LDLIBS += -lrt
endif
endif
-YOSYS_VER := 0.25+86
+YOSYS_VER := 0.26+24
# Note: We arrange for .gitcommit to contain the (short) commit hash in
# tarballs generated with git-archive(1) using .gitattributes. The git repo
@@ -157,7 +157,7 @@ endif
OBJS = kernel/version_$(GIT_REV).o
bumpversion:
- sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline e02b7f6.. | wc -l`/;" Makefile
+ sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 7e58866.. | wc -l`/;" Makefile
# set 'ABCREV = default' to use abc/ as it is
#
@@ -165,7 +165,7 @@ bumpversion:
# is just a symlink to your actual ABC working directory, as 'make mrproper'
# will remove the 'abc' directory and you do not want to accidentally
# delete your work on ABC..
-ABCREV = be9a35c
+ABCREV = a8f0ef2
ABCPULL = 1
ABCURL ?= https://github.com/YosysHQ/abc
ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q)
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index d68c52563..eb30ab4b9 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -346,6 +346,12 @@ void emit_elaborated_extmodules(RTLIL::Design *design, std::ostream &f)
{
// Find the module corresponding to this instance.
auto modInstance = design->module(cell->type);
+ // Ensure that we actually have a module instance
+ if (modInstance == nullptr) {
+ log_error("Unknown cell type %s\n", cell->type.c_str());
+ return;
+ }
+
bool modIsBlackbox = modInstance->get_blackbox_attribute();
if (modIsBlackbox)
diff --git a/backends/rtlil/rtlil_backend.cc b/backends/rtlil/rtlil_backend.cc
index 7c7e26a93..574eb3aaa 100644
--- a/backends/rtlil/rtlil_backend.cc
+++ b/backends/rtlil/rtlil_backend.cc
@@ -51,7 +51,7 @@ void RTLIL_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int wi
}
}
f << stringf("%d'", width);
- if (data.is_fully_undef()) {
+ if (data.is_fully_undef_x_only()) {
f << "x";
} else {
for (int i = offset+width-1; i >= offset; i--) {
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 1ab39a405..48da3f4be 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -462,7 +462,10 @@ struct Smt2Worker
int width = GetSize(sig_y);
if (type == 's' || type == 'S' || type == 'd' || type == 'b') {
- width = max(width, GetSize(cell->getPort(ID::A)));
+ if (type == 'b')
+ width = GetSize(cell->getPort(ID::A));
+ else
+ width = max(width, GetSize(cell->getPort(ID::A)));
if (cell->hasPort(ID::B))
width = max(width, GetSize(cell->getPort(ID::B)));
}
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 0a9c0590e..3da168960 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -2329,7 +2329,6 @@ struct VerilogBackend : public Backend {
if (!noexpr) {
Pass::call(design, "bmuxmap");
Pass::call(design, "demuxmap");
- Pass::call(design, "bwmuxmap");
}
Pass::call(design, "clean_zerowidth");
log_pop();
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 5f9f9f49c..f77b59d83 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -1025,7 +1025,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
// create name resolution entries for all objects with names
// also merge multiple declarations for the same wire (e.g. "output foobar; reg foobar;")
- if (type == AST_MODULE) {
+ if (type == AST_MODULE || type == AST_INTERFACE) {
current_scope.clear();
std::set<std::string> existing;
int counter = 0;
@@ -1710,7 +1710,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
current_filename = filename;
- if (type == AST_MODULE)
+ if (type == AST_MODULE || type == AST_INTERFACE)
current_scope.clear();
// convert defparam nodes to cell parameters
@@ -4700,7 +4700,7 @@ void AstNode::mem2reg_as_needed_pass1(dict<AstNode*, pool<std::string>> &mem2reg
if (type == AST_MEMORY && (get_bool_attribute(ID::mem2reg) || (flags & AstNode::MEM2REG_FL_ALL) || !(is_reg || is_logic)))
mem2reg_candidates[this] |= AstNode::MEM2REG_FL_FORCED;
- if (type == AST_MODULE && get_bool_attribute(ID::mem2reg))
+ if ((type == AST_MODULE || type == AST_INTERFACE) && get_bool_attribute(ID::mem2reg))
children_flags |= AstNode::MEM2REG_FL_ALL;
dict<AstNode*, uint32_t> *proc_flags_p = NULL;
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 8898c4597..c1e9fc7d0 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -361,10 +361,16 @@ RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portn
for (unsigned i = 0; i < portbus->Size(); i++) {
Net *net = inst->GetNet(portbus->ElementAtIndex(i));
if (net) {
- if (net->IsGnd())
- sig.append(RTLIL::State::S0);
- else if (net->IsPwr())
- sig.append(RTLIL::State::S1);
+ if (net->IsConstant()) {
+ if (net->IsGnd())
+ sig.append(RTLIL::State::S0);
+ else if (net->IsPwr())
+ sig.append(RTLIL::State::S1);
+ else if (net->IsX())
+ sig.append(RTLIL::State::Sx);
+ else
+ sig.append(RTLIL::State::Sz);
+ }
else
sig.append(net_map_at(net));
} else
@@ -379,6 +385,36 @@ RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portn
}
}
+RTLIL::SigSpec VerificImporter::operatorInportCase(Instance *inst, const char *portname)
+{
+ PortBus *portbus = inst->View()->GetPortBus(portname);
+ if (portbus) {
+ RTLIL::SigSpec sig;
+ for (unsigned i = 0; i < portbus->Size(); i++) {
+ Net *net = inst->GetNet(portbus->ElementAtIndex(i));
+ if (net) {
+ if (net->IsConstant()) {
+ if (net->IsGnd())
+ sig.append(RTLIL::State::S0);
+ else if (net->IsPwr())
+ sig.append(RTLIL::State::S1);
+ else
+ sig.append(RTLIL::State::Sa);
+ }
+ else
+ sig.append(net_map_at(net));
+ } else
+ sig.append(RTLIL::State::Sa);
+ }
+ return sig;
+ } else {
+ Port *port = inst->View()->GetPort(portname);
+ log_assert(port != NULL);
+ Net *net = inst->GetNet(port);
+ return net_map_at(net);
+ }
+}
+
RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst, const pool<Net*, hash_ptr_ops> *any_all_nets)
{
RTLIL::SigSpec sig;
@@ -989,6 +1025,47 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
return true;
}
+ if (inst->Type() == OPER_WIDE_CASE_SELECT_BOX)
+ {
+ RTLIL::SigSpec sig_out_val = operatorInport(inst, "out_value");
+ RTLIL::SigSpec sig_select = operatorInport(inst, "select");
+ RTLIL::SigSpec sig_select_values = operatorInportCase(inst, "select_values");
+ RTLIL::SigSpec sig_data_values = operatorInport(inst, "data_values");
+ RTLIL::SigSpec sig_data_default = operatorInport(inst, "default_value");
+
+ RTLIL::Process *proc = module->addProcess(new_verific_id(inst));
+ import_attributes(proc->attributes, inst);
+
+ RTLIL::CaseRule *current_case = &proc->root_case;
+ current_case = &proc->root_case;
+
+ RTLIL::SwitchRule *sw = new RTLIL::SwitchRule;
+ sw->signal = sig_select;
+ current_case->switches.push_back(sw);
+
+ int select_width = inst->InputSize();
+ int data_width = inst->OutputSize();
+ int select_num = inst->Input1Size() / inst->InputSize();
+
+ int offset_select = 0;
+ int offset_data = 0;
+
+ for (int i = 0; i < select_num; i++) {
+ RTLIL::CaseRule *cs = new RTLIL::CaseRule;
+ cs->compare.push_back(sig_select_values.extract(offset_select, select_width));
+ cs->actions.push_back(SigSig(sig_out_val, sig_data_values.extract(offset_data, data_width)));
+ sw->cases.push_back(cs);
+
+ offset_select += select_width;
+ offset_data += data_width;
+ }
+ RTLIL::CaseRule *cs_default = new RTLIL::CaseRule;
+ cs_default->actions.push_back(SigSig(sig_out_val, sig_data_default));
+ sw->cases.push_back(cs_default);
+
+ return true;
+ }
+
#undef IN
#undef IN1
#undef IN2
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index d9f0077db..44485751c 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -87,6 +87,7 @@ struct VerificImporter
RTLIL::SigSpec operatorInput1(Verific::Instance *inst);
RTLIL::SigSpec operatorInput2(Verific::Instance *inst);
RTLIL::SigSpec operatorInport(Verific::Instance *inst, const char *portname);
+ RTLIL::SigSpec operatorInportCase(Verific::Instance *inst, const char *portname);
RTLIL::SigSpec operatorOutput(Verific::Instance *inst, const pool<Verific::Net*, hash_ptr_ops> *any_all_nets = nullptr);
bool import_netlist_instance_gates(Verific::Instance *inst, RTLIL::IdString inst_name);
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index eee014c54..7f3508b2f 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -370,6 +370,17 @@ bool RTLIL::Const::is_fully_undef() const
return true;
}
+bool RTLIL::Const::is_fully_undef_x_only() const
+{
+ cover("kernel.rtlil.const.is_fully_undef_x_only");
+
+ for (const auto &bit : bits)
+ if (bit != RTLIL::State::Sx)
+ return false;
+
+ return true;
+}
+
bool RTLIL::Const::is_onehot(int *pos) const
{
cover("kernel.rtlil.const.is_onehot");
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index 42bb66da8..7c7669caa 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -686,6 +686,7 @@ struct RTLIL::Const
bool is_fully_ones() const;
bool is_fully_def() const;
bool is_fully_undef() const;
+ bool is_fully_undef_x_only() const;
bool is_onehot(int *pos = nullptr) const;
inline RTLIL::Const extract(int offset, int len = 1, RTLIL::State padding = RTLIL::State::S0) const {
diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc
index 66044b161..da97ff71d 100644
--- a/passes/cmds/chformal.cc
+++ b/passes/cmds/chformal.cc
@@ -55,6 +55,14 @@ struct ChformalPass : public Pass {
log(" -skip <N>\n");
log(" ignore activation of the constraint in the first <N> clock cycles\n");
log("\n");
+ log(" -coverenable\n");
+ log(" add cover statements for the enable signals of the constraints\n");
+ log("\n");
+#ifdef YOSYS_ENABLE_VERIFIC
+ log(" Note: For the Verific frontend it is currently not guaranteed that a\n");
+ log(" reachable SVA statement corresponds to an active enable signal.\n");
+ log("\n");
+#endif
log(" -assert2assume\n");
log(" -assume2assert\n");
log(" -live2fair\n");
@@ -114,6 +122,10 @@ struct ChformalPass : public Pass {
mode_arg = atoi(args[++argidx].c_str());
continue;
}
+ if (mode == 0 && args[argidx] == "-coverenable") {
+ mode = 'p';
+ continue;
+ }
if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2assume") {
assert2assume = true;
mode = 'c';
@@ -263,6 +275,13 @@ struct ChformalPass : public Pass {
cell->setPort(ID::EN, module->LogicAnd(NEW_ID, en, cell->getPort(ID::EN)));
}
else
+ if (mode =='p')
+ {
+ for (auto cell : constr_cells)
+ module->addCover(NEW_ID_SUFFIX("coverenable"),
+ cell->getPort(ID::EN), State::S1, cell->get_src_attribute());
+ }
+ else
if (mode == 'c')
{
for (auto cell : constr_cells)
diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc
index a7c77f96f..dd7de8273 100644
--- a/passes/cmds/show.cc
+++ b/passes/cmds/show.cc
@@ -233,76 +233,101 @@ struct ShowWorker
return std::string();
}
+ // Return the pieces of a label joined by a '|' separator
+ std::string join_label_pieces(std::vector<std::string> pieces)
+ {
+ std::string ret = "";
+ bool first_piece = true;
+
+ for (auto &piece : pieces) {
+ if (!first_piece)
+ ret += "|";
+ ret += piece;
+ first_piece = false;
+ }
+
+ return ret;
+ }
+
std::string gen_portbox(std::string port, RTLIL::SigSpec sig, bool driver, std::string *node = nullptr)
{
std::string code;
std::string net = gen_signode_simple(sig);
if (net.empty())
{
- std::string label_string;
- int pos = sig.size()-1;
- int idx = single_idx_count++;
- for (int rep, i = int(sig.chunks().size())-1; i >= 0; i -= rep) {
- const RTLIL::SigChunk &c = sig.chunks().at(i);
+ int dot_idx = single_idx_count++;
+ std::vector<std::string> label_pieces;
+ int bitpos = sig.size()-1;
+
+ for (int rep, chunk_idx = ((int) sig.chunks().size()) - 1; chunk_idx >= 0; chunk_idx -= rep) {
+ const RTLIL::SigChunk &c = sig.chunks().at(chunk_idx);
+
+ // Find the number of times this chunk is repeating
+ for (rep = 1; chunk_idx - rep >= 0 && c == sig.chunks().at(chunk_idx - rep); rep++);
+
int cl, cr;
- if (c.wire) {
+ cl = c.offset + c.width - 1;
+ cr = c.offset;
+
+ if (c.is_wire()) {
if (c.wire->upto) {
- cr = c.wire->start_offset + (c.wire->width - c.offset - 1);
+ cr = (c.wire->width - 1) - c.offset;
cl = cr - (c.width - 1);
- } else {
- cr = c.wire->start_offset + c.offset;
- cl = cr + c.width - 1;
}
- } else {
- cl = c.offset + c.width - 1;
- cr = c.offset;
+
+ cl += c.wire->start_offset;
+ cr += c.wire->start_offset;
}
- if (!driver && c.wire == nullptr) {
- RTLIL::State s1 = c.data.front();
- for (auto s2 : c.data)
- if (s1 != s2)
- goto not_const_stream;
- net.clear();
- } else {
- not_const_stream:
+
+ // Is this chunk a constant filled with one kind of bit state?
+ bool no_signode = !driver && !c.is_wire() \
+ && std::equal(c.data.begin() + 1, c.data.end(), c.data.begin());
+
+ if (!no_signode) {
net = gen_signode_simple(c, false);
log_assert(!net.empty());
}
- for (rep = 1; i-rep >= 0 && c == sig.chunks().at(i-rep); rep++) {}
+
std::string repinfo = rep > 1 ? stringf("%dx ", rep) : "";
+ std::string portside = stringf("%d:%d", bitpos, bitpos - rep*c.width + 1);
+ std::string remoteside = stringf("%s%d:%d", repinfo.c_str(), cl, cr);
+
if (driver) {
log_assert(!net.empty());
- label_string += stringf("<s%d> %d:%d - %s%d:%d |", i, pos, pos-c.width+1, repinfo.c_str(), cl, cr);
- net_conn_map[net].in.insert({stringf("x%d:s%d", idx, i), rep*c.width});
+ label_pieces.push_back(stringf("<s%d> %s - %s ", chunk_idx, portside.c_str(), remoteside.c_str()));
+ net_conn_map[net].in.insert({stringf("x%d:s%d", dot_idx, chunk_idx), rep*c.width});
net_conn_map[net].color = nextColor(c, net_conn_map[net].color);
- } else
- if (net.empty()) {
- log_assert(rep == 1);
- label_string += stringf("%c -&gt; %d:%d |",
- c.data.front() == State::S0 ? '0' :
- c.data.front() == State::S1 ? '1' :
- c.data.front() == State::Sx ? 'X' :
- c.data.front() == State::Sz ? 'Z' : '?',
- pos, pos-rep*c.width+1);
} else {
- label_string += stringf("<s%d> %s%d:%d - %d:%d |", i, repinfo.c_str(), cl, cr, pos, pos-rep*c.width+1);
- net_conn_map[net].out.insert({stringf("x%d:s%d", idx, i), rep*c.width});
- net_conn_map[net].color = nextColor(c, net_conn_map[net].color);
+ if (no_signode) {
+ log_assert(rep == 1);
+ label_pieces.push_back(stringf("%c -&gt; %d:%d ",
+ c.data.front() == State::S0 ? '0' :
+ c.data.front() == State::S1 ? '1' :
+ c.data.front() == State::Sx ? 'X' :
+ c.data.front() == State::Sz ? 'Z' : '?',
+ bitpos, bitpos-rep*c.width+1));
+ } else {
+ label_pieces.push_back(stringf("<s%d> %s - %s ", chunk_idx, remoteside.c_str(), portside.c_str()));
+ net_conn_map[net].out.insert({stringf("x%d:s%d", dot_idx, chunk_idx), rep*c.width});
+ net_conn_map[net].color = nextColor(c, net_conn_map[net].color);
+ }
}
- pos -= rep * c.width;
+
+ bitpos -= rep * c.width;
}
- if (label_string[label_string.size()-1] == '|')
- label_string = label_string.substr(0, label_string.size()-1);
- code += stringf("x%d [ shape=record, style=rounded, label=\"%s\" ];\n", idx, label_string.c_str());
+
+ code += stringf("x%d [ shape=record, style=rounded, label=\"", dot_idx) \
+ + join_label_pieces(label_pieces) + "\" ];\n";
+
if (!port.empty()) {
currentColor = xorshift32(currentColor);
if (driver)
- code += stringf("%s:e -> x%d:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, %s, %s];\n", port.c_str(), idx, nextColor(sig).c_str(), widthLabel(sig.size()).c_str());
+ code += stringf("%s:e -> x%d:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, %s, %s];\n", port.c_str(), dot_idx, nextColor(sig).c_str(), widthLabel(sig.size()).c_str());
else
- code += stringf("x%d:e -> %s:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, %s, %s];\n", idx, port.c_str(), nextColor(sig).c_str(), widthLabel(sig.size()).c_str());
+ code += stringf("x%d:e -> %s:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, %s, %s];\n", dot_idx, port.c_str(), nextColor(sig).c_str(), widthLabel(sig.size()).c_str());
}
if (node != nullptr)
- *node = stringf("x%d", idx);
+ *node = stringf("x%d", dot_idx);
}
else
{
@@ -417,6 +442,7 @@ struct ShowWorker
for (auto cell : module->selected_cells())
{
std::vector<RTLIL::IdString> in_ports, out_ports;
+ std::vector<std::string> in_label_pieces, out_label_pieces;
for (auto &conn : cell->connections()) {
if (!ct.cell_output(cell->type, conn.first))
@@ -428,23 +454,23 @@ struct ShowWorker
std::sort(in_ports.begin(), in_ports.end(), RTLIL::sort_by_id_str());
std::sort(out_ports.begin(), out_ports.end(), RTLIL::sort_by_id_str());
- std::string label_string = "{{";
+ for (auto &p : in_ports) {
+ bool signed_suffix = genSignedLabels && cell->hasParam(p.str() + "_SIGNED")
+ && cell->getParam(p.str() + "_SIGNED").as_bool();
- for (auto &p : in_ports)
- label_string += stringf("<p%d> %s%s|", id2num(p), escape(p.str()),
- genSignedLabels && cell->hasParam(p.str() + "_SIGNED") &&
- cell->getParam(p.str() + "_SIGNED").as_bool() ? "*" : "");
- if (label_string[label_string.size()-1] == '|')
- label_string = label_string.substr(0, label_string.size()-1);
-
- label_string += stringf("}|%s\\n%s|{", findLabel(cell->name.str()), escape(cell->type.str()));
+ in_label_pieces.push_back(stringf("<p%d> %s%s", id2num(p), escape(p.str()),
+ signed_suffix ? "*" : ""));
+ }
for (auto &p : out_ports)
- label_string += stringf("<p%d> %s|", id2num(p), escape(p.str()));
- if (label_string[label_string.size()-1] == '|')
- label_string = label_string.substr(0, label_string.size()-1);
+ out_label_pieces.push_back(stringf("<p%d> %s", id2num(p), escape(p.str())));
+
+ std::string in_label = join_label_pieces(in_label_pieces);
+ std::string out_label = join_label_pieces(out_label_pieces);
- label_string += "}}";
+ std::string label_string = stringf("{{%s}|%s\\n%s|{%s}}", in_label.c_str(),
+ findLabel(cell->name.str()), escape(cell->type.str()),
+ out_label.c_str());
std::string code;
for (auto &conn : cell->connections()) {
diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc
index 27cec7549..e15e510be 100644
--- a/passes/equiv/equiv_make.cc
+++ b/passes/equiv/equiv_make.cc
@@ -33,6 +33,7 @@ struct EquivMakeWorker
bool inames;
vector<string> blacklists;
vector<string> encfiles;
+ bool make_assert;
pool<IdString> blacklist_names;
dict<IdString, dict<Const, Const>> encdata;
@@ -133,6 +134,12 @@ struct EquivMakeWorker
delete gate_clone;
}
+ void add_eq_assertion(const SigSpec &gold_sig, const SigSpec &gate_sig)
+ {
+ auto eq_wire = equiv_mod->Eqx(NEW_ID, gold_sig, gate_sig);
+ equiv_mod->addAssert(NEW_ID_SUFFIX("assert"), eq_wire, State::S1);
+ }
+
void find_same_wires()
{
SigMap assign_map(equiv_mod);
@@ -231,15 +238,24 @@ struct EquivMakeWorker
if (gold_wire->port_output || gate_wire->port_output)
{
- Wire *wire = equiv_mod->addWire(id, gold_wire->width);
- wire->port_output = true;
gold_wire->port_input = false;
gate_wire->port_input = false;
gold_wire->port_output = false;
gate_wire->port_output = false;
- for (int i = 0; i < wire->width; i++)
- equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i));
+ Wire *wire = equiv_mod->addWire(id, gold_wire->width);
+ wire->port_output = true;
+
+ if (make_assert)
+ {
+ add_eq_assertion(gold_wire, gate_wire);
+ equiv_mod->connect(wire, gold_wire);
+ }
+ else
+ {
+ for (int i = 0; i < wire->width; i++)
+ equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i));
+ }
rd_signal_map.add(assign_map(gold_wire), wire);
rd_signal_map.add(assign_map(gate_wire), wire);
@@ -259,26 +275,31 @@ struct EquivMakeWorker
}
else
{
- Wire *wire = equiv_mod->addWire(id, gold_wire->width);
- SigSpec rdmap_gold, rdmap_gate, rdmap_equiv;
+ if (make_assert)
+ add_eq_assertion(gold_wire, gate_wire);
- for (int i = 0; i < wire->width; i++) {
- if (undriven_bits.count(assign_map(SigBit(gold_wire, i)))) {
- log(" Skipping signal bit %s [%d]: undriven on gold side.\n", id2cstr(gold_wire->name), i);
- continue;
- }
- if (undriven_bits.count(assign_map(SigBit(gate_wire, i)))) {
- log(" Skipping signal bit %s [%d]: undriven on gate side.\n", id2cstr(gate_wire->name), i);
- continue;
+ else {
+ Wire *wire = equiv_mod->addWire(id, gold_wire->width);
+ SigSpec rdmap_gold, rdmap_gate, rdmap_equiv;
+
+ for (int i = 0; i < wire->width; i++) {
+ if (undriven_bits.count(assign_map(SigBit(gold_wire, i)))) {
+ log(" Skipping signal bit %s [%d]: undriven on gold side.\n", id2cstr(gold_wire->name), i);
+ continue;
+ }
+ if (undriven_bits.count(assign_map(SigBit(gate_wire, i)))) {
+ log(" Skipping signal bit %s [%d]: undriven on gate side.\n", id2cstr(gate_wire->name), i);
+ continue;
+ }
+ equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i));
+ rdmap_gold.append(SigBit(gold_wire, i));
+ rdmap_gate.append(SigBit(gate_wire, i));
+ rdmap_equiv.append(SigBit(wire, i));
}
- equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i));
- rdmap_gold.append(SigBit(gold_wire, i));
- rdmap_gate.append(SigBit(gate_wire, i));
- rdmap_equiv.append(SigBit(wire, i));
- }
- rd_signal_map.add(rdmap_gold, rdmap_equiv);
- rd_signal_map.add(rdmap_gate, rdmap_equiv);
+ rd_signal_map.add(rdmap_gold, rdmap_equiv);
+ rd_signal_map.add(rdmap_gate, rdmap_equiv);
+ }
}
}
@@ -335,12 +356,20 @@ struct EquivMakeWorker
continue;
}
- for (int i = 0; i < GetSize(gold_sig); i++)
- if (gold_sig[i] != gate_sig[i]) {
- Wire *w = equiv_mod->addWire(NEW_ID);
- equiv_mod->addEquiv(NEW_ID, gold_sig[i], gate_sig[i], w);
- gold_sig[i] = w;
- }
+ if (make_assert)
+ {
+ if (gold_sig != gate_sig)
+ add_eq_assertion(gold_sig, gate_sig);
+ }
+ else
+ {
+ for (int i = 0; i < GetSize(gold_sig); i++)
+ if (gold_sig[i] != gate_sig[i]) {
+ Wire *w = equiv_mod->addWire(NEW_ID);
+ equiv_mod->addEquiv(NEW_ID, gold_sig[i], gate_sig[i], w);
+ gold_sig[i] = w;
+ }
+ }
gold_cell->setPort(gold_conn.first, gold_sig);
}
@@ -417,6 +446,10 @@ struct EquivMakePass : public Pass {
log(" Match FSM encodings using the description from the file.\n");
log(" See 'help fsm_recode' for details.\n");
log("\n");
+ log(" -make_assert\n");
+ log(" Check equivalence with $assert cells instead of $equiv.\n");
+ log(" $eqx (===) is used to compare signals.");
+ log("\n");
log("Note: The circuit created by this command is not a miter (with something like\n");
log("a trigger output), but instead uses $equiv cells to encode the equivalence\n");
log("checking problem. Use 'miter -equiv' if you want to create a miter circuit.\n");
@@ -427,6 +460,7 @@ struct EquivMakePass : public Pass {
EquivMakeWorker worker;
worker.ct.setup(design);
worker.inames = false;
+ worker.make_assert = false;
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
@@ -443,6 +477,10 @@ struct EquivMakePass : public Pass {
worker.encfiles.push_back(args[++argidx]);
continue;
}
+ if (args[argidx] == "-make_assert") {
+ worker.make_assert = true;
+ continue;
+ }
break;
}
diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc
index 5378ec89e..86d654cc4 100644
--- a/passes/fsm/fsm_detect.cc
+++ b/passes/fsm/fsm_detect.cc
@@ -118,7 +118,7 @@ static bool check_state_users(RTLIL::SigSpec sig)
return true;
}
-static void detect_fsm(RTLIL::Wire *wire)
+static void detect_fsm(RTLIL::Wire *wire, bool ignore_self_reset=false)
{
bool has_fsm_encoding_attr = wire->attributes.count(ID::fsm_encoding) > 0 && wire->attributes.at(ID::fsm_encoding).decode_string() != "none";
bool has_fsm_encoding_none = wire->attributes.count(ID::fsm_encoding) > 0 && wire->attributes.at(ID::fsm_encoding).decode_string() == "none";
@@ -199,7 +199,7 @@ static void detect_fsm(RTLIL::Wire *wire)
}
SigSpec sig_y = sig_d, sig_undef;
- if (ce.eval(sig_y, sig_undef))
+ if (!ignore_self_reset && ce.eval(sig_y, sig_undef))
is_self_resetting = true;
}
@@ -261,12 +261,15 @@ struct FsmDetectPass : public Pass {
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
- log(" fsm_detect [selection]\n");
+ log(" fsm_detect [options] [selection]\n");
log("\n");
log("This pass detects finite state machines by identifying the state signal.\n");
log("The state signal is then marked by setting the attribute 'fsm_encoding'\n");
log("on the state signal to \"auto\".\n");
log("\n");
+ log(" -ignore-self-reset\n");
+ log(" Mark FSMs even if they are self-resetting\n");
+ log("\n");
log("Existing 'fsm_encoding' attributes are not changed by this pass.\n");
log("\n");
log("Signals can be protected from being detected by this pass by setting the\n");
@@ -276,16 +279,28 @@ struct FsmDetectPass : public Pass {
log("before this pass to prepare the design for fsm_detect.\n");
log("\n");
#ifdef YOSYS_ENABLE_VERIFIC
- log("The Verific frontend may merge multiplexers in a way that interferes with FSM\n");
+ log("The Verific frontend may optimize the design in a way that interferes with FSM\n");
log("detection. Run 'verific -cfg db_infer_wide_muxes_post_elaboration 0' before\n");
- log("reading the source, and 'bmuxmap' after 'proc' for best results.\n");
+ log("reading the source, and 'bmuxmap -pmux' after 'proc' for best results.\n");
log("\n");
#endif
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
log_header(design, "Executing FSM_DETECT pass (finding FSMs in design).\n");
- extra_args(args, 1, design);
+
+ bool ignore_self_reset = false;
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ if (args[argidx] == "-ignore-self-reset") {
+ ignore_self_reset = true;
+ continue;
+ }
+ break;
+ }
+ extra_args(args, argidx, design);
CellTypes ct;
ct.setup_internals();
@@ -321,7 +336,7 @@ struct FsmDetectPass : public Pass {
sig_at_port.add(assign_map(wire));
for (auto wire : module->selected_wires())
- detect_fsm(wire);
+ detect_fsm(wire, ignore_self_reset);
}
assign_map.clear();
diff --git a/passes/techmap/bmuxmap.cc b/passes/techmap/bmuxmap.cc
index 03673c278..7aa67d3c0 100644
--- a/passes/techmap/bmuxmap.cc
+++ b/passes/techmap/bmuxmap.cc
@@ -33,13 +33,22 @@ struct BmuxmapPass : public Pass {
log("\n");
log("This pass transforms $bmux cells to trees of $mux cells.\n");
log("\n");
+ log(" -pmux\n");
+ log(" transform to $pmux instead of $mux cells.\n");
+ log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
+ bool pmux_mode = false;
+
log_header(design, "Executing BMUXMAP pass.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
+ if (args[argidx] == "-pmux") {
+ pmux_mode = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
@@ -53,18 +62,36 @@ struct BmuxmapPass : public Pass {
SigSpec sel = cell->getPort(ID::S);
SigSpec data = cell->getPort(ID::A);
int width = GetSize(cell->getPort(ID::Y));
+ int s_width = GetSize(cell->getPort(ID::S));
- for (int idx = 0; idx < GetSize(sel); idx++) {
- SigSpec new_data = module->addWire(NEW_ID, GetSize(data)/2);
- for (int i = 0; i < GetSize(new_data); i += width) {
- RTLIL::Cell *mux = module->addMux(NEW_ID,
+ if(pmux_mode)
+ {
+ int num_cases = 1 << s_width;
+ SigSpec new_a = SigSpec(State::Sx, width);
+ SigSpec new_s = module->addWire(NEW_ID, num_cases);
+ SigSpec new_data = module->addWire(NEW_ID, width);
+ for (int val = 0; val < num_cases; val++)
+ {
+ module->addEq(NEW_ID, sel, SigSpec(val, GetSize(sel)), new_s[val]);
+ }
+ RTLIL::Cell *pmux = module->addPmux(NEW_ID, new_a, data, new_s, new_data);
+ pmux->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src));
+ data = new_data;
+ }
+ else
+ {
+ for (int idx = 0; idx < GetSize(sel); idx++) {
+ SigSpec new_data = module->addWire(NEW_ID, GetSize(data)/2);
+ for (int i = 0; i < GetSize(new_data); i += width) {
+ RTLIL::Cell *mux = module->addMux(NEW_ID,
data.extract(i*2, width),
data.extract(i*2+width, width),
sel[idx],
new_data.extract(i, width));
- mux->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src));
+ mux->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src));
+ }
+ data = new_data;
}
- data = new_data;
}
module->connect(cell->getPort(ID::Y), data);
diff --git a/techlibs/gatemate/cells_bb.v b/techlibs/gatemate/cells_bb.v
index f6fe6a3e1..87b91764f 100644
--- a/techlibs/gatemate/cells_bb.v
+++ b/techlibs/gatemate/cells_bb.v
@@ -22,6 +22,9 @@ module CC_PLL #(
parameter REF_CLK = "", // e.g. "10.0"
parameter OUT_CLK = "", // e.g. "50.0"
parameter PERF_MD = "", // LOWPOWER, ECONOMY, SPEED
+ parameter LOCK_REQ = 1,
+ parameter CLK270_DOUB = 0,
+ parameter CLK180_DOUB = 0,
parameter LOW_JITTER = 1,
parameter CI_FILTER_CONST = 2,
parameter CP_FILTER_CONST = 4
@@ -123,6 +126,12 @@ module CC_CFG_CTRL(
);
endmodule
+(* blackbox *) (* keep *)
+module CC_USR_RSTN (
+ output USR_RSTN
+);
+endmodule
+
(* blackbox *)
module CC_FIFO_40K (
output A_ECC_1B_ERR,
diff --git a/techlibs/gatemate/cells_sim.v b/techlibs/gatemate/cells_sim.v
index 7e88fd7cf..7ed6d83ff 100644
--- a/techlibs/gatemate/cells_sim.v
+++ b/techlibs/gatemate/cells_sim.v
@@ -114,10 +114,10 @@ module CC_LVDS_IBUF #(
parameter [0:0] FF_IBF = 1'bx
)(
(* iopad_external_pin *)
- input IP, IN,
+ input I_P, I_N,
output Y
);
- assign Y = IP;
+ assign Y = I_P;
endmodule
@@ -133,10 +133,10 @@ module CC_LVDS_OBUF #(
)(
input A,
(* iopad_external_pin *)
- output OP, ON
+ output O_P, O_N
);
- assign OP = A;
- assign ON = ~A;
+ assign O_P = A;
+ assign O_N = ~A;
endmodule
@@ -152,10 +152,10 @@ module CC_LVDS_TOBUF #(
)(
input A, T,
(* iopad_external_pin *)
- output OP, ON
+ output O_P, O_N
);
- assign OP = T ? 1'bz : A;
- assign ON = T ? 1'bz : ~A;
+ assign O_P = T ? 1'bz : A;
+ assign O_N = T ? 1'bz : ~A;
endmodule
@@ -174,12 +174,12 @@ module CC_LVDS_IOBUF #(
)(
input A, T,
(* iopad_external_pin *)
- inout IOP, ION,
+ inout IO_P, IO_N,
output Y
);
- assign IOP = T ? 1'bz : A;
- assign ION = T ? 1'bz : ~A;
- assign Y = IOP;
+ assign IO_P = T ? 1'bz : A;
+ assign IO_N = T ? 1'bz : ~A;
+ assign Y = IO_P;
endmodule
diff --git a/tests/svinterfaces/resolve_types.sv b/tests/svinterfaces/resolve_types.sv
new file mode 100644
index 000000000..3c6644e33
--- /dev/null
+++ b/tests/svinterfaces/resolve_types.sv
@@ -0,0 +1,24 @@
+// This test checks that types, including package types, are resolved from within an interface.
+
+typedef logic [7:0] x_t;
+
+package pkg;
+ typedef logic [7:0] y_t;
+endpackage
+
+interface iface;
+ x_t x;
+ pkg::y_t y;
+endinterface
+
+module dut (input logic [7:0] x, output logic [7:0] y);
+ iface intf();
+ assign intf.x = x;
+ assign y = intf.y;
+
+ ondemand u(.intf);
+endmodule
+
+module ref (input logic [7:0] x, output logic [7:0] y);
+ assign y = ~x;
+endmodule
diff --git a/tests/svinterfaces/resolve_types.ys b/tests/svinterfaces/resolve_types.ys
new file mode 100644
index 000000000..a25791f37
--- /dev/null
+++ b/tests/svinterfaces/resolve_types.ys
@@ -0,0 +1,6 @@
+read_verilog -sv resolve_types.sv
+hierarchy -libdir . -check
+flatten
+equiv_make ref dut equiv
+equiv_simple
+equiv_status -assert
diff --git a/tests/svinterfaces/run-test.sh b/tests/svinterfaces/run-test.sh
index 9ef53926c..afa222766 100755
--- a/tests/svinterfaces/run-test.sh
+++ b/tests/svinterfaces/run-test.sh
@@ -4,3 +4,4 @@
./runone.sh svinterface_at_top
./run_simple.sh load_and_derive
+./run_simple.sh resolve_types
diff --git a/tests/techmap/bmuxmap_pmux.ys b/tests/techmap/bmuxmap_pmux.ys
new file mode 100644
index 000000000..c75d981e7
--- /dev/null
+++ b/tests/techmap/bmuxmap_pmux.ys
@@ -0,0 +1,45 @@
+read_ilang << EOT
+
+module \top
+ wire width 4 input 0 \S
+ wire width 5 output 1 \Y
+
+ cell $bmux $0
+ parameter \WIDTH 5
+ parameter \S_WIDTH 4
+ connect \A 80'10110100011101110001110010001110101010111000110011111111111110100000110100111000
+ connect \S \S
+ connect \Y \Y
+ end
+end
+
+EOT
+
+hierarchy -auto-top
+equiv_opt -assert bmuxmap -pmux
+
+###
+design -reset
+
+read_ilang << EOT
+
+module \top
+ wire width 10 input 0 \A
+ wire input 1 \S
+ wire width 5 output 2 \Y
+
+ cell $bmux $0
+ parameter \WIDTH 5
+ parameter \S_WIDTH 1
+ connect \A \A
+ connect \S \S
+ connect \Y \Y
+ end
+end
+
+EOT
+
+hierarchy -auto-top
+equiv_opt -assert bmuxmap -pmux
+
+
diff --git a/tests/various/chformal_coverenable.ys b/tests/various/chformal_coverenable.ys
new file mode 100644
index 000000000..52b3ee6bf
--- /dev/null
+++ b/tests/various/chformal_coverenable.ys
@@ -0,0 +1,25 @@
+read_verilog -formal <<EOT
+module top(input a, b, c, d);
+
+ always @* begin
+ if (a) assert (b == c);
+ if (!a) assert (b != c);
+ if (b) assume (c);
+ if (c) cover (d);
+ end
+
+endmodule
+EOT
+
+prep -top top
+
+select -assert-count 1 t:$cover
+
+chformal -cover -coverenable
+select -assert-count 2 t:$cover
+
+chformal -assert -coverenable
+select -assert-count 4 t:$cover
+
+chformal -assume -coverenable
+select -assert-count 5 t:$cover
diff --git a/tests/various/equiv_make_make_assert.ys b/tests/various/equiv_make_make_assert.ys
new file mode 100644
index 000000000..1c2efa723
--- /dev/null
+++ b/tests/various/equiv_make_make_assert.ys
@@ -0,0 +1,32 @@
+read_verilog <<EOT
+module gold(
+ input wire [7:0] a,
+ input wire [7:0] b,
+ output wire [7:0] c
+);
+
+wire [7:0] b_neg;
+assign b_neg = -b;
+assign c = a + b_neg;
+endmodule
+
+module gate(
+ input wire [7:0] a,
+ input wire [7:0] b,
+ output wire [7:0] c
+);
+
+wire [7:0] b_neg;
+assign b_neg = ~b + 1;
+assign c = a + b_neg;
+endmodule
+
+EOT
+
+equiv_make -make_assert gold gate miter
+
+select -assert-count 0 t:$equiv
+select -assert-count 2 t:$assert
+
+prep -top miter
+sat -prove-asserts -verify
diff --git a/tests/various/rtlil_z_bits.ys b/tests/various/rtlil_z_bits.ys
new file mode 100644
index 000000000..c38669159
--- /dev/null
+++ b/tests/various/rtlil_z_bits.ys
@@ -0,0 +1,9 @@
+! mkdir -p temp
+read_rtlil <<EOT
+module \test
+ wire output 1 \a
+ connect \a 1'z
+end
+EOT
+write_rtlil temp/rtlil_z_bits.il
+! grep -F -q "connect \\a 1'z" temp/rtlil_z_bits.il
diff --git a/tests/xprop/generate.py b/tests/xprop/generate.py
index eef8dc36e..484f1661c 100644
--- a/tests/xprop/generate.py
+++ b/tests/xprop/generate.py
@@ -6,6 +6,7 @@ import argparse
parser = argparse.ArgumentParser(formatter_class=argparse.ArgumentDefaultsHelpFormatter)
parser.add_argument('-S', '--seed', type=int, help='seed for PRNG')
+parser.add_argument('-m', '--more', action='store_true', help='run more tests')
parser.add_argument('-c', '--count', type=int, default=32, help='number of random patterns to test')
parser.add_argument('-f', '--filter', default='', help='regular expression to filter tests to generate')
args = parser.parse_args()
@@ -32,7 +33,7 @@ def add_test(name, src, seq=False):
print(
f"\t@cd {workdir} && python3 -u ../test.py -S {args.seed} -c {args.count}{seq_arg} > test.log 2>&1 || echo {workdir}: failed > status\n"
f"\t@cat {workdir}/status\n"
- # f"\t@grep '^.*: ok' {workdir}/status\n"
+ f"\t@grep '^.*: ok' {workdir}/status\n"
,
file=makefile,
)
@@ -123,50 +124,55 @@ print(".PHONY: all", file=makefile)
print("all:\n\t@echo done\n", file=makefile)
for cell in ["not", "pos", "neg"]:
- unary_test(cell, 1, False, 1)
- unary_test(cell, 3, False, 3)
- unary_test(cell, 3, True, 3)
- unary_test(cell, 3, True, 1)
- unary_test(cell, 3, False, 5)
+ if args.more:
+ unary_test(cell, 1, False, 1)
+ unary_test(cell, 3, False, 3)
+ unary_test(cell, 3, True, 3)
+ unary_test(cell, 3, True, 1)
+ unary_test(cell, 3, False, 5)
unary_test(cell, 3, True, 5)
for cell in ["and", "or", "xor", "xnor"]:
binary_test(cell, 1, 1, False, 1)
binary_test(cell, 1, 1, True, 2)
binary_test(cell, 2, 2, False, 2)
- binary_test(cell, 2, 2, False, 1)
- binary_test(cell, 2, 1, False, 2)
- binary_test(cell, 2, 1, False, 1)
+ if args.more:
+ binary_test(cell, 2, 2, False, 1)
+ binary_test(cell, 2, 1, False, 2)
+ binary_test(cell, 2, 1, False, 1)
# [, "pow"] are not implemented yet
for cell in ["add", "sub", "mul", "div", "mod", "divfloor", "modfloor"]:
- binary_test(cell, 1, 1, False, 1)
- binary_test(cell, 1, 1, False, 2)
- binary_test(cell, 3, 3, False, 1)
- binary_test(cell, 3, 3, False, 3)
- binary_test(cell, 3, 3, False, 6)
- binary_test(cell, 3, 3, True, 1)
- binary_test(cell, 3, 3, True, 3)
- binary_test(cell, 3, 3, True, 6)
+ if args.more:
+ binary_test(cell, 1, 1, False, 1)
+ binary_test(cell, 1, 1, False, 2)
+ binary_test(cell, 3, 3, False, 1)
+ binary_test(cell, 3, 3, False, 3)
+ binary_test(cell, 3, 3, False, 6)
+ binary_test(cell, 3, 3, True, 1)
+ binary_test(cell, 3, 3, True, 3)
+ binary_test(cell, 3, 3, True, 6)
binary_test(cell, 5, 3, False, 3)
binary_test(cell, 5, 3, True, 3)
for cell in ["lt", "le", "eq", "ne", "eqx", "nex", "ge", "gt"]:
- binary_test(cell, 1, 1, False, 1)
- binary_test(cell, 1, 1, False, 2)
- binary_test(cell, 3, 3, False, 1)
- binary_test(cell, 3, 3, False, 2)
- binary_test(cell, 3, 3, True, 1)
- binary_test(cell, 3, 3, True, 2)
- binary_test(cell, 5, 3, False, 1)
- binary_test(cell, 5, 3, True, 1)
+ if args.more:
+ binary_test(cell, 1, 1, False, 1)
+ binary_test(cell, 1, 1, False, 2)
+ binary_test(cell, 3, 3, False, 1)
+ binary_test(cell, 3, 3, False, 2)
+ binary_test(cell, 3, 3, True, 1)
+ binary_test(cell, 3, 3, True, 2)
+ binary_test(cell, 5, 3, False, 1)
+ binary_test(cell, 5, 3, True, 1)
binary_test(cell, 5, 3, False, 2)
binary_test(cell, 5, 3, True, 2)
for cell in ["reduce_and", "reduce_or", "reduce_xor", "reduce_xnor"]:
- unary_test(cell, 1, False, 1)
- unary_test(cell, 3, False, 1)
- unary_test(cell, 3, True, 1)
+ if args.more:
+ unary_test(cell, 1, False, 1)
+ unary_test(cell, 3, False, 1)
+ unary_test(cell, 3, True, 1)
unary_test(cell, 3, False, 3)
unary_test(cell, 3, True, 3)
@@ -183,33 +189,36 @@ for cell in ["logic_and", "logic_or"]:
binary_test(cell, 3, 3, True, 1)
for cell in ["shl", "shr", "sshl", "sshr", "shift"]:
- shift_test(cell, 2, 1, False, False, 2)
- shift_test(cell, 2, 1, True, False, 2)
- shift_test(cell, 2, 1, False, False, 4)
- shift_test(cell, 2, 1, True, False, 4)
- shift_test(cell, 4, 2, False, False, 4)
- shift_test(cell, 4, 2, True, False, 4)
- shift_test(cell, 4, 2, False, False, 8)
- shift_test(cell, 4, 2, True, False, 8)
+ if args.more:
+ shift_test(cell, 2, 1, False, False, 2)
+ shift_test(cell, 2, 1, True, False, 2)
+ shift_test(cell, 2, 1, False, False, 4)
+ shift_test(cell, 2, 1, True, False, 4)
+ shift_test(cell, 4, 2, False, False, 4)
+ shift_test(cell, 4, 2, True, False, 4)
+ shift_test(cell, 4, 2, False, False, 8)
+ shift_test(cell, 4, 2, True, False, 8)
shift_test(cell, 4, 3, False, False, 3)
shift_test(cell, 4, 3, True, False, 3)
for cell in ["shift"]:
- shift_test(cell, 2, 1, False, True, 2)
- shift_test(cell, 2, 1, True, True, 2)
- shift_test(cell, 2, 1, False, True, 4)
- shift_test(cell, 2, 1, True, True, 4)
- shift_test(cell, 4, 2, False, True, 4)
- shift_test(cell, 4, 2, True, True, 4)
+ if args.more:
+ shift_test(cell, 2, 1, False, True, 2)
+ shift_test(cell, 2, 1, True, True, 2)
+ shift_test(cell, 2, 1, False, True, 4)
+ shift_test(cell, 2, 1, True, True, 4)
+ shift_test(cell, 4, 2, False, True, 4)
+ shift_test(cell, 4, 2, True, True, 4)
shift_test(cell, 4, 2, False, True, 8)
shift_test(cell, 4, 2, True, True, 8)
shift_test(cell, 4, 3, False, True, 3)
shift_test(cell, 4, 3, True, True, 3)
for cell in ["shiftx"]:
- shift_test(cell, 2, 1, False, True, 2)
- shift_test(cell, 2, 1, False, True, 4)
- shift_test(cell, 4, 2, False, True, 4)
+ if args.more:
+ shift_test(cell, 2, 1, False, True, 2)
+ shift_test(cell, 2, 1, False, True, 4)
+ shift_test(cell, 4, 2, False, True, 4)
shift_test(cell, 4, 2, False, True, 8)
shift_test(cell, 4, 3, False, True, 3)
diff --git a/tests/xprop/run-test.sh b/tests/xprop/run-test.sh
index 1fc7e10b6..db4b7ca82 100755
--- a/tests/xprop/run-test.sh
+++ b/tests/xprop/run-test.sh
@@ -2,4 +2,4 @@
set -e
python3 generate.py $@
-make -f run-test.mk
+${MAKE:-make} -f run-test.mk
diff --git a/tests/xprop/test.py b/tests/xprop/test.py
index 84ad0a1f4..a275b0d93 100644
--- a/tests/xprop/test.py
+++ b/tests/xprop/test.py
@@ -47,7 +47,7 @@ if "clean" in steps:
def yosys(command):
- subprocess.check_call(["yosys", "-Qp", command])
+ subprocess.check_call(["../../../yosys", "-Qp", command])
def remove(file):
try:
@@ -275,7 +275,7 @@ if "prepare" in steps:
file=tb_file,
)
- print(" $finish;", file=tb_file)
+ print(" $finish(0);", file=tb_file)
print("end", file=tb_file)
print("endmodule", file=tb_file)
@@ -344,8 +344,8 @@ for mode in ["", "_xprop"]:
read_rtlil wrapped{mode}.il
chformal -remove
dffunmap
- write_verilog -noparallelcase vsim_expr{mode}.v
write_verilog -noexpr vsim_noexpr{mode}.v
+ write_verilog -noparallelcase vsim_expr{mode}.v
"""
)
@@ -357,15 +357,15 @@ for mode in ["", "_xprop"]:
"-DSIMLIB_FF",
"-DSIMLIB_GLOBAL_CLOCK=top.gclk",
f"-DDUMPFILE=\"vsim_{expr}.vcd\"",
+ "-o",
+ f"vsim_{expr}",
"verilog_sim_tb.v",
f"vsim_{expr}.v",
*simlibs,
- "-o",
- f"vsim_{expr}",
]
)
with open(f"vsim_{expr}.out", "w") as f:
- subprocess.check_call([f"./vsim_{expr}"], stdout=f)
+ subprocess.check_call(["vvp", f"./vsim_{expr}"], stdout=f)
for mode in ["", "_xprop"]:
if f"sim{mode}" not in steps: