aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile1
-rw-r--r--backends/btor/btor.cc1
-rw-r--r--backends/firrtl/firrtl.cc1
-rw-r--r--backends/smt2/smt2.cc1
-rw-r--r--backends/smv/smv.cc1
-rw-r--r--backends/verilog/verilog_backend.cc49
-rw-r--r--kernel/calc.cc23
-rw-r--r--kernel/celltypes.h12
-rw-r--r--kernel/rtlil.cc36
-rw-r--r--kernel/rtlil.h9
-rw-r--r--kernel/satgen.cc59
-rw-r--r--passes/cmds/Makefile.inc1
-rw-r--r--passes/cmds/xprop.cc1198
-rw-r--r--passes/opt/opt_expr.cc183
-rw-r--r--passes/sat/formalff.cc2
-rw-r--r--passes/sat/miter.cc14
-rw-r--r--passes/sat/sim.cc27
-rw-r--r--passes/techmap/Makefile.inc1
-rw-r--r--passes/techmap/bwmuxmap.cc70
-rw-r--r--passes/techmap/simplemap.cc46
-rw-r--r--passes/techmap/simplemap.h1
-rw-r--r--techlibs/common/simlib.v68
-rw-r--r--techlibs/common/techmap.v2
-rw-r--r--tests/opt/opt_expr_xnor.ys2
-rw-r--r--tests/opt/opt_expr_xor.ys7
-rw-r--r--tests/xprop/.gitignore2
-rw-r--r--tests/xprop/generate.py278
-rwxr-xr-xtests/xprop/run-test.sh5
-rw-r--r--tests/xprop/test.py516
29 files changed, 2537 insertions, 79 deletions
diff --git a/Makefile b/Makefile
index e8d83c12c..e8af0e77d 100644
--- a/Makefile
+++ b/Makefile
@@ -874,6 +874,7 @@ test: $(TARGETS) $(EXTRA_TARGETS)
+cd tests/rpc && bash run-test.sh
+cd tests/memfile && bash run-test.sh
+cd tests/verilog && bash run-test.sh
+ +cd tests/xprop && bash run-test.sh $(SEEDOPT)
@echo ""
@echo " Passed \"make test\"."
@echo ""
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 06de71018..8368ab82d 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -1417,6 +1417,7 @@ struct BtorBackend : public Backend {
log_push();
Pass::call(design, "bmuxmap");
Pass::call(design, "demuxmap");
+ Pass::call(design, "bwmuxmap");
log_pop();
size_t argidx;
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index 76ba77abb..e483117d1 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -1215,6 +1215,7 @@ struct FirrtlBackend : public Backend {
Pass::call(design, "pmuxtree");
Pass::call(design, "bmuxmap");
Pass::call(design, "demuxmap");
+ Pass::call(design, "bwmuxmap");
namecache.clear();
autoid_counter = 0;
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 7434b13da..fe50ca7f6 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -1744,6 +1744,7 @@ struct Smt2Backend : public Backend {
log_push();
Pass::call(design, "bmuxmap");
Pass::call(design, "demuxmap");
+ Pass::call(design, "bwmuxmap");
log_pop();
size_t argidx;
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index 7d4f94adc..49c2cc7a6 100644
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -744,6 +744,7 @@ struct SmvBackend : public Backend {
log_push();
Pass::call(design, "bmuxmap");
Pass::call(design, "demuxmap");
+ Pass::call(design, "bwmuxmap");
log_pop();
size_t argidx;
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index e60ebc70e..0a9c0590e 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -35,7 +35,7 @@
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
-bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs;
+bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs, noparallelcase;
int auto_name_counter, auto_name_offset, auto_name_digits, extmem_counter;
std::map<RTLIL::IdString, int> auto_name_map;
std::set<RTLIL::IdString> reg_wires;
@@ -1209,7 +1209,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
if (cell->type == ID($modfloor))
{
// wire truncated = $signed(A) % $signed(B);
- // assign Y = (A[-1] == B[-1]) || truncated == 0 ? truncated : $signed(B) + $signed(truncated);
+ // assign Y = (A[-1] == B[-1]) || truncated == 0 ? $signed(truncated) : $signed(B) + $signed(truncated);
if (cell->getParam(ID::A_SIGNED).as_bool() && cell->getParam(ID::B_SIGNED).as_bool()) {
SigSpec sig_a = cell->getPort(ID::A);
@@ -1229,7 +1229,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
dump_sigspec(f, sig_a.extract(sig_a.size()-1));
f << stringf(" == ");
dump_sigspec(f, sig_b.extract(sig_b.size()-1));
- f << stringf(") || %s == 0 ? %s : ", temp_id.c_str(), temp_id.c_str());
+ f << stringf(") || %s == 0 ? $signed(%s) : ", temp_id.c_str(), temp_id.c_str());
dump_cell_expr_port(f, cell, "B", true);
f << stringf(" + $signed(%s);\n", temp_id.c_str());
return true;
@@ -1314,24 +1314,38 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
f << stringf("%s" " input [%d:0] s;\n", indent.c_str(), s_width-1);
dump_attributes(f, indent + " ", cell->attributes);
- if (!noattr)
- f << stringf("%s" " (* parallel_case *)\n", indent.c_str());
- f << stringf("%s" " casez (s)", indent.c_str());
- f << stringf(noattr ? " // synopsys parallel_case\n" : "\n");
+ if (noparallelcase)
+ f << stringf("%s" " case (s)\n", indent.c_str());
+ else {
+ if (!noattr)
+ f << stringf("%s" " (* parallel_case *)\n", indent.c_str());
+ f << stringf("%s" " casez (s)", indent.c_str());
+ f << stringf(noattr ? " // synopsys parallel_case\n" : "\n");
+ }
for (int i = 0; i < s_width; i++)
{
f << stringf("%s" " %d'b", indent.c_str(), s_width);
for (int j = s_width-1; j >= 0; j--)
- f << stringf("%c", j == i ? '1' : '?');
+ f << stringf("%c", j == i ? '1' : noparallelcase ? '0' : '?');
f << stringf(":\n");
f << stringf("%s" " %s = b[%d:%d];\n", indent.c_str(), func_name.c_str(), (i+1)*width-1, i*width);
}
- f << stringf("%s" " default:\n", indent.c_str());
+ if (noparallelcase) {
+ f << stringf("%s" " %d'b", indent.c_str(), s_width);
+ for (int j = s_width-1; j >= 0; j--)
+ f << '0';
+ f << stringf(":\n");
+ } else
+ f << stringf("%s" " default:\n", indent.c_str());
f << stringf("%s" " %s = a;\n", indent.c_str(), func_name.c_str());
+ if (noparallelcase) {
+ f << stringf("%s" " default:\n", indent.c_str());
+ f << stringf("%s" " %s = %d'bx;\n", indent.c_str(), func_name.c_str(), width);
+ }
f << stringf("%s" " endcase\n", indent.c_str());
f << stringf("%s" "endfunction\n", indent.c_str());
@@ -2136,6 +2150,11 @@ struct VerilogBackend : public Backend {
log(" without this option all internal cells are converted to Verilog\n");
log(" expressions.\n");
log("\n");
+ log(" -noparallelcase\n");
+ log(" With this option no parallel_case attributes are used. Instead, a case\n");
+ log(" statement that assigns don't-care values for priority dependent inputs\n");
+ log(" is generated.\n");
+ log("\n");
log(" -siminit\n");
log(" add initial statements with hierarchical refs to initialize FFs when\n");
log(" in -noexpr mode.\n");
@@ -2211,6 +2230,7 @@ struct VerilogBackend : public Backend {
decimal = false;
siminit = false;
simple_lhs = false;
+ noparallelcase = false;
auto_prefix = "";
bool blackboxes = false;
@@ -2246,6 +2266,10 @@ struct VerilogBackend : public Backend {
noexpr = true;
continue;
}
+ if (arg == "-noparallelcase") {
+ noparallelcase = true;
+ continue;
+ }
if (arg == "-nodec") {
nodec = true;
continue;
@@ -2302,8 +2326,11 @@ struct VerilogBackend : public Backend {
}
log_push();
- Pass::call(design, "bmuxmap");
- Pass::call(design, "demuxmap");
+ if (!noexpr) {
+ Pass::call(design, "bmuxmap");
+ Pass::call(design, "demuxmap");
+ Pass::call(design, "bwmuxmap");
+ }
Pass::call(design, "clean_zerowidth");
log_pop();
diff --git a/kernel/calc.cc b/kernel/calc.cc
index 32e8a49fe..9b02a6e30 100644
--- a/kernel/calc.cc
+++ b/kernel/calc.cc
@@ -690,5 +690,28 @@ RTLIL::Const RTLIL::const_demux(const RTLIL::Const &arg1, const RTLIL::Const &ar
return res;
}
+RTLIL::Const RTLIL::const_bweqx(const RTLIL::Const &arg1, const RTLIL::Const &arg2)
+{
+ log_assert(arg2.size() == arg1.size());
+ RTLIL::Const result(RTLIL::State::S0, arg1.size());
+ for (int i = 0; i < arg1.size(); i++)
+ result[i] = arg1[i] == arg2[i] ? State::S1 : State::S0;
+
+ return result;
+}
+
+RTLIL::Const RTLIL::const_bwmux(const RTLIL::Const &arg1, const RTLIL::Const &arg2, const RTLIL::Const &arg3)
+{
+ log_assert(arg2.size() == arg1.size());
+ log_assert(arg3.size() == arg1.size());
+ RTLIL::Const result(RTLIL::State::Sx, arg1.size());
+ for (int i = 0; i < arg1.size(); i++) {
+ if (arg3[i] != State::Sx || arg1[i] == arg2[i])
+ result[i] = arg3[i] == State::S1 ? arg2[i] : arg1[i];
+ }
+
+ return result;
+}
+
YOSYS_NAMESPACE_END
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index e617b4603..63e7408c1 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -116,7 +116,8 @@ struct CellTypes
ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx),
ID($lt), ID($le), ID($eq), ID($ne), ID($eqx), ID($nex), ID($ge), ID($gt),
ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($pow),
- ID($logic_and), ID($logic_or), ID($concat), ID($macc)
+ ID($logic_and), ID($logic_or), ID($concat), ID($macc),
+ ID($bweqx)
};
for (auto type : unary_ops)
@@ -125,7 +126,7 @@ struct CellTypes
for (auto type : binary_ops)
setup_type(type, {ID::A, ID::B}, {ID::Y}, true);
- for (auto type : std::vector<RTLIL::IdString>({ID($mux), ID($pmux)}))
+ for (auto type : std::vector<RTLIL::IdString>({ID($mux), ID($pmux), ID($bwmux)}))
setup_type(type, {ID::A, ID::B, ID::S}, {ID::Y}, true);
for (auto type : std::vector<RTLIL::IdString>({ID($bmux), ID($demux)}))
@@ -430,6 +431,11 @@ struct CellTypes
return const_demux(arg1, arg2);
}
+ if (cell->type == ID($bweqx))
+ {
+ return const_bweqx(arg1, arg2);
+ }
+
if (cell->type == ID($lut))
{
int width = cell->parameters.at(ID::WIDTH).as_int();
@@ -490,6 +496,8 @@ struct CellTypes
{
if (cell->type.in(ID($mux), ID($_MUX_)))
return const_mux(arg1, arg2, arg3);
+ if (cell->type == ID($bwmux))
+ return const_bwmux(arg1, arg2, arg3);
if (cell->type == ID($pmux))
return const_pmux(arg1, arg2, arg3);
if (cell->type == ID($_AOI3_))
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 5211c3b3f..eee014c54 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -1613,6 +1613,23 @@ namespace {
return;
}
+ if (cell->type == ID($bweqx)) {
+ port(ID::A, param(ID::WIDTH));
+ port(ID::B, param(ID::WIDTH));
+ port(ID::Y, param(ID::WIDTH));
+ check_expected();
+ return;
+ }
+
+ if (cell->type == ID($bwmux)) {
+ port(ID::A, param(ID::WIDTH));
+ port(ID::B, param(ID::WIDTH));
+ port(ID::S, param(ID::WIDTH));
+ port(ID::Y, param(ID::WIDTH));
+ check_expected();
+ return;
+ }
+
if (cell->type.in(ID($assert), ID($assume), ID($live), ID($fair), ID($cover))) {
port(ID::A, 1);
port(ID::EN, 1);
@@ -2466,6 +2483,7 @@ DEF_METHOD(Sshr, sig_a.size(), ID($sshr))
return sig_y; \
}
DEF_METHOD(Mux, ID($mux), 0)
+DEF_METHOD(Bwmux, ID($bwmux), 0)
DEF_METHOD(Pmux, ID($pmux), 1)
#undef DEF_METHOD
@@ -2489,6 +2507,24 @@ DEF_METHOD(Bmux, ID($bmux), 0)
DEF_METHOD(Demux, ID($demux), 1)
#undef DEF_METHOD
+#define DEF_METHOD(_func, _type) \
+ RTLIL::Cell* RTLIL::Module::add ## _func(RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_y, const std::string &src) { \
+ RTLIL::Cell *cell = addCell(name, _type); \
+ cell->parameters[ID::WIDTH] = sig_a.size(); \
+ cell->setPort(ID::A, sig_a); \
+ cell->setPort(ID::B, sig_b); \
+ cell->setPort(ID::Y, sig_y); \
+ cell->set_src_attribute(src); \
+ return cell; \
+ } \
+ RTLIL::SigSpec RTLIL::Module::_func(RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_s, const std::string &src) { \
+ RTLIL::SigSpec sig_y = addWire(NEW_ID, sig_a.size()); \
+ add ## _func(name, sig_a, sig_s, sig_y, src); \
+ return sig_y; \
+ }
+DEF_METHOD(Bweqx, ID($bweqx))
+#undef DEF_METHOD
+
#define DEF_METHOD_2(_func, _type, _P1, _P2) \
RTLIL::Cell* RTLIL::Module::add ## _func(RTLIL::IdString name, const RTLIL::SigBit &sig1, const RTLIL::SigBit &sig2, const std::string &src) { \
RTLIL::Cell *cell = addCell(name, _type); \
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index 755abf534..42bb66da8 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -505,6 +505,9 @@ namespace RTLIL
RTLIL::Const const_bmux (const RTLIL::Const &arg1, const RTLIL::Const &arg2);
RTLIL::Const const_demux (const RTLIL::Const &arg1, const RTLIL::Const &arg2);
+ RTLIL::Const const_bweqx (const RTLIL::Const &arg1, const RTLIL::Const &arg2);
+ RTLIL::Const const_bwmux (const RTLIL::Const &arg1, const RTLIL::Const &arg2, const RTLIL::Const &arg3);
+
// This iterator-range-pair is used for Design::modules(), Module::wires() and Module::cells().
// It maintains a reference counter that is used to make sure that the container is not modified while being iterated over.
@@ -1303,6 +1306,9 @@ public:
RTLIL::Cell* addBmux (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_s, const RTLIL::SigSpec &sig_y, const std::string &src = "");
RTLIL::Cell* addDemux (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_s, const RTLIL::SigSpec &sig_y, const std::string &src = "");
+ RTLIL::Cell* addBweqx (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_y, const std::string &src = "");
+ RTLIL::Cell* addBwmux (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_s, const RTLIL::SigSpec &sig_y, const std::string &src = "");
+
RTLIL::Cell* addSlice (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_y, RTLIL::Const offset, const std::string &src = "");
RTLIL::Cell* addConcat (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_y, const std::string &src = "");
RTLIL::Cell* addLut (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_y, RTLIL::Const lut, const std::string &src = "");
@@ -1432,6 +1438,9 @@ public:
RTLIL::SigSpec Bmux (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_s, const std::string &src = "");
RTLIL::SigSpec Demux (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_s, const std::string &src = "");
+ RTLIL::SigSpec Bweqx (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const std::string &src = "");
+ RTLIL::SigSpec Bwmux (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_s, const std::string &src = "");
+
RTLIL::SigBit BufGate (RTLIL::IdString name, const RTLIL::SigBit &sig_a, const std::string &src = "");
RTLIL::SigBit NotGate (RTLIL::IdString name, const RTLIL::SigBit &sig_a, const std::string &src = "");
RTLIL::SigBit AndGate (RTLIL::IdString name, const RTLIL::SigBit &sig_a, const RTLIL::SigBit &sig_b, const std::string &src = "");
diff --git a/kernel/satgen.cc b/kernel/satgen.cc
index 2a1fd1711..3a2fa4735 100644
--- a/kernel/satgen.cc
+++ b/kernel/satgen.cc
@@ -223,7 +223,33 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
return true;
}
- if (cell->type.in(ID($_MUX_), ID($mux), ID($_NMUX_)))
+ if (cell->type == ID($bweqx))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+
+ std::vector<int> bweqx = ez->vec_not(ez->vec_xor(a, b));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+
+ std::vector<int> both_undef = ez->vec_and(undef_a, undef_b);
+ std::vector<int> both_def = ez->vec_and(ez->vec_not(undef_a), ez->vec_not(undef_b));
+
+ bweqx = ez->vec_or(both_undef, ez->vec_and(both_def, bweqx));
+
+ for (int yx : undef_y)
+ ez->assume(ez->NOT(yx));
+ }
+ ez->assume(ez->vec_eq(bweqx, y));
+ return true;
+ }
+
+ if (cell->type.in(ID($_MUX_), ID($mux), ID($_NMUX_), ID($bwmux)))
{
std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
@@ -233,6 +259,8 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
if (cell->type == ID($_NMUX_))
ez->assume(ez->vec_eq(ez->vec_not(ez->vec_ite(s.at(0), b, a)), yy));
+ else if (cell->type == ID($bwmux))
+ ez->assume(ez->vec_eq(ez->vec_ite(s, b, a), yy));
else
ez->assume(ez->vec_eq(ez->vec_ite(s.at(0), b, a), yy));
@@ -245,7 +273,11 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
std::vector<int> unequal_ab = ez->vec_not(ez->vec_iff(a, b));
std::vector<int> undef_ab = ez->vec_or(unequal_ab, ez->vec_or(undef_a, undef_b));
- std::vector<int> yX = ez->vec_ite(undef_s.at(0), undef_ab, ez->vec_ite(s.at(0), undef_b, undef_a));
+ std::vector<int> yX;
+ if (cell->type == ID($bwmux))
+ yX = ez->vec_ite(undef_s, undef_ab, ez->vec_ite(s, undef_b, undef_a));
+ else
+ yX = ez->vec_ite(undef_s.at(0), undef_ab, ez->vec_ite(s.at(0), undef_b, undef_a));
ez->assume(ez->vec_eq(yX, undef_y));
undefGating(y, yy, undef_y);
}
@@ -375,29 +407,24 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
std::vector<int> undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- int maybe_a = ez->CONST_TRUE;
+ int all_undef = ez->CONST_FALSE;
+ int found_active = ez->CONST_FALSE;
- std::vector<int> bits_set = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
- std::vector<int> bits_clr = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
+ std::vector<int> undef_tmp = undef_a;
for (size_t i = 0; i < s.size(); i++)
{
- std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
std::vector<int> part_of_undef_b(undef_b.begin()+i*a.size(), undef_b.begin()+(i+1)*a.size());
- int maybe_s = ez->OR(s.at(i), undef_s.at(i));
- int sure_s = ez->AND(s.at(i), ez->NOT(undef_s.at(i)));
-
- maybe_a = ez->AND(maybe_a, ez->NOT(sure_s));
-
- bits_set = ez->vec_ite(maybe_s, ez->vec_or(bits_set, ez->vec_or(part_of_b, part_of_undef_b)), bits_set);
- bits_clr = ez->vec_ite(maybe_s, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b)), bits_clr);
+ undef_tmp = ez->vec_ite(s.at(i), part_of_undef_b, undef_tmp);
+ all_undef = ez->OR(all_undef, undef_s.at(i));
+ all_undef = ez->OR(all_undef, ez->AND(s.at(i), found_active));
+ found_active = ez->OR(found_active, s.at(i));
}
- bits_set = ez->vec_ite(maybe_a, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(a, undef_a))), bits_set);
- bits_clr = ez->vec_ite(maybe_a, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(a), undef_a))), bits_clr);
+ undef_tmp = ez->vec_or(undef_tmp, std::vector<int>(a.size(), all_undef));
- ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(bits_set, bits_clr)), undef_y));
+ ez->assume(ez->vec_eq(undef_tmp, undef_y));
undefGating(y, yy, undef_y);
}
return true;
diff --git a/passes/cmds/Makefile.inc b/passes/cmds/Makefile.inc
index 16a38b511..8c7a18d02 100644
--- a/passes/cmds/Makefile.inc
+++ b/passes/cmds/Makefile.inc
@@ -43,3 +43,4 @@ OBJS += passes/cmds/logger.o
OBJS += passes/cmds/printattrs.o
OBJS += passes/cmds/sta.o
OBJS += passes/cmds/clean_zerowidth.o
+OBJS += passes/cmds/xprop.o
diff --git a/passes/cmds/xprop.cc b/passes/cmds/xprop.cc
new file mode 100644
index 000000000..c2a1b5c44
--- /dev/null
+++ b/passes/cmds/xprop.cc
@@ -0,0 +1,1198 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one>
+ *
+ * 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/celltypes.h"
+#include "kernel/ffinit.h"
+#include "kernel/ff.h"
+#include "kernel/modtools.h"
+#include "kernel/sigtools.h"
+#include "kernel/utils.h"
+#include "kernel/yosys.h"
+#include <deque>
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct XpropOptions
+{
+ bool split_inputs = false;
+ bool split_outputs = false;
+ bool assume_encoding = false;
+ bool assert_encoding = false;
+ bool assume_def_inputs = false;
+ bool required = false;
+ bool formal = false;
+ bool debug_asserts = false;
+};
+
+struct XpropWorker
+{
+ struct EncodedBit {
+ SigBit is_0, is_1, is_x;
+ bool driven;
+ };
+
+ struct EncodedSig {
+ SigSpec is_0, is_1, is_x;
+ Module *module;
+
+ void invert() { std::swap(is_0, is_1); }
+ void auto_0() { connect_0(module->Not(NEW_ID, module->Or(NEW_ID, is_1, is_x))); }
+ void auto_1() { connect_1(module->Not(NEW_ID, module->Or(NEW_ID, is_0, is_x))); }
+ void auto_x() { connect_x(module->Not(NEW_ID, module->Or(NEW_ID, is_0, is_1))); }
+
+ void connect_0(SigSpec sig) { module->connect(is_0, sig); }
+ void connect_1(SigSpec sig) { module->connect(is_1, sig); }
+ void connect_x(SigSpec sig) { module->connect(is_x, sig); }
+
+ void connect_1_under_x(SigSpec sig) { connect_1(module->And(NEW_ID, sig, module->Not(NEW_ID, is_x))); }
+ void connect_0_under_x(SigSpec sig) { connect_0(module->And(NEW_ID, sig, module->Not(NEW_ID, is_x))); }
+
+ void connect_x_under_0(SigSpec sig) { connect_x(module->And(NEW_ID, sig, module->Not(NEW_ID, is_0))); }
+
+ void connect_as_bool() {
+ int width = GetSize(is_0);
+ if (width <= 1)
+ return;
+ module->connect(is_0.extract(1, width - 1), Const(State::S1, width - 1));
+ module->connect(is_1.extract(1, width - 1), Const(State::S0, width - 1));
+ module->connect(is_x.extract(1, width - 1), Const(State::S0, width - 1));
+ is_0 = is_0[0];
+ is_1 = is_1[0];
+ is_x = is_x[0];
+ }
+
+ int size() const { return is_0.size(); }
+ };
+
+ Module *module;
+ XpropOptions options;
+ ModWalker modwalker;
+ SigMap &sigmap;
+ FfInitVals initvals;
+
+ pool<SigBit> maybe_x_bits;
+ dict<SigBit, EncodedBit> encoded_bits;
+
+ pool<Cell *> pending_cells;
+ std::deque<Cell *> pending_cell_queue;
+
+ XpropWorker(Module *module, XpropOptions options) :
+ module(module), options(options),
+ modwalker(module->design), sigmap(modwalker.sigmap)
+ {
+ modwalker.setup(module);
+ initvals.set(&modwalker.sigmap, module);
+
+ maybe_x_bits.insert(State::Sx);
+
+ for (auto cell : module->cells()) {
+ pending_cells.insert(cell);
+ pending_cell_queue.push_back(cell);
+ }
+
+ if (!options.assume_def_inputs) {
+ for (auto port : module->ports) {
+ auto wire = module->wire(port);
+ if (wire->port_input)
+ mark_maybe_x(SigSpec(wire));
+ }
+ }
+ }
+
+ bool maybe_x(SigBit bit)
+ {
+ return maybe_x_bits.count(sigmap(bit));
+ }
+
+ bool maybe_x(const SigSpec &sig)
+ {
+ for (auto bit : sig)
+ if (maybe_x(bit)) return true;
+ return false;
+ }
+
+ bool ports_maybe_x(Cell *cell)
+ {
+ for (auto &conn : cell->connections())
+ if (maybe_x(conn.second))
+ return true;
+ return false;
+ }
+
+ bool inputs_maybe_x(Cell *cell)
+ {
+ for (auto &conn : cell->connections())
+ if (cell->input(conn.first) && maybe_x(conn.second))
+ return true;
+ return false;
+ }
+
+ void mark_maybe_x(SigBit bit)
+ {
+ sigmap.apply(bit);
+ if (!maybe_x_bits.insert(bit).second)
+ return;
+ auto it = modwalker.signal_consumers.find(bit);
+ if (it == modwalker.signal_consumers.end())
+ return;
+ for (auto &consumer : it->second)
+ if (pending_cells.insert(consumer.cell).second)
+ pending_cell_queue.push_back(consumer.cell);
+ }
+
+ void mark_maybe_x(const SigSpec &sig)
+ {
+ for (auto bit : sig)
+ mark_maybe_x(bit);
+ }
+
+ void mark_outputs_maybe_x(Cell *cell)
+ {
+ for (auto &conn : cell->connections())
+ if (cell->output(conn.first))
+ mark_maybe_x(conn.second);
+ }
+
+ EncodedSig encoded(SigSpec sig, bool driving = false)
+ {
+ EncodedSig result;
+ SigSpec invert;
+
+ if (driving)
+ result.module = module;
+
+ int new_bits = 0;
+
+ sigmap.apply(sig);
+
+ for (auto bit : sig) {
+ if (!bit.is_wire())
+ continue;
+ else if (!maybe_x(bit) && !driving)
+ invert.append(bit);
+ else if (!encoded_bits.count(bit)) {
+ new_bits += 1;
+ encoded_bits.emplace(bit, {
+ State::Sm, State::Sm, State::Sm, false
+ });
+ }
+ }
+
+ if (!invert.empty() && !driving)
+ invert = module->Not(NEW_ID, invert);
+
+ EncodedSig new_sigs;
+ if (new_bits > 0) {
+ new_sigs.is_0 = module->addWire(NEW_ID, new_bits);
+ new_sigs.is_1 = module->addWire(NEW_ID, new_bits);
+ new_sigs.is_x = module->addWire(NEW_ID, new_bits);
+ }
+
+ int invert_pos = 0;
+ int new_pos = 0;
+
+ SigSpec driven_orig;
+ EncodedSig driven_enc;
+ SigSig driven_never_x;
+
+ for (auto bit : sig)
+ {
+ if (!bit.is_wire()) {
+ result.is_0.append(bit == State::S0 ? State::S1 : State::S0);
+ result.is_1.append(bit == State::S1 ? State::S1 : State::S0);
+ result.is_x.append(bit == State::Sx ? State::S1 : State::S0);
+ continue;
+ } else if (!maybe_x(bit) && !driving) {
+ result.is_0.append(invert[invert_pos++]);
+ result.is_1.append(bit);
+ result.is_x.append(State::S0);
+ continue;
+ }
+ auto &enc = encoded_bits.at(bit);
+ if (enc.is_0 == State::Sm) {
+ enc.is_0 = new_sigs.is_0[new_pos];
+ enc.is_1 = new_sigs.is_1[new_pos];
+ enc.is_x = new_sigs.is_x[new_pos];
+ new_pos++;
+ }
+ if (driving) {
+ log_assert(!enc.driven);
+ enc.driven = true;
+ if (maybe_x(bit)) {
+ driven_orig.append(bit);
+ driven_enc.is_0.append(enc.is_0);
+ driven_enc.is_1.append(enc.is_1);
+ driven_enc.is_x.append(enc.is_x);
+ } else {
+ driven_never_x.first.append(bit);
+ driven_never_x.second.append(enc.is_1);
+ }
+ }
+ result.is_0.append(enc.is_0);
+ result.is_1.append(enc.is_1);
+ result.is_x.append(enc.is_x);
+ }
+
+ if (!driven_orig.empty()) {
+ module->addBwmux(NEW_ID, driven_enc.is_1, Const(State::Sx, GetSize(driven_orig)), driven_enc.is_x, driven_orig);
+ }
+ if (!driven_never_x.first.empty()) {
+ module->connect(driven_never_x);
+ }
+
+ if (driving && (options.assert_encoding || options.assume_encoding)) {
+ auto not_0 = module->Not(NEW_ID, result.is_0);
+ auto not_1 = module->Not(NEW_ID, result.is_1);
+ auto not_x = module->Not(NEW_ID, result.is_x);
+ auto valid = module->ReduceAnd(NEW_ID, {
+ module->Eq(NEW_ID, result.is_0, module->And(NEW_ID, not_1, not_x)),
+ module->Eq(NEW_ID, result.is_1, module->And(NEW_ID, not_0, not_x)),
+ module->Eq(NEW_ID, result.is_x, module->And(NEW_ID, not_0, not_1)),
+ });
+ if (options.assert_encoding)
+ module->addAssert(NEW_ID_SUFFIX("xprop_enc"), valid, State::S1);
+ else
+ module->addAssume(NEW_ID_SUFFIX("xprop_enc"), valid, State::S1);
+ if (options.debug_asserts) {
+ auto bad_bits = module->Bweqx(NEW_ID, {result.is_0, result.is_1, result.is_x}, Const(State::Sx, GetSize(result) * 3));
+ module->addAssert(NEW_ID_SUFFIX("xprop_debug"), module->LogicNot(NEW_ID, bad_bits), State::S1);
+ }
+ }
+
+ return result;
+ }
+
+ void mark_all_maybe_x()
+ {
+ while (!pending_cell_queue.empty()) {
+ Cell *cell = pending_cell_queue.front();
+ pending_cell_queue.pop_front();
+ pending_cells.erase(cell);
+
+ mark_maybe_x(cell);
+ }
+ }
+
+ void mark_maybe_x(Cell *cell) {
+ if (cell->type.in(ID($bweqx), ID($eqx), ID($nex), ID($initstate), ID($assert), ID($assume), ID($cover), ID($anyseq), ID($anyconst)))
+ return;
+
+ if (cell->type.in(ID($pmux))) {
+ mark_outputs_maybe_x(cell);
+ return;
+ }
+
+ if (RTLIL::builtin_ff_cell_types().count(cell->type) || cell->type == ID($anyinit)) {
+ FfData ff(&initvals, cell);
+
+ if (cell->type != ID($anyinit))
+ for (int i = 0; i < ff.width; i++)
+ if (ff.val_init[i] == State::Sx)
+ mark_maybe_x(ff.sig_q[i]);
+
+ for (int i = 0; i < ff.width; i++)
+ if (maybe_x(ff.sig_d[i]))
+ mark_maybe_x(ff.sig_q[i]);
+
+ if ((ff.has_clk || ff.has_gclk) && !ff.has_ce && !ff.has_aload && !ff.has_srst && !ff.has_arst && !ff.has_sr)
+ return;
+ }
+
+ if (cell->type == ID($not)) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto sig_a = cell->getPort(ID::A); sig_a.extend_u0(GetSize(sig_y), cell->getParam(ID::A_SIGNED).as_bool());
+ for (int i = 0; i < GetSize(sig_y); i++)
+ if (maybe_x(sig_a[i]))
+ mark_maybe_x(sig_y[i]);
+ return;
+ }
+
+ if (cell->type.in(ID($and), ID($or), ID($xor), ID($xnor))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto sig_a = cell->getPort(ID::A); sig_a.extend_u0(GetSize(sig_y), cell->getParam(ID::A_SIGNED).as_bool());
+ auto sig_b = cell->getPort(ID::B); sig_b.extend_u0(GetSize(sig_y), cell->getParam(ID::B_SIGNED).as_bool());
+ for (int i = 0; i < GetSize(sig_y); i++)
+ if (maybe_x(sig_a[i]) || maybe_x(sig_b[i]))
+ mark_maybe_x(sig_y[i]);
+ return;
+ }
+
+ if (cell->type.in(ID($bwmux))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto &sig_a = cell->getPort(ID::A);
+ auto &sig_b = cell->getPort(ID::B);
+ auto &sig_s = cell->getPort(ID::S);
+ for (int i = 0; i < GetSize(sig_y); i++)
+ if (maybe_x(sig_a[i]) || maybe_x(sig_b[i]) || maybe_x(sig_s[i]))
+ mark_maybe_x(sig_y[i]);
+ return;
+ }
+
+ if (cell->type.in(ID($_MUX_), ID($mux), ID($bmux))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto &sig_a = cell->getPort(ID::A);
+ auto &sig_b = cell->getPort(ID::B);
+ auto &sig_s = cell->getPort(ID::S);
+ if (maybe_x(sig_s)) {
+ mark_maybe_x(sig_y);
+ return;
+ }
+ for (int i = 0; i < GetSize(sig_y); i++) {
+ if (maybe_x(sig_a[i])) {
+ mark_maybe_x(sig_y[i]);
+ continue;
+ }
+ for (int j = i; j < GetSize(sig_b); j += GetSize(sig_y)) {
+ if (maybe_x(sig_b[j])) {
+ mark_maybe_x(sig_y[i]);
+ break;
+ }
+ }
+ }
+ return;
+ }
+
+ if (cell->type.in(ID($demux))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto &sig_a = cell->getPort(ID::A);
+ auto &sig_s = cell->getPort(ID::S);
+ if (maybe_x(sig_s)) {
+ mark_maybe_x(sig_y);
+ return;
+ }
+ for (int i = 0; i < GetSize(sig_a); i++)
+ if (maybe_x(sig_a[i]))
+ for (int j = i; j < GetSize(sig_y); j += GetSize(sig_a))
+ mark_maybe_x(sig_y[j]);
+ return;
+ }
+
+ if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift))) {
+ auto &sig_b = cell->getPort(ID::B);
+ auto &sig_y = cell->getPort(ID::Y);
+
+ if (maybe_x(sig_b)) {
+ mark_maybe_x(sig_y);
+ return;
+ }
+
+ auto &sig_a = cell->getPort(ID::A);
+
+ if (maybe_x(sig_a)) {
+ // We could be more precise for shifts, but that's not required
+ // for correctness, so let's keep it simple
+ mark_maybe_x(sig_y);
+ return;
+ }
+ return;
+ }
+
+ if (cell->type.in(ID($shiftx))) {
+ auto &sig_b = cell->getPort(ID::B);
+ auto &sig_y = cell->getPort(ID::Y);
+
+ if (cell->getParam(ID::B_SIGNED).as_bool() || GetSize(sig_b) >= 30) {
+ mark_maybe_x(sig_y);
+ } else {
+ int max_shift = (1 << GetSize(sig_b)) - 1;
+
+ auto &sig_a = cell->getPort(ID::A);
+
+ for (int i = 0; i < GetSize(sig_y); i++)
+ if (i + max_shift >= GetSize(sig_a))
+ mark_maybe_x(sig_y[i]);
+ }
+
+ if (maybe_x(sig_b)) {
+ mark_maybe_x(sig_y);
+ return;
+ }
+
+ auto &sig_a = cell->getPort(ID::A);
+ if (maybe_x(sig_a)) {
+ // We could be more precise for shifts, but that's not required
+ // for correctness, so let's keep it simple
+ mark_maybe_x(sig_y);
+ return;
+ }
+ return;
+ }
+
+ if (cell->type.in(ID($add), ID($sub), ID($mul), ID($neg))) {
+ if (inputs_maybe_x(cell))
+ mark_outputs_maybe_x(cell);
+ return;
+ }
+
+ if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor))) {
+ mark_outputs_maybe_x(cell);
+ return;
+ }
+
+ if (cell->type.in(
+ ID($le), ID($lt), ID($ge), ID($gt),
+ ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_xnor),
+ ID($reduce_bool), ID($logic_not), ID($logic_or), ID($logic_and),
+ ID($eq), ID($ne),
+
+ ID($_NOT_), ID($_AND_), ID($_NAND_), ID($_ANDNOT_), ID($_OR_), ID($_NOR_), ID($_ORNOT_), ID($_XOR_), ID($_XNOR_)
+ )) {
+ auto &sig_y = cell->getPort(ID::Y);
+ if (inputs_maybe_x(cell))
+ mark_maybe_x(sig_y[0]);
+ return;
+ }
+
+ log_warning("Unhandled cell %s (%s) during maybe-x marking\n", log_id(cell), log_id(cell->type));
+ mark_outputs_maybe_x(cell);
+ }
+
+ void process_cells()
+ {
+ for (auto cell : module->selected_cells())
+ process_cell(cell);
+ }
+
+ void process_cell(Cell *cell)
+ {
+ if (!ports_maybe_x(cell)) {
+
+ if (cell->type == ID($bweq)) {
+ auto sig_y = cell->getPort(ID::Y);
+ auto sig_a = cell->getPort(ID::A);
+ auto sig_b = cell->getPort(ID::B);
+
+ auto name = cell->name;
+ module->remove(cell);
+ module->addXnor(name, sig_a, sig_b, sig_y);
+ return;
+ }
+
+ if (cell->type.in(ID($nex), ID($eqx))) {
+ auto sig_y = cell->getPort(ID::Y);
+ auto sig_a = cell->getPort(ID::A);
+ auto sig_b = cell->getPort(ID::B);
+
+ auto name = cell->name;
+ module->remove(cell);
+ if (cell->type == ID($eqx))
+ module->addEq(name, sig_a, sig_b, sig_y);
+ else
+ module->addNe(name, sig_a, sig_b, sig_y);
+ return;
+ }
+
+ return;
+ }
+
+ if (cell->type.in(ID($not), ID($_NOT_))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto sig_a = cell->getPort(ID::A);
+ if (cell->type == ID($not))
+ sig_a.extend_u0(GetSize(sig_y), cell->getParam(ID::A_SIGNED).as_bool());
+
+ auto enc_a = encoded(sig_a);
+ auto enc_y = encoded(sig_y, true);
+
+ enc_y.connect_x(enc_a.is_x);
+ enc_y.connect_0(enc_a.is_1);
+ enc_y.connect_1(enc_a.is_0);
+
+ module->remove(cell);
+ return;
+ }
+
+ if (cell->type.in(ID($and), ID($or), ID($_AND_), ID($_OR_), ID($_NAND_), ID($_NOR_), ID($_ANDNOT_), ID($_ORNOT_))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto sig_a = cell->getPort(ID::A);
+ auto sig_b = cell->getPort(ID::B);
+ if (cell->type.in(ID($and), ID($or))) {
+ sig_a.extend_u0(GetSize(sig_y), cell->getParam(ID::A_SIGNED).as_bool());
+ sig_b.extend_u0(GetSize(sig_y), cell->getParam(ID::B_SIGNED).as_bool());
+ }
+
+ auto enc_a = encoded(sig_a);
+ auto enc_b = encoded(sig_b);
+ auto enc_y = encoded(sig_y, true);
+
+ if (cell->type.in(ID($or), ID($_OR_)))
+ enc_a.invert(), enc_b.invert(), enc_y.invert();
+ if (cell->type.in(ID($_NAND_), ID($_NOR_)))
+ enc_y.invert();
+ if (cell->type.in(ID($_ANDNOT_), ID($_ORNOT_)))
+ enc_b.invert();
+
+ enc_y.connect_0(module->Or(NEW_ID, enc_a.is_0, enc_b.is_0));
+ enc_y.connect_1(module->And(NEW_ID, enc_a.is_1, enc_b.is_1));
+ enc_y.auto_x();
+ module->remove(cell);
+ return;
+ }
+
+ if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool), ID($logic_not))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto &sig_a = cell->getPort(ID::A);
+
+ auto enc_a = encoded(sig_a);
+ auto enc_y = encoded(sig_y, true);
+
+ enc_y.connect_as_bool();
+
+ if (cell->type.in(ID($reduce_or), ID($reduce_bool)))
+ enc_a.invert(), enc_y.invert();
+ if (cell->type == ID($logic_not))
+ enc_a.invert();
+
+ enc_y.connect_0(module->ReduceOr(NEW_ID, enc_a.is_0));
+ enc_y.connect_1(module->ReduceAnd(NEW_ID, enc_a.is_1));
+ enc_y.auto_x();
+ module->remove(cell);
+
+ return;
+ }
+
+ if (cell->type.in(ID($reduce_xor), ID($reduce_xnor))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto &sig_a = cell->getPort(ID::A);
+
+ auto enc_a = encoded(sig_a);
+ auto enc_y = encoded(sig_y, true);
+
+ enc_y.connect_as_bool();
+ if (cell->type == ID($reduce_xnor))
+ enc_y.invert();
+
+
+ enc_y.connect_x(module->ReduceOr(NEW_ID, enc_a.is_x));
+ enc_y.connect_1_under_x(module->ReduceXor(NEW_ID, enc_a.is_1));
+ enc_y.auto_0();
+ module->remove(cell);
+
+ return;
+ }
+
+ if (cell->type.in(ID($logic_and), ID($logic_or))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto &sig_a = cell->getPort(ID::A);
+ auto &sig_b = cell->getPort(ID::B);
+
+ auto enc_a = encoded(sig_a);
+ auto enc_b = encoded(sig_b);
+ auto enc_y = encoded(sig_y, true);
+
+ enc_y.connect_as_bool();
+
+ auto a_is_1 = module->ReduceOr(NEW_ID, enc_a.is_1);
+ auto a_is_0 = module->ReduceAnd(NEW_ID, enc_a.is_0);
+ auto b_is_1 = module->ReduceOr(NEW_ID, enc_b.is_1);
+ auto b_is_0 = module->ReduceAnd(NEW_ID, enc_b.is_0);
+
+ if (cell->type == ID($logic_or))
+ enc_y.invert(), std::swap(a_is_0, a_is_1), std::swap(b_is_0, b_is_1);
+
+ enc_y.connect_0(module->Or(NEW_ID, a_is_0, b_is_0));
+ enc_y.connect_1(module->And(NEW_ID, a_is_1, b_is_1));
+ enc_y.auto_x();
+ module->remove(cell);
+ return;
+ }
+
+ if (cell->type.in(ID($xor), ID($xnor), ID($_XOR_), ID($_XNOR_))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto sig_a = cell->getPort(ID::A);
+ auto sig_b = cell->getPort(ID::B);
+ if (cell->type.in(ID($xor), ID($xnor))) {
+ sig_a.extend_u0(GetSize(sig_y), cell->getParam(ID::A_SIGNED).as_bool());
+ sig_b.extend_u0(GetSize(sig_y), cell->getParam(ID::B_SIGNED).as_bool());
+ }
+
+ auto enc_a = encoded(sig_a);
+ auto enc_b = encoded(sig_b);
+ auto enc_y = encoded(sig_y, true);
+
+ if (cell->type.in(ID($xnor), ID($_XNOR_)))
+ enc_y.invert();
+
+ enc_y.connect_x(module->Or(NEW_ID, enc_a.is_x, enc_b.is_x));
+ enc_y.connect_1_under_x(module->Xor(NEW_ID, enc_a.is_1, enc_b.is_1));
+ enc_y.auto_0();
+ module->remove(cell);
+ return;
+ }
+
+ if (cell->type.in(ID($eq), ID($ne))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto sig_a = cell->getPort(ID::A);
+ auto sig_b = cell->getPort(ID::B);
+ int width = std::max(GetSize(sig_a), GetSize(sig_b));
+ sig_a.extend_u0(width, cell->getParam(ID::A_SIGNED).as_bool());
+ sig_b.extend_u0(width, cell->getParam(ID::B_SIGNED).as_bool());
+
+ auto enc_a = encoded(sig_a);
+ auto enc_b = encoded(sig_b);
+ auto enc_y = encoded(sig_y, true);
+ enc_y.connect_as_bool();
+
+ if (cell->type == ID($ne))
+ enc_y.invert();
+
+ auto delta = module->Xor(NEW_ID, enc_a.is_1, enc_b.is_1);
+ auto xpos = module->Or(NEW_ID, enc_a.is_x, enc_b.is_x);
+
+ enc_y.connect_0(module->ReduceOr(NEW_ID, module->And(NEW_ID, delta, module->Not(NEW_ID, xpos))));
+ enc_y.connect_x_under_0(module->ReduceOr(NEW_ID, xpos));
+ enc_y.auto_1();
+ module->remove(cell);
+ return;
+ }
+
+ if (cell->type.in(ID($eqx), ID($nex))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto sig_a = cell->getPort(ID::A);
+ auto sig_b = cell->getPort(ID::B);
+ int width = std::max(GetSize(sig_a), GetSize(sig_b));
+ sig_a.extend_u0(width, cell->getParam(ID::A_SIGNED).as_bool());
+ sig_b.extend_u0(width, cell->getParam(ID::B_SIGNED).as_bool());
+
+ auto enc_a = encoded(sig_a);
+ auto enc_b = encoded(sig_b);
+
+ auto delta_0 = module->Xnor(NEW_ID, enc_a.is_0, enc_b.is_0);
+ auto delta_1 = module->Xnor(NEW_ID, enc_a.is_1, enc_b.is_1);
+
+ auto eq = module->ReduceAnd(NEW_ID, {delta_0, delta_1});
+
+ auto res = cell->type == ID($nex) ? module->Not(NEW_ID, eq) : eq;
+
+ module->connect(sig_y[0], res);
+ if (GetSize(sig_y) > 1)
+ module->connect(sig_y.extract(1, GetSize(sig_y) - 1), Const(State::S0, GetSize(sig_y) - 1));
+ module->remove(cell);
+ return;
+ }
+
+ if (cell->type.in(ID($bweqx))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto &sig_a = cell->getPort(ID::A);
+ auto &sig_b = cell->getPort(ID::B);
+
+ auto enc_a = encoded(sig_a);
+ auto enc_b = encoded(sig_b);
+
+ auto delta_0 = module->Xnor(NEW_ID, enc_a.is_0, enc_b.is_0);
+ auto delta_1 = module->Xnor(NEW_ID, enc_a.is_1, enc_b.is_1);
+ module->addAnd(NEW_ID, delta_0, delta_1, sig_y);
+ module->remove(cell);
+ return;
+ }
+
+ if (cell->type.in(ID($_MUX_), ID($mux), ID($bwmux))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto &sig_a = cell->getPort(ID::A);
+ auto &sig_b = cell->getPort(ID::B);
+ auto sig_s = cell->getPort(ID::S);
+
+ if (cell->type == ID($mux))
+ sig_s = SigSpec(sig_s[0], GetSize(sig_y));
+
+ auto enc_a = encoded(sig_a);
+ auto enc_b = encoded(sig_b);
+ auto enc_s = encoded(sig_s);
+ auto enc_y = encoded(sig_y, true);
+
+ enc_y.connect_1(module->And(NEW_ID,
+ module->Or(NEW_ID, enc_a.is_1, enc_s.is_1),
+ module->Or(NEW_ID, enc_b.is_1, enc_s.is_0)));
+ enc_y.connect_0(module->And(NEW_ID,
+ module->Or(NEW_ID, enc_a.is_0, enc_s.is_1),
+ module->Or(NEW_ID, enc_b.is_0, enc_s.is_0)));
+ enc_y.auto_x();
+ module->remove(cell);
+ return;
+ }
+
+ if (cell->type.in(ID($pmux))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto &sig_a = cell->getPort(ID::A);
+ auto &sig_b = cell->getPort(ID::B);
+ auto &sig_s = cell->getPort(ID::S);
+
+ auto enc_a = encoded(sig_a);
+ auto enc_b = encoded(sig_b);
+ auto enc_s = encoded(sig_s);
+ auto enc_y = encoded(sig_y, true);
+
+ int width = GetSize(enc_y);
+
+ auto all_x = module->ReduceOr(NEW_ID, {
+ enc_s.is_x,
+ module->And(NEW_ID, enc_s.is_1, module->Sub(NEW_ID, enc_s.is_1, Const(1, width)))
+ });
+
+ auto selected = enc_a;
+
+ for (int i = 0; i < GetSize(enc_s); i++) {
+ auto sel_bit = enc_s.is_1[i];
+ selected.is_0 = module->Mux(NEW_ID, selected.is_0, enc_b.is_0.extract(i * width, width), sel_bit);
+ selected.is_1 = module->Mux(NEW_ID, selected.is_1, enc_b.is_1.extract(i * width, width), sel_bit);
+ selected.is_x = module->Mux(NEW_ID, selected.is_x, enc_b.is_x.extract(i * width, width), sel_bit);
+ }
+
+ enc_y.connect_0(module->Mux(NEW_ID, selected.is_0, Const(State::S0, width), all_x));
+ enc_y.connect_1(module->Mux(NEW_ID, selected.is_1, Const(State::S0, width), all_x));
+ enc_y.connect_x(module->Mux(NEW_ID, selected.is_x, Const(State::S1, width), all_x));
+
+ module->remove(cell);
+ return;
+ }
+
+ if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx))) {
+ auto &sig_y = cell->getPort(ID::Y);
+ auto &sig_a = cell->getPort(ID::A);
+ auto &sig_b = cell->getPort(ID::B);
+
+ auto enc_a = encoded(sig_a);
+ auto enc_b = encoded(sig_b);
+ auto enc_y = encoded(sig_y, true);
+
+ auto all_x = module->ReduceOr(NEW_ID, enc_b.is_x)[0];
+ auto not_all_x = module->Not(NEW_ID, all_x)[0];
+
+ SigSpec y_not_0 = module->addWire(NEW_ID, GetSize(sig_y));
+ SigSpec y_1 = module->addWire(NEW_ID, GetSize(sig_y));
+ SigSpec y_x = module->addWire(NEW_ID, GetSize(sig_y));
+
+ auto encoded_type = cell->type == ID($shiftx) ? ID($shift) : cell->type;
+
+ if (cell->type == ID($shiftx)) {
+ std::swap(enc_a.is_0, enc_a.is_x);
+ }
+
+ auto shift_0 = module->addCell(NEW_ID, encoded_type);
+ shift_0->parameters = cell->parameters;
+ shift_0->setPort(ID::A, module->Not(NEW_ID, enc_a.is_0));
+ shift_0->setPort(ID::B, enc_b.is_1);
+ shift_0->setPort(ID::Y, y_not_0);
+
+ auto shift_1 = module->addCell(NEW_ID, encoded_type);
+ shift_1->parameters = cell->parameters;
+ shift_1->setPort(ID::A, enc_a.is_1);
+ shift_1->setPort(ID::B, enc_b.is_1);
+ shift_1->setPort(ID::Y, y_1);
+
+ auto shift_x = module->addCell(NEW_ID, encoded_type);
+ shift_x->parameters = cell->parameters;
+ shift_x->setPort(ID::A, enc_a.is_x);
+ shift_x->setPort(ID::B, enc_b.is_1);
+ shift_x->setPort(ID::Y, y_x);
+
+ SigSpec y_0 = module->Not(NEW_ID, y_not_0);
+
+ if (cell->type == ID($shiftx))
+ std::swap(y_0, y_x);
+
+ enc_y.connect_0(module->And(NEW_ID, y_0, SigSpec(not_all_x, GetSize(sig_y))));
+ enc_y.connect_1(module->And(NEW_ID, y_1, SigSpec(not_all_x, GetSize(sig_y))));
+ enc_y.connect_x(module->Or(NEW_ID, y_x, SigSpec(all_x, GetSize(sig_y))));
+
+ module->remove(cell);
+ return;
+ }
+
+ if (cell->type.in(ID($ff))) {
+ auto &sig_d = cell->getPort(ID::D);
+ auto &sig_q = cell->getPort(ID::Q);
+
+ auto init_q = initvals(sig_q);
+ auto init_q_is_1 = init_q;
+ auto init_q_is_x = init_q;
+
+ for (auto &bit : init_q_is_1)
+ bit = bit == State::S1 ? State::S1 : State::S0;
+ for (auto &bit : init_q_is_x)
+ bit = bit == State::Sx ? State::S1 : State::S0;
+
+ initvals.remove_init(sig_q);
+
+ auto enc_d = encoded(sig_d);
+ auto enc_q = encoded(sig_q, true);
+
+ auto data_q = module->addWire(NEW_ID, GetSize(sig_q));
+
+ module->addFf(NEW_ID, enc_d.is_1, data_q);
+ module->addFf(NEW_ID, enc_d.is_x, enc_q.is_x);
+
+ initvals.set_init(data_q, init_q_is_1);
+ initvals.set_init(enc_q.is_x, init_q_is_x);
+
+ enc_q.connect_1_under_x(data_q);
+ enc_q.auto_0();
+
+ module->remove(cell);
+ return;
+ }
+
+ if (RTLIL::builtin_ff_cell_types().count(cell->type) || cell->type == ID($anyinit)) {
+ FfData ff(&initvals, cell);
+
+ if ((ff.has_clk || ff.has_gclk) && !ff.has_ce && !ff.has_aload && !ff.has_srst && !ff.has_arst && !ff.has_sr) {
+ if (ff.has_clk && maybe_x(ff.sig_clk)) {
+ log_warning("Only non-x CLK inputs are currently supported for %s (%s)\n", log_id(cell), log_id(cell->type));
+ } else {
+ auto init_q = ff.val_init;
+ auto init_q_is_1 = init_q;
+ auto init_q_is_x = init_q;
+
+ if (ff.is_anyinit) {
+ for (auto &bit : init_q_is_1)
+ bit = State::Sx;
+ for (auto &bit : init_q_is_x)
+ bit = State::S0;
+ } else {
+ for (auto &bit : init_q_is_1)
+ bit = bit == State::S1 ? State::S1 : State::S0;
+ for (auto &bit : init_q_is_x)
+ bit = bit == State::Sx ? State::S1 : State::S0;
+ }
+
+ ff.remove();
+
+ auto enc_d = encoded(ff.sig_d);
+ auto enc_q = encoded(ff.sig_q, true);
+
+ auto data_q = module->addWire(NEW_ID, GetSize(ff.sig_q));
+
+ ff.sig_d = enc_d.is_1;
+ ff.sig_q = data_q;
+ ff.val_init = init_q_is_1;
+ ff.emit();
+
+ ff.name = NEW_ID;
+ ff.cell = nullptr;
+ ff.sig_d = enc_d.is_x;
+ ff.sig_q = enc_q.is_x;
+ ff.is_anyinit = false;
+ ff.val_init = init_q_is_x;
+ ff.emit();
+
+
+ enc_q.connect_1_under_x(data_q);
+ enc_q.auto_0();
+
+ return;
+ }
+ } else {
+ log_warning("Unhandled FF-cell %s (%s), consider running clk2fflogic, async2sync and/or dffunmap\n", log_id(cell), log_id(cell->type));
+ }
+ }
+
+ // Celltypes where any input x bit makes the whole output x
+ if (cell->type.in(
+ ID($neg),
+ ID($le), ID($lt), ID($ge), ID($gt),
+ ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor)
+ )) {
+
+ SigSpec inbits_x;
+ for (auto &conn : cell->connections()) {
+ if (cell->input(conn.first)) {
+ auto enc_port = encoded(conn.second);
+ inbits_x.append(enc_port.is_x);
+ cell->setPort(conn.first, enc_port.is_1);
+ }
+ }
+
+ if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor))) {
+ auto sig_b = cell->getPort(ID::B);
+ auto invalid = module->LogicNot(NEW_ID, sig_b);
+ inbits_x.append(invalid);
+ sig_b[0] = module->Or(NEW_ID, sig_b[0], invalid);
+ cell->setPort(ID::B, sig_b);
+ }
+
+ SigBit outbits_x = (GetSize(inbits_x) == 1 ? inbits_x : module->ReduceOr(NEW_ID, inbits_x));
+
+ bool bool_out = cell->type.in(ID($le), ID($lt), ID($ge), ID($gt));
+
+ for (auto &conn : cell->connections()) {
+ if (cell->output(conn.first)) {
+ auto enc_port = encoded(conn.second, true);
+ if (bool_out)
+ enc_port.connect_as_bool();
+
+ SigSpec new_output = module->addWire(NEW_ID, GetSize(conn.second));
+
+ enc_port.connect_1_under_x(bool_out ? new_output.extract(0) : new_output);
+ enc_port.connect_x(SigSpec(outbits_x, GetSize(enc_port)));
+ enc_port.auto_0();
+
+ cell->setPort(conn.first, new_output);
+ }
+ }
+
+ return;
+ }
+
+ if (cell->type == ID($bmux)) // TODO might want to support bmux natively anyway
+ log("Running 'bmuxmap' preserves x-propagation and can be run before 'xprop'.\n");
+ if (cell->type == ID($demux)) // TODO might want to support demux natively anyway
+ log("Running 'demuxmap' preserves x-propagation and can be run before 'xprop'.\n");
+
+ if (options.required)
+ log_error("Unhandled cell %s (%s)\n", log_id(cell), log_id(cell->type));
+ else
+ log_warning("Unhandled cell %s (%s)\n", log_id(cell), log_id(cell->type));
+ }
+
+ void split_ports()
+ {
+ if (!options.split_inputs && !options.split_outputs)
+ return;
+
+ vector<IdString> new_ports;
+
+ for (auto port : module->ports) {
+ auto wire = module->wire(port);
+ if (module->design->selected(module, wire)) {
+ if (wire->port_input == wire->port_output) {
+ log_warning("Port %s not an input or an output port which is not supported by xprop\n", log_id(wire));
+ } else if ((options.split_inputs && !options.assume_def_inputs && wire->port_input) || (options.split_outputs && wire->port_output)) {
+ auto port_d = module->uniquify(stringf("%s_d", port.c_str()));
+ auto port_x = module->uniquify(stringf("%s_x", port.c_str()));
+
+ auto wire_d = module->addWire(port_d, GetSize(wire));
+ auto wire_x = module->addWire(port_x, GetSize(wire));
+
+ wire_d->port_input = wire->port_input;
+ wire_d->port_output = wire->port_output;
+ wire_d->port_id = GetSize(new_ports) + 1;
+
+ wire_x->port_input = wire->port_input;
+ wire_x->port_output = wire->port_output;
+ wire_x->port_id = GetSize(new_ports) + 2;
+
+ if (wire->port_output) {
+ auto enc = encoded(wire);
+ module->connect(wire_d, enc.is_1);
+ module->connect(wire_x, enc.is_x);
+ } else {
+ auto enc = encoded(wire, true);
+
+ enc.connect_x(wire_x);
+ enc.connect_1_under_x(wire_d);
+ enc.auto_0();
+ }
+
+ wire->port_input = wire->port_output = false;
+ wire->port_id = 0;
+
+ new_ports.push_back(port_d);
+ new_ports.push_back(port_x);
+
+ continue;
+ }
+ }
+ wire->port_id = GetSize(new_ports) + 1;
+ new_ports.push_back(port);
+ }
+
+ module->ports = new_ports;
+
+ module->fixup_ports();
+ }
+
+ void encode_remaining()
+ {
+ pool<Wire *> enc_undriven_wires;
+
+ for (auto &enc_bit : encoded_bits) {
+ if (!enc_bit.second.driven) {
+ log_assert(enc_bit.first.is_wire());
+ enc_undriven_wires.insert(enc_bit.first.wire);
+ }
+ }
+
+ if (options.formal && !enc_undriven_wires.empty()) {
+ for (auto &bit : enc_undriven_wires)
+ log_warning("Found encoded wire %s having a non-encoded driver\n", log_signal(bit));
+
+ log_error("Found encoded wires having a non-encoded driver, not allowed in -formal mode\n");
+ }
+
+
+ for (auto wire : enc_undriven_wires) {
+ SigSpec sig(sigmap(wire));
+
+ SigSpec orig;
+ EncodedSig enc;
+
+ for (auto bit : sig) {
+ auto it = encoded_bits.find(bit);
+ if (it == encoded_bits.end() || it->second.driven)
+ continue;
+ orig.append(bit);
+ enc.is_0.append(it->second.is_0);
+ enc.is_1.append(it->second.is_1);
+ enc.is_x.append(it->second.is_x);
+ it->second.driven = true;
+ }
+
+ module->addBweqx(NEW_ID, orig, Const(State::S0, GetSize(orig)), enc.is_0);
+ module->addBweqx(NEW_ID, orig, Const(State::S1, GetSize(orig)), enc.is_1);
+ module->addBweqx(NEW_ID, orig, Const(State::Sx, GetSize(orig)), enc.is_x);
+ }
+ }
+};
+
+struct XpropPass : public Pass {
+ XpropPass() : Pass("xprop", "formal x propagation") {}
+ void help() override
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" xprop [options] [selection]\n");
+ log("\n");
+ log("This pass transforms the circuit into an equivalent circuit that explicitly\n");
+ log("encodes the propagation of x values using purely 2-valued logic. On the\n");
+ log("interface between xprop-transformed and non-transformed parts of the design,\n");
+ log("appropriate conversions are inserted automatically.\n");
+ log("\n");
+ log(" -split-inputs\n");
+ log(" -split-outputs\n");
+ log(" -split-ports\n");
+ log(" Replace each input/output/port with two new ports, one carrying the\n");
+ log(" defined values (named <portname>_d) and one carrying the mask of which\n");
+ log(" bits are x (named <portname>_x). When a bit in the <portname>_x is set\n");
+ log(" the corresponding bit in <portname>_d is ignored for inputs and\n");
+ log(" guaranteed to be 0 for outputs.\n");
+ log("\n");
+ log(" -assume-encoding\n");
+ log(" Add encoding invariants as assumptions. This can speed up formal\n");
+ log(" verification tasks.\n");
+ log("\n");
+ log(" -assert-encoding\n");
+ log(" Add encoding invariants as assertions. Used for testing the xprop\n");
+ log(" pass itself.\n");
+ log("\n");
+ log(" -assume-def-inputs\n");
+ log(" Assume all inputs are fully defined. This adds corresponding\n");
+ log(" assumptions to the design and uses these assumptions to optimize the\n");
+ log(" xprop encoding.\n");
+ log("\n");
+ log(" -required\n");
+ log(" Produce a runtime error if any encountered cell could not be encoded.\n");
+ log("\n");
+ log(" -formal\n");
+ log(" Produce a runtime error if any encoded cell uses a signal that is\n");
+ log(" neither known to be non-x nor driven by another encoded cell.\n");
+ log("\n");
+ log(" -debug-asserts\n");
+ log(" Add assertions checking that the encoding used by this pass never\n");
+ log(" produces x values within the encoded signals.\n");
+ log("\n");
+ }
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override
+ {
+ XpropOptions options;
+
+ log_header(design, "Executing XPROP pass.\n");
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++) {
+ if (args[argidx] == "-split-ports") {
+ options.split_inputs = true;
+ options.split_outputs = true;
+ continue;
+ }
+ if (args[argidx] == "-split-inputs") {
+ options.split_inputs = true;
+ continue;
+ }
+ if (args[argidx] == "-split-outputs") {
+ options.split_outputs = true;
+ continue;
+ }
+ if (args[argidx] == "-assume-encoding") {
+ options.assume_encoding = true;
+ continue;
+ }
+ if (args[argidx] == "-assert-encoding") {
+ options.assert_encoding = true;
+ continue;
+ }
+ if (args[argidx] == "-assume-def-inputs") {
+ options.assume_def_inputs = true;
+ continue;
+ }
+ if (args[argidx] == "-required") {
+ options.required = true; // TODO check more
+ continue;
+ }
+ if (args[argidx] == "-formal") {
+ options.formal = true;
+ options.required = true;
+ continue;
+ }
+ if (args[argidx] == "-debug-asserts") { // TODO documented
+ options.debug_asserts = true;
+ options.assert_encoding = true;
+ continue;
+ }
+ break;
+ }
+
+ if (options.assert_encoding && options.assume_encoding)
+ log_cmd_error("The options -assert-encoding and -assume-encoding are exclusive.\n");
+
+ extra_args(args, argidx, design);
+
+ log_push();
+ Pass::call(design, "bmuxmap");
+ Pass::call(design, "demuxmap");
+ log_pop();
+
+ for (auto module : design->selected_modules()) {
+ if (options.assume_def_inputs) {
+ for (auto port : module->ports) {
+ auto wire = module->wire(port);
+ if (!module->design->selected(module, wire))
+ continue;
+
+ if (wire->port_input) {
+ module->addAssume(NEW_ID, module->Not(NEW_ID, module->ReduceOr(NEW_ID, module->Bweqx(NEW_ID, wire, Const(State::Sx, GetSize(wire))))), State::S1);
+ }
+ }
+ }
+
+ XpropWorker worker(module, options);
+ log_debug("Marking all x-bits.\n");
+ worker.mark_all_maybe_x();
+ log_debug("Repalcing cells.\n");
+ worker.process_cells();
+ log_debug("Splitting ports.\n");
+ worker.split_ports();
+ log_debug("Encode remaining signals.\n");
+ worker.encode_remaining();
+
+ }
+ }
+} XpropPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/opt/opt_expr.cc b/passes/opt/opt_expr.cc
index 9cc0170dc..9d5ca4ef9 100644
--- a/passes/opt/opt_expr.cc
+++ b/passes/opt/opt_expr.cc
@@ -643,6 +643,148 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
goto next_cell;
}
+ if (cell->type.in(ID($and), ID($or), ID($xor), ID($xnor)))
+ {
+ RTLIL::SigSpec sig_a = assign_map(cell->getPort(ID::A));
+ RTLIL::SigSpec sig_b = assign_map(cell->getPort(ID::B));
+
+ bool a_fully_const = (sig_a.is_fully_const() && (!keepdc || !sig_a.is_fully_undef()));
+ bool b_fully_const = (sig_b.is_fully_const() && (!keepdc || !sig_b.is_fully_undef()));
+
+ if (a_fully_const != b_fully_const)
+ {
+ cover("opt.opt_expr.bitwise_logic_one_const");
+ log_debug("Replacing %s cell `%s' in module `%s' having one fully constant input\n",
+ log_id(cell->type), log_id(cell->name), log_id(module));
+ RTLIL::SigSpec sig_y = assign_map(cell->getPort(ID::Y));
+
+ int width = GetSize(cell->getPort(ID::Y));
+
+ sig_a.extend_u0(width, cell->getParam(ID::A_SIGNED).as_bool());
+ sig_b.extend_u0(width, cell->getParam(ID::B_SIGNED).as_bool());
+
+ if (!a_fully_const)
+ std::swap(sig_a, sig_b);
+
+ RTLIL::SigSpec b_group_0, b_group_1, b_group_x;
+ RTLIL::SigSpec y_group_0, y_group_1, y_group_x;
+
+ for (int i = 0; i < width; i++) {
+ auto bit_a = sig_a[i].data;
+ if (bit_a == State::S0) b_group_0.append(sig_b[i]), y_group_0.append(sig_y[i]);
+ if (bit_a == State::S1) b_group_1.append(sig_b[i]), y_group_1.append(sig_y[i]);
+ if (bit_a == State::Sx) b_group_x.append(sig_b[i]), y_group_x.append(sig_y[i]);
+ }
+
+ if (cell->type == ID($xnor)) {
+ std::swap(b_group_0, b_group_1);
+ std::swap(y_group_0, y_group_1);
+ }
+
+ RTLIL::SigSpec y_new_0, y_new_1, y_new_x;
+
+ if (cell->type == ID($and)) {
+ if (!y_group_0.empty()) y_new_0 = Const(State::S0, GetSize(y_group_0));
+ if (!y_group_1.empty()) y_new_1 = b_group_1;
+ if (!y_group_x.empty()) {
+ if (keepdc)
+ y_new_x = module->And(NEW_ID, Const(State::Sx, GetSize(y_group_x)), b_group_x);
+ else
+ y_new_x = Const(State::S0, GetSize(y_group_x));
+ }
+ } else if (cell->type == ID($or)) {
+ if (!y_group_0.empty()) y_new_0 = b_group_0;
+ if (!y_group_1.empty()) y_new_1 = Const(State::S1, GetSize(y_group_1));
+ if (!y_group_x.empty()) {
+ if (keepdc)
+ y_new_x = module->Or(NEW_ID, Const(State::Sx, GetSize(y_group_x)), b_group_x);
+ else
+ y_new_x = Const(State::S1, GetSize(y_group_x));
+ }
+ } else if (cell->type.in(ID($xor), ID($xnor))) {
+ if (!y_group_0.empty()) y_new_0 = b_group_0;
+ if (!y_group_1.empty()) y_new_1 = module->Not(NEW_ID, b_group_1);
+ if (!y_group_x.empty()) {
+ if (keepdc)
+ y_new_x = module->Xor(NEW_ID, Const(State::Sx, GetSize(y_group_x)), b_group_x);
+ else // This should be fine even with keepdc, but opt_expr_xor.ys wants to keep the xor
+ y_new_x = Const(State::Sx, GetSize(y_group_x));
+ }
+ } else {
+ log_abort();
+ }
+
+ assign_map.add(y_group_0, y_new_0); module->connect(y_group_0, y_new_0);
+ assign_map.add(y_group_1, y_new_1); module->connect(y_group_1, y_new_1);
+ assign_map.add(y_group_x, y_new_x); module->connect(y_group_x, y_new_x);
+
+ module->remove(cell);
+ did_something = true;
+ goto next_cell;
+ }
+ }
+
+ if (cell->type == ID($bwmux))
+ {
+ RTLIL::SigSpec sig_a = assign_map(cell->getPort(ID::A));
+ RTLIL::SigSpec sig_b = assign_map(cell->getPort(ID::B));
+ RTLIL::SigSpec sig_s = assign_map(cell->getPort(ID::S));
+ RTLIL::SigSpec sig_y = assign_map(cell->getPort(ID::Y));
+ int width = GetSize(cell->getPort(ID::Y));
+
+ if (sig_s.is_fully_def())
+ {
+ RTLIL::SigSpec a_group_0, b_group_1;
+ RTLIL::SigSpec y_group_0, y_group_1;
+ for (int i = 0; i < width; i++) {
+ if (sig_s[i].data == State::S1)
+ y_group_1.append(sig_y[i]), b_group_1.append(sig_b[i]);
+ else
+ y_group_0.append(sig_y[i]), a_group_0.append(sig_a[i]);
+ }
+
+ assign_map.add(y_group_0, a_group_0); module->connect(y_group_0, a_group_0);
+ assign_map.add(y_group_1, b_group_1); module->connect(y_group_1, b_group_1);
+
+ module->remove(cell);
+ did_something = true;
+ goto next_cell;
+ }
+ else if (sig_a.is_fully_def() || sig_b.is_fully_def())
+ {
+ bool flip = !sig_a.is_fully_def();
+ if (flip)
+ std::swap(sig_a, sig_b);
+
+ RTLIL::SigSpec b_group_0, b_group_1;
+ RTLIL::SigSpec s_group_0, s_group_1;
+ RTLIL::SigSpec y_group_0, y_group_1;
+ for (int i = 0; i < width; i++) {
+ if (sig_a[i].data == State::S1)
+ y_group_1.append(sig_y[i]), b_group_1.append(sig_b[i]), s_group_1.append(sig_s[i]);
+ else
+ y_group_0.append(sig_y[i]), b_group_0.append(sig_b[i]), s_group_0.append(sig_s[i]);
+ }
+
+ RTLIL::SigSpec y_new_0, y_new_1;
+
+ if (flip) {
+ if (!y_group_0.empty()) y_new_0 = module->And(NEW_ID, b_group_0, module->Not(NEW_ID, s_group_0));
+ if (!y_group_1.empty()) y_new_1 = module->Or(NEW_ID, b_group_1, s_group_1);
+ } else {
+ if (!y_group_0.empty()) y_new_0 = module->And(NEW_ID, b_group_0, s_group_0);
+ if (!y_group_1.empty()) y_new_1 = module->Or(NEW_ID, b_group_1, module->Not(NEW_ID, s_group_1));
+ }
+
+ module->connect(y_group_0, y_new_0);
+ module->connect(y_group_1, y_new_1);
+
+ module->remove(cell);
+ did_something = true;
+ goto next_cell;
+ }
+ }
+
if (do_fine)
{
if (cell->type.in(ID($not), ID($pos), ID($and), ID($or), ID($xor), ID($xnor)))
@@ -905,7 +1047,7 @@ skip_fine_alu:
}
}
- if (cell->type.in(ID($shiftx), ID($shift))) {
+ if (cell->type.in(ID($shiftx), ID($shift)) && (cell->type == ID($shiftx) || !cell->getParam(ID::A_SIGNED).as_bool())) {
SigSpec sig_a = assign_map(cell->getPort(ID::A));
int width;
bool trim_x = cell->type == ID($shiftx) || !keepdc;
@@ -1152,7 +1294,7 @@ skip_fine_alu:
goto next_cell;
}
- if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)) && assign_map(cell->getPort(ID::B)).is_fully_const())
+ if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)) && (keepdc ? assign_map(cell->getPort(ID::B)).is_fully_def() : assign_map(cell->getPort(ID::B)).is_fully_const()))
{
bool sign_ext = cell->type == ID($sshr) && cell->getParam(ID::A_SIGNED).as_bool();
int shift_bits = assign_map(cell->getPort(ID::B)).as_int(cell->type.in(ID($shift), ID($shiftx)) && cell->getParam(ID::B_SIGNED).as_bool());
@@ -1163,7 +1305,7 @@ skip_fine_alu:
RTLIL::SigSpec sig_a = assign_map(cell->getPort(ID::A));
RTLIL::SigSpec sig_y(cell->type == ID($shiftx) ? RTLIL::State::Sx : RTLIL::State::S0, cell->getParam(ID::Y_WIDTH).as_int());
- if (GetSize(sig_a) < GetSize(sig_y))
+ if (cell->type != ID($shiftx) && GetSize(sig_a) < GetSize(sig_y))
sig_a.extend_u0(GetSize(sig_y), cell->getParam(ID::A_SIGNED).as_bool());
for (int i = 0; i < GetSize(sig_y); i++) {
@@ -1446,6 +1588,31 @@ skip_identity:
goto next_cell; \
} \
}
+#define FOLD_2ARG_SIMPLE_CELL(_t, B_ID) \
+ if (cell->type == ID($##_t)) { \
+ RTLIL::SigSpec a = cell->getPort(ID::A); \
+ RTLIL::SigSpec b = cell->getPort(B_ID); \
+ assign_map.apply(a), assign_map.apply(b); \
+ if (a.is_fully_const() && b.is_fully_const()) { \
+ RTLIL::SigSpec y(RTLIL::const_ ## _t(a.as_const(), b.as_const())); \
+ cover("opt.opt_expr.const.$" #_t); \
+ replace_cell(assign_map, module, cell, stringf("%s, %s", log_signal(a), log_signal(b)), ID::Y, y); \
+ goto next_cell; \
+ } \
+ }
+#define FOLD_MUX_CELL(_t) \
+ if (cell->type == ID($##_t)) { \
+ RTLIL::SigSpec a = cell->getPort(ID::A); \
+ RTLIL::SigSpec b = cell->getPort(ID::B); \
+ RTLIL::SigSpec s = cell->getPort(ID::S); \
+ assign_map.apply(a), assign_map.apply(b), assign_map.apply(s); \
+ if (a.is_fully_const() && b.is_fully_const() && s.is_fully_const()) { \
+ RTLIL::SigSpec y(RTLIL::const_ ## _t(a.as_const(), b.as_const(), s.as_const())); \
+ cover("opt.opt_expr.const.$" #_t); \
+ replace_cell(assign_map, module, cell, stringf("%s, %s, %s", log_signal(a), log_signal(b), log_signal(s)), ID::Y, y); \
+ goto next_cell; \
+ } \
+ }
FOLD_1ARG_CELL(not)
FOLD_2ARG_CELL(and)
@@ -1477,6 +1644,9 @@ skip_identity:
FOLD_2ARG_CELL(gt)
FOLD_2ARG_CELL(ge)
+ FOLD_2ARG_CELL(eqx)
+ FOLD_2ARG_CELL(nex)
+
FOLD_2ARG_CELL(add)
FOLD_2ARG_CELL(sub)
FOLD_2ARG_CELL(mul)
@@ -1489,6 +1659,13 @@ skip_identity:
FOLD_1ARG_CELL(pos)
FOLD_1ARG_CELL(neg)
+ FOLD_MUX_CELL(mux);
+ FOLD_MUX_CELL(pmux);
+ FOLD_2ARG_SIMPLE_CELL(bmux, ID::S);
+ FOLD_2ARG_SIMPLE_CELL(demux, ID::S);
+ FOLD_2ARG_SIMPLE_CELL(bweqx, ID::B);
+ FOLD_MUX_CELL(bwmux);
+
// be very conservative with optimizing $mux cells as we do not want to break mux trees
if (cell->type == ID($mux)) {
RTLIL::SigSpec input = assign_map(cell->getPort(ID::S));
diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc
index 962e350a1..e36379096 100644
--- a/passes/sat/formalff.cc
+++ b/passes/sat/formalff.cc
@@ -532,12 +532,14 @@ struct FormalFfPass : public Pass {
if ((int)bits.size() == ff.val_init.size()) {
// This check is only to make the private names more helpful for debugging
ff.is_anyinit = true;
+ ff.is_fine = false;
emit = true;
break;
}
auto slice = ff.slice(bits);
slice.is_anyinit = is_anyinit;
+ slice.is_fine = false;
slice.emit();
}
}
diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index bf33c9ce3..1f64c0216 100644
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.cc
@@ -30,6 +30,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
bool flag_make_outputs = false;
bool flag_make_outcmp = false;
bool flag_make_assert = false;
+ bool flag_make_cover = false;
bool flag_flatten = false;
bool flag_cross = false;
@@ -54,6 +55,10 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
flag_make_assert = true;
continue;
}
+ if (args[argidx] == "-make_cover") {
+ flag_make_cover = true;
+ continue;
+ }
if (args[argidx] == "-flatten") {
flag_flatten = true;
continue;
@@ -237,6 +242,12 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
miter_module->connect(RTLIL::SigSig(w_cmp, this_condition));
}
+ if (flag_make_cover)
+ {
+ auto cover_condition = miter_module->Not(NEW_ID, this_condition);
+ miter_module->addCover("\\cover_" + RTLIL::unescape_id(gold_wire->name), cover_condition, State::S1);
+ }
+
all_conditions.append(this_condition);
}
}
@@ -402,6 +413,9 @@ struct MiterPass : public Pass {
log(" -make_assert\n");
log(" also create an 'assert' cell that checks if trigger is always low.\n");
log("\n");
+ log(" -make_cover\n");
+ log(" also create a 'cover' cell for each gold/gate output pair.\n");
+ log("\n");
log(" -flatten\n");
log(" call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
log("\n");
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 1cd1ebc71..e8dda4c45 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -509,7 +509,7 @@ struct SimInstance
}
}
- bool update_ph2()
+ bool update_ph2(bool gclk)
{
bool did_something = false;
@@ -567,7 +567,8 @@ struct SimInstance
}
if (ff_data.has_gclk) {
// $ff
- current_q = ff.past_d;
+ if (gclk)
+ current_q = ff.past_d;
}
if (set_state(ff_data.sig_q, current_q))
did_something = true;
@@ -616,7 +617,7 @@ struct SimInstance
}
for (auto it : children)
- if (it.second->update_ph2()) {
+ if (it.second->update_ph2(gclk)) {
dirty_children.insert(it.second);
did_something = true;
}
@@ -985,7 +986,7 @@ struct SimWorker : SimShared
writer->write(use_signal);
}
- void update()
+ void update(bool gclk)
{
while (1)
{
@@ -997,7 +998,7 @@ struct SimWorker : SimShared
if (debug)
log("\n-- ph2 --\n");
- if (!top->update_ph2())
+ if (!top->update_ph2(gclk))
break;
}
@@ -1047,7 +1048,7 @@ struct SimWorker : SimShared
set_inports(clock, State::Sx);
set_inports(clockn, State::Sx);
- update();
+ update(false);
register_output_step(0);
@@ -1060,7 +1061,7 @@ struct SimWorker : SimShared
set_inports(clock, State::S0);
set_inports(clockn, State::S1);
- update();
+ update(true);
register_output_step(10*cycle + 5);
if (debug)
@@ -1076,7 +1077,7 @@ struct SimWorker : SimShared
set_inports(resetn, State::S1);
}
- update();
+ update(true);
register_output_step(10*cycle + 10);
}
@@ -1193,7 +1194,7 @@ struct SimWorker : SimShared
initial = false;
}
if (did_something)
- update();
+ update(true);
register_output_step(time);
bool status = top->checkSignals();
@@ -1342,12 +1343,12 @@ struct SimWorker : SimShared
set_inports(clock, State::S0);
set_inports(clockn, State::S1);
}
- update();
+ update(true);
register_output_step(10*cycle);
if (!multiclock && cycle) {
set_inports(clock, State::S0);
set_inports(clockn, State::S1);
- update();
+ update(true);
register_output_step(10*cycle + 5);
}
cycle++;
@@ -1419,12 +1420,12 @@ struct SimWorker : SimShared
log("Simulating cycle %d.\n", cycle);
set_inports(clock, State::S1);
set_inports(clockn, State::S0);
- update();
+ update(true);
register_output_step(10*cycle+0);
if (!multiclock) {
set_inports(clock, State::S0);
set_inports(clockn, State::S1);
- update();
+ update(true);
register_output_step(10*cycle+5);
}
cycle++;
diff --git a/passes/techmap/Makefile.inc b/passes/techmap/Makefile.inc
index 98ccfc303..1b834fabc 100644
--- a/passes/techmap/Makefile.inc
+++ b/passes/techmap/Makefile.inc
@@ -31,6 +31,7 @@ OBJS += passes/techmap/dffinit.o
OBJS += passes/techmap/pmuxtree.o
OBJS += passes/techmap/bmuxmap.o
OBJS += passes/techmap/demuxmap.o
+OBJS += passes/techmap/bwmuxmap.o
OBJS += passes/techmap/muxcover.o
OBJS += passes/techmap/aigmap.o
OBJS += passes/techmap/tribuf.o
diff --git a/passes/techmap/bwmuxmap.cc b/passes/techmap/bwmuxmap.cc
new file mode 100644
index 000000000..7fe1cded7
--- /dev/null
+++ b/passes/techmap/bwmuxmap.cc
@@ -0,0 +1,70 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one>
+ *
+ * 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
+
+struct BwmuxmapPass : public Pass {
+ BwmuxmapPass() : Pass("bwmuxmap", "replace $bwmux cells with equivalent logic") {}
+ void help() override
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" bwmxumap [options] [selection]\n");
+ log("\n");
+ log("This pass replaces $bwmux cells with equivalent logic\n");
+ log("\n");
+ }
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override
+ {
+ log_header(design, "Executing BWMUXMAP pass.\n");
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++) {
+ // if (args[argidx] == "-arg") {
+ // continue;
+ // }
+ break;
+ }
+
+ extra_args(args, argidx, design);
+
+ for (auto module : design->selected_modules())
+ for (auto cell : module->selected_cells())
+ {
+ if (cell->type != ID($bwmux))
+ continue;
+ auto &sig_y = cell->getPort(ID::Y);
+ auto &sig_a = cell->getPort(ID::A);
+ auto &sig_b = cell->getPort(ID::B);
+ auto &sig_s = cell->getPort(ID::S);
+
+ auto not_s = module->Not(NEW_ID, sig_s);
+ auto masked_b = module->And(NEW_ID, sig_s, sig_b);
+ auto masked_a = module->And(NEW_ID, not_s, sig_a);
+ module->addOr(NEW_ID, masked_a, masked_b, sig_y);
+
+ module->remove(cell);
+ }
+ }
+} BwmuxmapPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/techmap/simplemap.cc b/passes/techmap/simplemap.cc
index f75b82919..11692b715 100644
--- a/passes/techmap/simplemap.cc
+++ b/passes/techmap/simplemap.cc
@@ -58,28 +58,17 @@ void simplemap_bitop(RTLIL::Module *module, RTLIL::Cell *cell)
RTLIL::SigSpec sig_b = cell->getPort(ID::B);
RTLIL::SigSpec sig_y = cell->getPort(ID::Y);
- sig_a.extend_u0(GetSize(sig_y), cell->parameters.at(ID::A_SIGNED).as_bool());
- sig_b.extend_u0(GetSize(sig_y), cell->parameters.at(ID::B_SIGNED).as_bool());
-
- if (cell->type == ID($xnor))
- {
- RTLIL::SigSpec sig_t = module->addWire(NEW_ID, GetSize(sig_y));
-
- for (int i = 0; i < GetSize(sig_y); i++) {
- RTLIL::Cell *gate = module->addCell(NEW_ID, ID($_NOT_));
- gate->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src));
- gate->setPort(ID::A, sig_t[i]);
- gate->setPort(ID::Y, sig_y[i]);
- }
-
- sig_y = sig_t;
+ if (cell->type != ID($bweqx)) {
+ sig_a.extend_u0(GetSize(sig_y), cell->parameters.at(ID::A_SIGNED).as_bool());
+ sig_b.extend_u0(GetSize(sig_y), cell->parameters.at(ID::B_SIGNED).as_bool());
}
IdString gate_type;
- if (cell->type == ID($and)) gate_type = ID($_AND_);
- if (cell->type == ID($or)) gate_type = ID($_OR_);
- if (cell->type == ID($xor)) gate_type = ID($_XOR_);
- if (cell->type == ID($xnor)) gate_type = ID($_XOR_);
+ if (cell->type == ID($and)) gate_type = ID($_AND_);
+ if (cell->type == ID($or)) gate_type = ID($_OR_);
+ if (cell->type == ID($xor)) gate_type = ID($_XOR_);
+ if (cell->type == ID($xnor)) gate_type = ID($_XNOR_);
+ if (cell->type == ID($bweqx)) gate_type = ID($_XNOR_);
log_assert(!gate_type.empty());
for (int i = 0; i < GetSize(sig_y); i++) {
@@ -284,6 +273,23 @@ void simplemap_mux(RTLIL::Module *module, RTLIL::Cell *cell)
}
}
+void simplemap_bwmux(RTLIL::Module *module, RTLIL::Cell *cell)
+{
+ RTLIL::SigSpec sig_a = cell->getPort(ID::A);
+ RTLIL::SigSpec sig_b = cell->getPort(ID::B);
+ RTLIL::SigSpec sig_s = cell->getPort(ID::S);
+ RTLIL::SigSpec sig_y = cell->getPort(ID::Y);
+
+ for (int i = 0; i < GetSize(sig_y); i++) {
+ RTLIL::Cell *gate = module->addCell(NEW_ID, ID($_MUX_));
+ gate->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src));
+ gate->setPort(ID::A, sig_a[i]);
+ gate->setPort(ID::B, sig_b[i]);
+ gate->setPort(ID::S, sig_s[i]);
+ gate->setPort(ID::Y, sig_y[i]);
+ }
+}
+
void simplemap_tribuf(RTLIL::Module *module, RTLIL::Cell *cell)
{
RTLIL::SigSpec sig_a = cell->getPort(ID::A);
@@ -409,6 +415,7 @@ void simplemap_get_mappers(dict<IdString, void(*)(RTLIL::Module*, RTLIL::Cell*)>
mappers[ID($or)] = simplemap_bitop;
mappers[ID($xor)] = simplemap_bitop;
mappers[ID($xnor)] = simplemap_bitop;
+ mappers[ID($bweqx)] = simplemap_bitop;
mappers[ID($reduce_and)] = simplemap_reduce;
mappers[ID($reduce_or)] = simplemap_reduce;
mappers[ID($reduce_xor)] = simplemap_reduce;
@@ -422,6 +429,7 @@ void simplemap_get_mappers(dict<IdString, void(*)(RTLIL::Module*, RTLIL::Cell*)>
mappers[ID($ne)] = simplemap_eqne;
mappers[ID($nex)] = simplemap_eqne;
mappers[ID($mux)] = simplemap_mux;
+ mappers[ID($bwmux)] = simplemap_bwmux;
mappers[ID($tribuf)] = simplemap_tribuf;
mappers[ID($bmux)] = simplemap_bmux;
mappers[ID($lut)] = simplemap_lut;
diff --git a/passes/techmap/simplemap.h b/passes/techmap/simplemap.h
index c7654f68c..30cc1ccfe 100644
--- a/passes/techmap/simplemap.h
+++ b/passes/techmap/simplemap.h
@@ -31,6 +31,7 @@ extern void simplemap_reduce(RTLIL::Module *module, RTLIL::Cell *cell);
extern void simplemap_lognot(RTLIL::Module *module, RTLIL::Cell *cell);
extern void simplemap_logbin(RTLIL::Module *module, RTLIL::Cell *cell);
extern void simplemap_mux(RTLIL::Module *module, RTLIL::Cell *cell);
+extern void simplemap_bwmux(RTLIL::Module *module, RTLIL::Cell *cell);
extern void simplemap_lut(RTLIL::Module *module, RTLIL::Cell *cell);
extern void simplemap_slice(RTLIL::Module *module, RTLIL::Cell *cell);
extern void simplemap_concat(RTLIL::Module *module, RTLIL::Cell *cell);
diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index e64697efb..9cb68e725 100644
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -1300,11 +1300,11 @@ wire [WIDTH-1:0] bm0_out, bm1_out;
generate
if (S_WIDTH > 1) begin:muxlogic
- \$bmux #(.WIDTH(WIDTH), .S_WIDTH(S_WIDTH-1)) bm0 (.A(A), .S(S[S_WIDTH-2:0]), .Y(bm0_out));
+ \$bmux #(.WIDTH(WIDTH), .S_WIDTH(S_WIDTH-1)) bm0 (.A(A[(WIDTH << (S_WIDTH - 1))-1:0]), .S(S[S_WIDTH-2:0]), .Y(bm0_out));
\$bmux #(.WIDTH(WIDTH), .S_WIDTH(S_WIDTH-1)) bm1 (.A(A[(WIDTH << S_WIDTH)-1:WIDTH << (S_WIDTH - 1)]), .S(S[S_WIDTH-2:0]), .Y(bm1_out));
assign Y = S[S_WIDTH-1] ? bm1_out : bm0_out;
end else if (S_WIDTH == 1) begin:simple
- assign Y = S ? A[1] : A[0];
+ assign Y = S ? A[2*WIDTH-1:WIDTH] : A[WIDTH-1:0];
end else begin:passthru
assign Y = A;
end
@@ -1331,10 +1331,17 @@ always @* begin
Y = A;
found_active_sel_bit = 0;
for (i = 0; i < S_WIDTH; i = i+1)
- if (S[i]) begin
- Y = found_active_sel_bit ? 'bx : B >> (WIDTH*i);
- found_active_sel_bit = 1;
- end
+ case (S[i])
+ 1'b1: begin
+ Y = found_active_sel_bit ? 'bx : B >> (WIDTH*i);
+ found_active_sel_bit = 1;
+ end
+ 1'b0: ;
+ 1'bx: begin
+ Y = 'bx;
+ found_active_sel_bit = 'bx;
+ end
+ endcase
end
endmodule
@@ -1370,7 +1377,7 @@ parameter LUT = 0;
input [WIDTH-1:0] A;
output Y;
-\$bmux #(.WIDTH(1), .S_WIDTH(WIDTH)) mux(.A(LUT), .S(A), .Y(Y));
+\$bmux #(.WIDTH(1), .S_WIDTH(WIDTH)) mux(.A(LUT[(1<<WIDTH)-1:0]), .S(A), .Y(Y));
endmodule
@@ -1594,6 +1601,43 @@ endmodule
// --------------------------------------------------------
+module \$bweqx (A, B, Y);
+
+parameter WIDTH = 0;
+
+input [WIDTH-1:0] A, B;
+output [WIDTH-1:0] Y;
+
+genvar i;
+generate
+ for (i = 0; i < WIDTH; i = i + 1) begin:slices
+ assign Y[i] = A[i] === B[i];
+ end
+endgenerate
+
+endmodule
+
+// --------------------------------------------------------
+
+module \$bwmux (A, B, S, Y);
+
+parameter WIDTH = 0;
+
+input [WIDTH-1:0] A, B;
+input [WIDTH-1:0] S;
+output [WIDTH-1:0] Y;
+
+genvar i;
+generate
+ for (i = 0; i < WIDTH; i = i + 1) begin:slices
+ assign Y[i] = S[i] ? B[i] : A[i];
+ end
+endgenerate
+
+endmodule
+
+// --------------------------------------------------------
+
module \$assert (A, EN);
input A, EN;
@@ -1693,6 +1737,9 @@ endmodule
// --------------------------------------------------------
`ifdef SIMLIB_FF
+`ifndef SIMLIB_GLOBAL_CLOCK
+`define SIMLIB_GLOBAL_CLOCK $global_clk
+`endif
module \$anyinit (D, Q);
parameter WIDTH = 0;
@@ -1702,7 +1749,7 @@ output reg [WIDTH-1:0] Q;
initial Q <= 'bx;
-always @($global_clk) begin
+always @(`SIMLIB_GLOBAL_CLOCK) begin
Q <= D;
end
@@ -1783,6 +1830,9 @@ endmodule
`endif
// --------------------------------------------------------
`ifdef SIMLIB_FF
+`ifndef SIMLIB_GLOBAL_CLOCK
+`define SIMLIB_GLOBAL_CLOCK $global_clk
+`endif
module \$ff (D, Q);
@@ -1791,7 +1841,7 @@ parameter WIDTH = 0;
input [WIDTH-1:0] D;
output reg [WIDTH-1:0] Q;
-always @($global_clk) begin
+always @(`SIMLIB_GLOBAL_CLOCK) begin
Q <= D;
end
diff --git a/techlibs/common/techmap.v b/techlibs/common/techmap.v
index 91d385b80..7fb8173b0 100644
--- a/techlibs/common/techmap.v
+++ b/techlibs/common/techmap.v
@@ -59,7 +59,7 @@ module _90_simplemap_compare_ops;
endmodule
(* techmap_simplemap *)
-(* techmap_celltype = "$pos $slice $concat $mux $tribuf $bmux" *)
+(* techmap_celltype = "$pos $slice $concat $mux $tribuf $bmux $bwmux $bweqx" *)
module _90_simplemap_various;
endmodule
diff --git a/tests/opt/opt_expr_xnor.ys b/tests/opt/opt_expr_xnor.ys
index f8ef0d352..225df7076 100644
--- a/tests/opt/opt_expr_xnor.ys
+++ b/tests/opt/opt_expr_xnor.ys
@@ -32,7 +32,7 @@ select -assert-count 1 c:*
cd fine_keepdc
simplemap
opt_expr -keepdc
-select -assert-count 1 t:$_XOR_
+select -assert-count 1 t:$_XNOR_
cd
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
diff --git a/tests/opt/opt_expr_xor.ys b/tests/opt/opt_expr_xor.ys
index 8874f2775..9edec35d6 100644
--- a/tests/opt/opt_expr_xor.ys
+++ b/tests/opt/opt_expr_xor.ys
@@ -22,9 +22,8 @@ simplemap
equiv_opt -assert opt_expr
design -load postopt
select -assert-none t:$_XOR_
-select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
-select -assert-count 3 t:$_NOT_
-
+select -assert-none t:$_XNOR_
+select -assert-count 2 t:$_NOT_
design -reset
read_verilog -icells <<EOT
@@ -36,7 +35,7 @@ EOT
select -assert-count 2 t:$_XNOR_
equiv_opt -assert opt_expr
design -load postopt
-select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
+select -assert-none t:$_XNOR_
select -assert-count 1 t:$_NOT_
diff --git a/tests/xprop/.gitignore b/tests/xprop/.gitignore
new file mode 100644
index 000000000..ff0b65b54
--- /dev/null
+++ b/tests/xprop/.gitignore
@@ -0,0 +1,2 @@
+/xprop_*
+/run-test.mk
diff --git a/tests/xprop/generate.py b/tests/xprop/generate.py
new file mode 100644
index 000000000..eef8dc36e
--- /dev/null
+++ b/tests/xprop/generate.py
@@ -0,0 +1,278 @@
+import os
+import re
+import sys
+import random
+import argparse
+
+parser = argparse.ArgumentParser(formatter_class=argparse.ArgumentDefaultsHelpFormatter)
+parser.add_argument('-S', '--seed', type=int, help='seed for PRNG')
+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()
+
+if args.seed is None:
+ args.seed = random.randrange(1 << 32)
+
+print(f"xprop PRNG seed: {args.seed}")
+
+makefile = open("run-test.mk", "w")
+
+def add_test(name, src, seq=False):
+ if not re.search(args.filter, name):
+ return
+ workdir = f"xprop_{name}"
+
+ os.makedirs(workdir, exist_ok=True)
+ with open(f"{workdir}/uut.v", "w") as uut:
+ print(src, file=uut)
+ print(f"all: {workdir}", file=makefile)
+ print(f".PHONY: {workdir}", file=makefile)
+ print(f"{workdir}:", file=makefile)
+ seq_arg = " -s" if seq else ""
+ 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"
+ ,
+ file=makefile,
+ )
+
+def cell_test(name, cell, inputs, outputs, params, initial={}, defclock=False, seq=False):
+ ports = []
+ port_conns = []
+ for inport, width in inputs.items():
+ ports.append(f"input [{width-1}:0] {inport}")
+ if defclock and inport in ["C", "CLK"]:
+ port_conns.append(f".{inport}({inport} !== 0)")
+ else:
+ port_conns.append(f".{inport}({inport})")
+ for outport, width in outputs.items():
+ reg = " reg" if outport in initial else ""
+ ports.append(f"output{reg} [{width-1}:0] {outport}")
+ port_conns.append(f".{outport}({outport})")
+ param_defs = []
+ for param, value in params.items():
+ param_defs.append(f".{param}({value})")
+ initials = []
+ # for port, value in initial.items():
+ # initials.append(f"initial {port} = {value};\n")
+ add_test(name,
+ f"module uut({', '.join(ports)});\n"
+ f"\\${cell} #({', '.join(param_defs)}) cell ({', '.join(port_conns)});\n"
+ f"{''.join(initials)}"
+ "endmodule",
+ seq=seq,
+ )
+
+def unary_test(cell, width, signed, out_width):
+ add_test(
+ f"{cell}_{width}{'us'[signed]}_{out_width}",
+ f"module uut(input [{width-1}:0] A, output [{out_width}-1:0] Y);\n"
+ f"\\${cell} #(.A_WIDTH({width}), .A_SIGNED({int(signed)}), .Y_WIDTH({out_width}))"
+ " cell (.A(A), .Y(Y));\n"
+ "endmodule",
+ )
+
+def binary_test(cell, a_width, b_width, signed, out_width):
+ add_test(
+ f"{cell}_{a_width}{'us'[signed]}{b_width}_{out_width}",
+ f"module uut(input [{a_width-1}:0] A, input [{b_width-1}:0] B, output [{out_width}-1:0] Y);\n"
+ f"\\${cell} #(.A_WIDTH({a_width}), .A_SIGNED({int(signed)}), .B_WIDTH({b_width}), .B_SIGNED({int(signed)}), .Y_WIDTH({out_width}))"
+ " cell (.A(A), .B(B), .Y(Y));\n"
+ "endmodule",
+ )
+
+def shift_test(cell, a_width, b_width, a_signed, b_signed, out_width):
+ add_test(
+ f"{cell}_{a_width}{'us'[a_signed]}{b_width}{'us'[b_signed]}_{out_width}",
+ f"module uut(input [{a_width-1}:0] A, input [{b_width-1}:0] B, output [{out_width}-1:0] Y);\n"
+ f"\\${cell} #(.A_WIDTH({a_width}), .A_SIGNED({int(a_signed)}), .B_WIDTH({b_width}), .B_SIGNED({int(b_signed)}), .Y_WIDTH({out_width}))"
+ " cell (.A(A), .B(B), .Y(Y));\n"
+ "endmodule",
+ )
+
+def mux_test(width):
+ cell_test(f"mux_{width}", 'mux', {"A": width, "B": width, "S": 1}, {"Y": width}, {"WIDTH": width})
+
+def bmux_test(width, s_width):
+ cell_test(f"bmux_{width}_{s_width}", 'bmux', {"A": width << s_width, "S": s_width}, {"Y": width}, {"WIDTH": width, "S_WIDTH": s_width})
+
+def demux_test(width, s_width):
+ cell_test(f"demux_{width}_{s_width}", 'demux', {"A": width, "S": s_width}, {"Y": width << s_width}, {"WIDTH": width, "S_WIDTH": s_width})
+
+def pmux_test(width, s_width):
+ cell_test(f"pmux_{width}_{s_width}", 'pmux', {"A": width, "B": width * s_width, "S": s_width}, {"Y": width}, {"WIDTH": width, "S_WIDTH": s_width})
+
+def bwmux_test(width):
+ cell_test(f"bwmux_{width}", 'bwmux', {"A": width, "B": width, "S": width}, {"Y": width}, {"WIDTH": width})
+
+def bweqx_test(width):
+ cell_test(f"bweqx_{width}", 'bweqx', {"A": width, "B": width}, {"Y": width}, {"WIDTH": width})
+
+def ff_test(width):
+ cell_test(f"ff_{width}", 'ff', {"D": width}, {"Q": width}, {"WIDTH": width}, seq=True)
+
+def dff_test(width, pol, defclock):
+ cell_test(f"dff_{width}{'np'[pol]}{'xd'[defclock]}", 'dff', {"CLK": 1, "D": width}, {"Q": width}, {"WIDTH": width, "CLK_POLARITY": int(pol)}, defclock=defclock, seq=True)
+
+def dffe_test(width, pol, enpol, defclock):
+ cell_test(f"dffe_{width}{'np'[pol]}{'np'[enpol]}{'xd'[defclock]}", 'dffe', {"CLK": 1, "EN": 1, "D": width}, {"Q": width}, {"WIDTH": width, "CLK_POLARITY": int(pol), "EN_POLARITY": int(enpol)}, defclock=defclock, seq=True)
+
+
+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)
+ 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)
+
+# [, "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)
+ 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)
+ 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)
+ unary_test(cell, 3, False, 3)
+ unary_test(cell, 3, True, 3)
+
+for cell in ["reduce_bool", "logic_not"]:
+ unary_test(cell, 1, False, 1)
+ unary_test(cell, 3, False, 3)
+ unary_test(cell, 3, True, 3)
+ unary_test(cell, 3, True, 1)
+
+for cell in ["logic_and", "logic_or"]:
+ binary_test(cell, 1, 1, False, 1)
+ binary_test(cell, 3, 3, False, 3)
+ binary_test(cell, 3, 3, True, 3)
+ 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)
+ 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)
+ 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)
+ shift_test(cell, 4, 2, False, True, 8)
+ shift_test(cell, 4, 3, False, True, 3)
+
+mux_test(1)
+mux_test(3)
+
+bmux_test(1, 2)
+bmux_test(2, 2)
+bmux_test(3, 1)
+
+demux_test(1, 2)
+demux_test(2, 2)
+demux_test(3, 1)
+
+pmux_test(1, 4)
+pmux_test(2, 2)
+pmux_test(3, 1)
+pmux_test(4, 4)
+
+bwmux_test(1)
+bwmux_test(3)
+
+bweqx_test(1)
+bweqx_test(3)
+
+ff_test(1)
+ff_test(3)
+
+dff_test(1, True, True)
+dff_test(1, False, True)
+dff_test(3, True, True)
+dff_test(3, False, True)
+
+# dff_test(1, True, False) # TODO support x clocks
+# dff_test(1, False, False) # TODO support x clocks
+# dff_test(3, True, False) # TODO support x clocks
+# dff_test(3, False, False) # TODO support x clocks
+
+dffe_test(1, True, False, True)
+dffe_test(1, False, False, True)
+dffe_test(3, True, False, True)
+dffe_test(3, False, False, True)
+dffe_test(1, True, True, True)
+dffe_test(1, False, True, True)
+dffe_test(3, True, True, True)
+dffe_test(3, False, True, True)
+
+
+
+# TODO "shift", "shiftx"
+
+# TODO "fa", "lcu", "alu", "macc", "lut", "sop"
+
+# TODO "slice", "concat"
+
+# TODO "tribuf", "specify2", "specify3", "specrule"
+
+# TODO "assert", "assume", "live", "fair", "cover", "initstate", "anyconst", "anyseq", "anyinit", "allconst", "allseq", "equiv",
+
+# TODO "bweqx", "bwmux"
+
+# TODO "sr", "ff", "dff", "dffe", "dffsr", "sffsre", "adff", "aldff", "sdff", "adffe", "aldffe", "sdffe", "sdffce", "dlatch", "adlatch", "dlatchsr"
+
+# TODO "fsm"
+
+# TODO "memrd", "memrd_v2", "memwr", "memwr_v2", "meminit", "meminit_v2", "mem", "mem_v2"
diff --git a/tests/xprop/run-test.sh b/tests/xprop/run-test.sh
new file mode 100755
index 000000000..1fc7e10b6
--- /dev/null
+++ b/tests/xprop/run-test.sh
@@ -0,0 +1,5 @@
+#!/bin/bash
+set -e
+
+python3 generate.py $@
+make -f run-test.mk
diff --git a/tests/xprop/test.py b/tests/xprop/test.py
new file mode 100644
index 000000000..84ad0a1f4
--- /dev/null
+++ b/tests/xprop/test.py
@@ -0,0 +1,516 @@
+import os
+import re
+import subprocess
+import itertools
+import random
+import argparse
+from pathlib import Path
+
+parser = argparse.ArgumentParser(formatter_class=argparse.ArgumentDefaultsHelpFormatter)
+parser.add_argument('-S', '--seed', type=int, help='seed for PRNG')
+parser.add_argument('-c', '--count', type=int, default=32, help='number of random patterns to test')
+parser.add_argument('-s', '--seq', action='store_true', help='run a sequential test')
+parser.add_argument('steps', nargs='*', help='steps to run')
+args = parser.parse_args()
+
+if args.seed is None:
+ args.seed = random.randrange(1 << 32)
+
+print(f"PRNG seed: {args.seed}")
+random.seed(args.seed)
+
+steps = args.steps
+
+all_outputs = [
+ "sim",
+ "sim_xprop",
+ "vsim_expr",
+ "vsim_expr_xprop",
+ "vsim_noexpr",
+ "vsim_noexpr_xprop",
+ "sat",
+ "sat_xprop",
+]
+
+if not args.seq:
+ all_outputs += ["opt_expr", "opt_expr_xprop"]
+
+if not steps:
+ steps = ["clean", "prepare", "verify", *all_outputs, "compare"]
+
+if "clean" in steps:
+ for output in all_outputs:
+ try:
+ os.unlink(f"{output}.out")
+ except FileNotFoundError:
+ pass
+
+
+def yosys(command):
+ subprocess.check_call(["yosys", "-Qp", command])
+
+def remove(file):
+ try:
+ os.unlink(file)
+ except FileNotFoundError:
+ pass
+
+
+def vcdextract(signals, on_change, file, output, limit=None):
+ scope = []
+ ids = {}
+ prefix = []
+
+ for line in file:
+ line = prefix + line.split()
+ if line[-1] != "$end":
+ prefix = line
+ continue
+ prefix = []
+
+ if not line:
+ continue
+ if line[0] == "$scope":
+ scope.append(line[2].lstrip("\\"))
+ elif line[0] == "$upscope":
+ scope.pop()
+ elif line[0] == "$var":
+ ids[".".join(scope + [line[4].lstrip("\\")])] = line[3]
+ elif line[0] == "$enddefinitions":
+ break
+ elif line[0] in ["$version", "$date", "$comment"]:
+ continue
+ else:
+ raise RuntimeError(f"unexpected input in vcd {line}")
+
+ dump_pos = {}
+
+ for i, sig in enumerate(signals + on_change):
+ dump_pos[ids[sig]] = i
+
+ values = [None] * len(signals + on_change)
+
+ last_values = []
+
+ counter = 0
+
+ for line in file:
+ if line.startswith("#"):
+ if None in values:
+ continue
+
+ if values != last_values:
+ last_values = list(values)
+ if limit is None or counter < limit:
+ print(*values[:len(signals)], file=output)
+ counter += 1
+ continue
+
+ if line.startswith("b"):
+ value, id = line[1:].split()
+ else:
+ value, id = line[:1], line[1:]
+
+ pos = dump_pos.get(id)
+ if pos is None:
+ continue
+
+ values[pos] = value
+
+ if values != last_values:
+ if limit is None or counter < limit:
+ print(*values[:len(signals)], file=output)
+
+
+share = Path(__file__).parent / ".." / ".." / "share"
+
+simlibs = [str(share / "simlib.v"), str(share / "simcells.v")]
+
+if "prepare" in steps:
+ yosys(
+ """
+ read_verilog -icells uut.v
+ hierarchy -top uut; proc -noopt
+ write_rtlil uut.il
+ dump -o ports.list uut/x:*
+ """
+ )
+
+inputs = []
+outputs = []
+
+with open("ports.list") as ports_file:
+ for line in ports_file:
+ line = line.split()
+ if not line or line[0] != "wire":
+ continue
+ line = line[1:]
+ width = 1
+ if line[0] == "width":
+ width = int(line[1])
+ line = line[2:]
+ direction, seq, name = line
+ assert name.startswith("\\")
+ name = name[1:]
+ seq = int(seq)
+
+ if direction == "input":
+ inputs.append((seq, name, width))
+ else:
+ outputs.append((seq, name, width))
+
+inputs.sort()
+outputs.sort()
+
+input_width = sum(width for seq, name, width in inputs)
+output_width = sum(width for seq, name, width in outputs)
+
+if "prepare" in steps:
+ if args.seq:
+ patterns = [''.join(random.choices('01x', k=input_width)) for i in range(args.count)]
+ else:
+ if 3**input_width <= args.count * 2:
+ patterns = ["".join(bits) for bits in itertools.product(*["01x"] * input_width)]
+ else:
+ patterns = set()
+
+ for bit in '01x':
+ patterns.add(bit * input_width)
+
+ for bits in itertools.combinations('01x', 2):
+ for bit1, bit2 in itertools.permutations(bits):
+ for i in range(input_width):
+ pattern = [bit1] * input_width
+ pattern[i] = bit2
+ patterns.add(''.join(pattern))
+
+ for i, j in itertools.combinations(range(input_width), 2):
+ pattern = [bit1] * input_width
+ pattern[i] = bit2
+ pattern[j] = bit2
+ patterns.add(''.join(pattern))
+
+ for bit1, bit2, bit3 in itertools.permutations('01x'):
+ for i, j in itertools.combinations(range(input_width), 2):
+ pattern = [bit1] * input_width
+ pattern[i] = bit2
+ pattern[j] = bit3
+ patterns.add(''.join(pattern))
+
+ if len(patterns) > args.count // 2:
+ patterns = sorted(patterns)
+ random.shuffle(patterns)
+ patterns = set(patterns[:args.count // 2])
+
+ while len(patterns) < args.count:
+ pattern = ''.join(random.choices('01x', k=input_width))
+ patterns.add(pattern)
+
+ patterns = sorted(patterns)
+ with open("patterns.list", "w") as f:
+ for pattern in patterns:
+ print(pattern, file=f)
+else:
+ with open("patterns.list") as f:
+ patterns = [pattern.strip() for pattern in f]
+
+
+if "prepare" in steps:
+ with open("wrapper.v", "w") as wrapper_file:
+ print(
+ "module wrapper("
+ f"input [{input_width-1}:0] A, "
+ f"output [{output_width-1}:0] Y);",
+ file=wrapper_file,
+ )
+
+ connections = []
+ pos = 0
+ for seq, name, width in inputs:
+ connections.append(f".{name}(A[{pos+width-1}:{pos}])")
+ pos += width
+ pos = 0
+ for seq, name, width in outputs:
+ connections.append(f".{name}(Y[{pos+width-1}:{pos}])")
+ pos += width
+
+ print(f"uut uut({', '.join(connections)});", file=wrapper_file)
+ print("endmodule", file=wrapper_file)
+
+ yosys(
+ """
+ read_rtlil uut.il
+ read_verilog wrapper.v
+ hierarchy -top wrapper; proc -noopt
+ flatten; clean;
+ rename wrapper uut
+ write_rtlil wrapped.il
+ """
+ )
+
+ try:
+ yosys(
+ """
+ read_rtlil wrapped.il
+ dffunmap
+ xprop -required
+ check -assert
+ write_rtlil wrapped_xprop.il
+ """
+ )
+ except subprocess.CalledProcessError:
+ remove("wrapped_xprop.il")
+
+ with open("verilog_sim_tb.v", "w") as tb_file:
+ print("module top();", file=tb_file)
+ print(f"reg gclk;", file=tb_file)
+ print(f"reg [{input_width-1}:0] A;", file=tb_file)
+ print(f"wire [{output_width-1}:0] Y;", file=tb_file)
+ print(f"uut uut(.A(A), .Y(Y));", file=tb_file)
+ print("initial begin", file=tb_file)
+
+ for pattern in patterns:
+ print(
+ f' gclk = 1; #0; A[0] = 1\'b{pattern[-1]}; #0; A = {input_width}\'b{pattern}; #5; gclk = 0; $display("%b %b", A, Y); #5',
+ file=tb_file,
+ )
+
+ print(" $finish;", file=tb_file)
+ print("end", file=tb_file)
+ print("endmodule", file=tb_file)
+
+ with open("synth_tb.v", "w") as tb_file:
+ print("module top(input clk);", file=tb_file)
+ print(f"reg [{len(patterns).bit_length() - 1}:0] counter = 0;", file=tb_file)
+ print(f"reg [{input_width-1}:0] A;", file=tb_file)
+ print(f"(* gclk *) reg gclk;", file=tb_file)
+ print(f"wire [{output_width-1}:0] Y;", file=tb_file)
+ print(f"uut uut(.A(A), .Y(Y));", file=tb_file)
+ print(f"always @(posedge gclk) counter <= counter + 1;", file=tb_file)
+ print(f"always @* case (counter)", file=tb_file)
+ for i, pattern in enumerate(patterns):
+ print(f" {i:7} : A = {input_width}'b{pattern};", file=tb_file)
+ print(f" default : A = {input_width}'b{'x' * input_width};", file=tb_file)
+ print(f"endcase", file=tb_file)
+ print("endmodule", file=tb_file)
+
+ with open("const_tb.v", "w") as tb_file:
+ print("module top();", file=tb_file)
+ for i, pattern in enumerate(patterns):
+ print(
+ f"(* keep *) wire [{output_width-1}:0] Y_{i}; "
+ f"uut uut_{i}(.A({input_width}'b{pattern}), .Y(Y_{i}));",
+ file=tb_file,
+ )
+ print("endmodule", file=tb_file)
+
+if "verify" in steps:
+ try:
+ seq_args = " -tempinduct -set-init-undef" if args.seq else ""
+ yosys(
+ f"""
+ read_rtlil wrapped.il
+ copy uut gold
+ rename uut gate
+ design -push-copy
+ dffunmap
+ xprop -formal -split-inputs -required -debug-asserts gate
+ clk2fflogic
+ sat{seq_args} -enable_undef -set-def-inputs -prove-asserts -verify -show-all gate
+ design -pop
+
+ dffunmap
+ xprop -required -assume-encoding gate
+ miter -equiv -make_assert -flatten gold gate miter
+ clk2fflogic
+ sat{seq_args} -enable_undef -set-assumes -prove-asserts -verify -show-all miter
+ """
+ )
+ with open("verified", "w") as f:
+ pass
+ except subprocess.CalledProcessError:
+ remove("verified")
+
+
+for mode in ["", "_xprop"]:
+ if not Path(f"wrapped{mode}.il").is_file():
+ for expr in [f"expr{mode}", f"noexpr{mode}"]:
+ remove(f"vsim_{expr}.out")
+ continue
+
+ if "prepare" in steps:
+ yosys(
+ f"""
+ read_rtlil wrapped{mode}.il
+ chformal -remove
+ dffunmap
+ write_verilog -noparallelcase vsim_expr{mode}.v
+ write_verilog -noexpr vsim_noexpr{mode}.v
+ """
+ )
+
+ for expr in [f"expr{mode}", f"noexpr{mode}"]:
+ if f"vsim_{expr}" in steps:
+ subprocess.check_call(
+ [
+ "iverilog",
+ "-DSIMLIB_FF",
+ "-DSIMLIB_GLOBAL_CLOCK=top.gclk",
+ f"-DDUMPFILE=\"vsim_{expr}.vcd\"",
+ "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)
+
+for mode in ["", "_xprop"]:
+ if f"sim{mode}" not in steps:
+ continue
+ if not Path(f"wrapped{mode}.il").is_file():
+ remove(f"sim{mode}.out")
+ continue
+ yosys(
+ f"""
+ read_verilog synth_tb.v
+ read_rtlil wrapped{mode}.il
+ hierarchy -top top; proc -noopt
+ dffunmap
+ sim -clock clk -n {len(patterns) // 2} -vcd sim{mode}.vcd top
+ """
+ )
+
+ with open(f"sim{mode}.vcd") as fin, open(f"sim{mode}.out", "w") as fout:
+ vcdextract(["top.A", "top.Y"], ["top.counter"], fin, fout, len(patterns))
+
+for mode in ["", "_xprop"]:
+ if f"sat{mode}" not in steps:
+ continue
+ if not Path(f"wrapped{mode}.il").is_file():
+ remove(f"sat{mode}.out")
+ continue
+ chunk_size = len(patterns) if args.seq else 32
+ last_progress = 0
+ with open(f"sat{mode}.ys", "w") as ys:
+ for chunk_start in range(0, len(patterns), chunk_size):
+ chunk = patterns[chunk_start : chunk_start + chunk_size]
+ progress = (10 * chunk_start) // len(patterns)
+ if progress > last_progress:
+ print(f"log sat {progress}0%", file=ys)
+ last_progress = progress
+
+ append = "-a" if chunk_start else "-o"
+ print(
+ end=f"tee -q {append} sat{mode}.log sat -set-init-undef -seq {len(chunk)}"
+ " -show A -show Y -dump_vcd sat.vcd -enable_undef",
+ file=ys,
+ )
+ for i, pattern in enumerate(chunk, 1):
+ ad = pattern.replace("x", "0")
+ ax = pattern.replace("1", "0").replace("x", "1")
+ print(end=f" -set-at {i} A {input_width}'b{pattern}", file=ys)
+ print(file=ys)
+ print(f"log sat 100%", file=ys)
+
+ try:
+ yosys(
+ f"""
+ read_rtlil wrapped{mode}.il
+ clk2fflogic
+ script sat{mode}.ys
+ """
+ )
+ except subprocess.CalledProcessError:
+ remove(f"sat{mode}.out")
+ else:
+ sig_re = re.compile(
+ r" *[0-9]+ +\\([AY]) +(?:--|[0-9]+) +(?:--|[0-9a-f]+) +([01x]+)"
+ )
+ current_input = None
+ with open(f"sat{mode}.log") as logfile, open(f"sat{mode}.out", "w") as outfile:
+ for line in logfile:
+ match = sig_re.match(line)
+ if match:
+ if match[1] == "A":
+ current_input = match[2]
+ else:
+ print(current_input, match[2], file=outfile)
+
+for mode in ["", "_xprop"]:
+ if f"opt_expr{mode}" not in steps:
+ continue
+ if not Path(f"wrapped{mode}.il").is_file():
+ remove(f"opt_expr{mode}.out")
+ continue
+ yosys(
+ f"""
+ read_verilog const_tb.v
+ read_rtlil wrapped{mode}.il
+ hierarchy -top top; proc -noopt
+ flatten
+ opt_expr -keepdc; clean
+ dump -o opt_expr{mode}.list */\Y_*
+ """
+ )
+
+ values = []
+
+ connect_re = re.compile(r" *connect +\\Y_([0-9]+) +[0-9]+'([01x]+)$")
+ with open(f"opt_expr{mode}.list") as connections:
+ for line in connections:
+ match = connect_re.match(line)
+ if match:
+ seq = int(match[1])
+ data = match[2]
+ if len(data) < output_width:
+ data = data * output_width
+ values.append((seq, data))
+
+ values.sort()
+
+ with open(f"opt_expr{mode}.out", "w") as outfile:
+ for seq, data in values:
+ print(patterns[seq], data, file=outfile)
+
+
+if "compare" in steps:
+ groups = {}
+ missing = []
+
+ for output in all_outputs:
+ try:
+ with open(f"{output}.out") as f:
+ groups.setdefault(f.read(), []).append(output)
+ except FileNotFoundError:
+ missing.append(output)
+
+ verified = Path(f"verified").is_file()
+
+ with open("status", "w") as status:
+ name = Path('.').absolute().name
+
+ status_list = []
+
+ if len(groups) > 1:
+ status_list.append("mismatch")
+ if not verified:
+ status_list.append("failed-verify")
+ if missing:
+ status_list.append("missing")
+ if not status_list:
+ status_list.append("ok")
+ print(f"{name}: {', '.join(status_list)}", file=status)
+
+ if len(groups) > 1:
+ print("output differences:", file=status)
+ for group in groups.values():
+ print(" -", *group, file=status)
+ if missing:
+ print("missing:", file=status)
+ print(" -", *missing, file=status)
+
+ with open("status") as status:
+ print(end=status.read())
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-07 19:32:28 +0000