aboutsummaryrefslogtreecommitdiffstats
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/calc.cc60
-rw-r--r--kernel/celledges.h4
-rw-r--r--kernel/celltypes.h40
-rw-r--r--kernel/constids.inc4
-rw-r--r--kernel/driver.cc2
-rw-r--r--kernel/ff.h486
-rw-r--r--kernel/ffinit.h141
-rw-r--r--kernel/hashlib.h2
-rw-r--r--kernel/log.cc12
-rw-r--r--kernel/log.h37
-rw-r--r--kernel/macc.h2
-rw-r--r--kernel/mem.cc436
-rw-r--r--kernel/mem.h78
-rw-r--r--kernel/modtools.h8
-rw-r--r--kernel/register.cc10
-rw-r--r--kernel/register.h12
-rw-r--r--kernel/rtlil.cc474
-rw-r--r--kernel/rtlil.h52
-rw-r--r--kernel/satgen.cc1239
-rw-r--r--kernel/satgen.h1178
-rw-r--r--kernel/yosys.cc96
-rw-r--r--kernel/yosys.h30
22 files changed, 3064 insertions, 1339 deletions
diff --git a/kernel/calc.cc b/kernel/calc.cc
index ae18809d3..d54ccbc10 100644
--- a/kernel/calc.cc
+++ b/kernel/calc.cc
@@ -275,10 +275,15 @@ RTLIL::Const RTLIL::const_logic_or(const RTLIL::Const &arg1, const RTLIL::Const
return result;
}
-static RTLIL::Const const_shift_worker(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool sign_ext, int direction, int result_len)
+// Shift `arg1` by `arg2` bits.
+// If `direction` is +1, `arg1` is shifted right by `arg2` bits; if `direction` is -1, `arg1` is shifted left by `arg2` bits.
+// If `signed2` is true, `arg2` is interpreted as a signed integer; a negative `arg2` will cause a shift in the opposite direction.
+// Any required bits outside the bounds of `arg1` are padded with `vacant_bits` unless `sign_ext` is true, in which case any bits outside the left
+// bounds are filled with the leftmost bit of `arg1` (arithmetic shift).
+static RTLIL::Const const_shift_worker(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool sign_ext, bool signed2, int direction, int result_len, RTLIL::State vacant_bits = RTLIL::State::S0)
{
int undef_bit_pos = -1;
- BigInteger offset = const2big(arg2, false, undef_bit_pos) * direction;
+ BigInteger offset = const2big(arg2, signed2, undef_bit_pos) * direction;
if (result_len < 0)
result_len = arg1.bits.size();
@@ -290,9 +295,9 @@ static RTLIL::Const const_shift_worker(const RTLIL::Const &arg1, const RTLIL::Co
for (int i = 0; i < result_len; i++) {
BigInteger pos = BigInteger(i) + offset;
if (pos < 0)
- result.bits[i] = RTLIL::State::S0;
+ result.bits[i] = vacant_bits;
else if (pos >= BigInteger(int(arg1.bits.size())))
- result.bits[i] = sign_ext ? arg1.bits.back() : RTLIL::State::S0;
+ result.bits[i] = sign_ext ? arg1.bits.back() : vacant_bits;
else
result.bits[i] = arg1.bits[pos.toInt()];
}
@@ -304,61 +309,36 @@ RTLIL::Const RTLIL::const_shl(const RTLIL::Const &arg1, const RTLIL::Const &arg2
{
RTLIL::Const arg1_ext = arg1;
extend_u0(arg1_ext, result_len, signed1);
- return const_shift_worker(arg1_ext, arg2, false, -1, result_len);
+ return const_shift_worker(arg1_ext, arg2, false, false, -1, result_len);
}
RTLIL::Const RTLIL::const_shr(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool, int result_len)
{
RTLIL::Const arg1_ext = arg1;
extend_u0(arg1_ext, max(result_len, GetSize(arg1)), signed1);
- return const_shift_worker(arg1_ext, arg2, false, +1, result_len);
-}
-
-RTLIL::Const RTLIL::const_sshl(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
-{
- if (!signed1)
- return const_shl(arg1, arg2, signed1, signed2, result_len);
- return const_shift_worker(arg1, arg2, true, -1, result_len);
+ return const_shift_worker(arg1_ext, arg2, false, false, +1, result_len);
}
-RTLIL::Const RTLIL::const_sshr(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
+RTLIL::Const RTLIL::const_sshl(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool, int result_len)
{
- if (!signed1)
- return const_shr(arg1, arg2, signed1, signed2, result_len);
- return const_shift_worker(arg1, arg2, true, +1, result_len);
+ return const_shift_worker(arg1, arg2, signed1, false, -1, result_len);
}
-static RTLIL::Const const_shift_shiftx(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool, bool signed2, int result_len, RTLIL::State other_bits)
+RTLIL::Const RTLIL::const_sshr(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool, int result_len)
{
- int undef_bit_pos = -1;
- BigInteger offset = const2big(arg2, signed2, undef_bit_pos);
-
- if (result_len < 0)
- result_len = arg1.bits.size();
-
- RTLIL::Const result(RTLIL::State::Sx, result_len);
- if (undef_bit_pos >= 0)
- return result;
-
- for (int i = 0; i < result_len; i++) {
- BigInteger pos = BigInteger(i) + offset;
- if (pos < 0 || pos >= BigInteger(int(arg1.bits.size())))
- result.bits[i] = other_bits;
- else
- result.bits[i] = arg1.bits[pos.toInt()];
- }
-
- return result;
+ return const_shift_worker(arg1, arg2, signed1, false, +1, result_len);
}
RTLIL::Const RTLIL::const_shift(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
{
- return const_shift_shiftx(arg1, arg2, signed1, signed2, result_len, RTLIL::State::S0);
+ RTLIL::Const arg1_ext = arg1;
+ extend_u0(arg1_ext, max(result_len, GetSize(arg1)), signed1);
+ return const_shift_worker(arg1_ext, arg2, false, signed2, +1, result_len);
}
-RTLIL::Const RTLIL::const_shiftx(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
+RTLIL::Const RTLIL::const_shiftx(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool, bool signed2, int result_len)
{
- return const_shift_shiftx(arg1, arg2, signed1, signed2, result_len, RTLIL::State::Sx);
+ return const_shift_worker(arg1, arg2, false, signed2, +1, result_len, RTLIL::State::Sx);
}
RTLIL::Const RTLIL::const_lt(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
diff --git a/kernel/celledges.h b/kernel/celledges.h
index 2cc297cb2..d105e4009 100644
--- a/kernel/celledges.h
+++ b/kernel/celledges.h
@@ -38,7 +38,7 @@ struct FwdCellEdgesDatabase : AbstractCellEdgesDatabase
dict<SigBit, pool<SigBit>> db;
FwdCellEdgesDatabase(SigMap &sigmap) : sigmap(sigmap) { }
- void add_edge(RTLIL::Cell *cell, RTLIL::IdString from_port, int from_bit, RTLIL::IdString to_port, int to_bit, int) YS_OVERRIDE {
+ void add_edge(RTLIL::Cell *cell, RTLIL::IdString from_port, int from_bit, RTLIL::IdString to_port, int to_bit, int) override {
SigBit from_sigbit = sigmap(cell->getPort(from_port)[from_bit]);
SigBit to_sigbit = sigmap(cell->getPort(to_port)[to_bit]);
db[from_sigbit].insert(to_sigbit);
@@ -51,7 +51,7 @@ struct RevCellEdgesDatabase : AbstractCellEdgesDatabase
dict<SigBit, pool<SigBit>> db;
RevCellEdgesDatabase(SigMap &sigmap) : sigmap(sigmap) { }
- void add_edge(RTLIL::Cell *cell, RTLIL::IdString from_port, int from_bit, RTLIL::IdString to_port, int to_bit, int) YS_OVERRIDE {
+ void add_edge(RTLIL::Cell *cell, RTLIL::IdString from_port, int from_bit, RTLIL::IdString to_port, int to_bit, int) override {
SigBit from_sigbit = sigmap(cell->getPort(from_port)[from_bit]);
SigBit to_sigbit = sigmap(cell->getPort(to_port)[to_bit]);
db[to_sigbit].insert(from_sigbit);
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index db54436cb..944cb301a 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -139,8 +139,14 @@ struct CellTypes
setup_type(ID($dff), {ID::CLK, ID::D}, {ID::Q});
setup_type(ID($dffe), {ID::CLK, ID::EN, ID::D}, {ID::Q});
setup_type(ID($dffsr), {ID::CLK, ID::SET, ID::CLR, ID::D}, {ID::Q});
+ setup_type(ID($dffsre), {ID::CLK, ID::SET, ID::CLR, ID::D, ID::EN}, {ID::Q});
setup_type(ID($adff), {ID::CLK, ID::ARST, ID::D}, {ID::Q});
+ setup_type(ID($adffe), {ID::CLK, ID::ARST, ID::D, ID::EN}, {ID::Q});
+ setup_type(ID($sdff), {ID::CLK, ID::SRST, ID::D}, {ID::Q});
+ setup_type(ID($sdffe), {ID::CLK, ID::SRST, ID::D, ID::EN}, {ID::Q});
+ setup_type(ID($sdffce), {ID::CLK, ID::SRST, ID::D, ID::EN}, {ID::Q});
setup_type(ID($dlatch), {ID::EN, ID::D}, {ID::Q});
+ setup_type(ID($adlatch), {ID::EN, ID::D, ID::ARST}, {ID::Q});
setup_type(ID($dlatchsr), {ID::EN, ID::SET, ID::CLR, ID::D}, {ID::Q});
}
@@ -210,14 +216,48 @@ struct CellTypes
for (auto c1 : list_np)
for (auto c2 : list_np)
+ for (auto c3 : list_01)
+ for (auto c4 : list_np)
+ setup_type(stringf("$_DFFE_%c%c%c%c_", c1, c2, c3, c4), {ID::C, ID::R, ID::D, ID::E}, {ID::Q});
+
+ for (auto c1 : list_np)
+ for (auto c2 : list_np)
for (auto c3 : list_np)
setup_type(stringf("$_DFFSR_%c%c%c_", c1, c2, c3), {ID::C, ID::S, ID::R, ID::D}, {ID::Q});
for (auto c1 : list_np)
+ for (auto c2 : list_np)
+ for (auto c3 : list_np)
+ for (auto c4 : list_np)
+ setup_type(stringf("$_DFFSRE_%c%c%c%c_", c1, c2, c3, c4), {ID::C, ID::S, ID::R, ID::D, ID::E}, {ID::Q});
+
+ for (auto c1 : list_np)
+ for (auto c2 : list_np)
+ for (auto c3 : list_01)
+ setup_type(stringf("$_SDFF_%c%c%c_", c1, c2, c3), {ID::C, ID::R, ID::D}, {ID::Q});
+
+ for (auto c1 : list_np)
+ for (auto c2 : list_np)
+ for (auto c3 : list_01)
+ for (auto c4 : list_np)
+ setup_type(stringf("$_SDFFE_%c%c%c%c_", c1, c2, c3, c4), {ID::C, ID::R, ID::D, ID::E}, {ID::Q});
+
+ for (auto c1 : list_np)
+ for (auto c2 : list_np)
+ for (auto c3 : list_01)
+ for (auto c4 : list_np)
+ setup_type(stringf("$_SDFFCE_%c%c%c%c_", c1, c2, c3, c4), {ID::C, ID::R, ID::D, ID::E}, {ID::Q});
+
+ for (auto c1 : list_np)
setup_type(stringf("$_DLATCH_%c_", c1), {ID::E, ID::D}, {ID::Q});
for (auto c1 : list_np)
for (auto c2 : list_np)
+ for (auto c3 : list_01)
+ setup_type(stringf("$_DLATCH_%c%c%c_", c1, c2, c3), {ID::E, ID::R, ID::D}, {ID::Q});
+
+ for (auto c1 : list_np)
+ for (auto c2 : list_np)
for (auto c3 : list_np)
setup_type(stringf("$_DLATCHSR_%c%c%c_", c1, c2, c3), {ID::E, ID::S, ID::R, ID::D}, {ID::Q});
}
diff --git a/kernel/constids.inc b/kernel/constids.inc
index 383d7c615..3c2ff9beb 100644
--- a/kernel/constids.inc
+++ b/kernel/constids.inc
@@ -158,6 +158,9 @@ X(SRC_EN)
X(SRC_PEN)
X(SRC_POL)
X(SRC_WIDTH)
+X(SRST)
+X(SRST_POLARITY)
+X(SRST_VALUE)
X(STATE_BITS)
X(STATE_NUM)
X(STATE_NUM_LOG2)
@@ -169,6 +172,7 @@ X(T)
X(TABLE)
X(techmap_autopurge)
X(_TECHMAP_BITS_CONNMAP_)
+X(_TECHMAP_CELLNAME_)
X(_TECHMAP_CELLTYPE_)
X(techmap_celltype)
X(_TECHMAP_FAIL_)
diff --git a/kernel/driver.cc b/kernel/driver.cc
index 57ed7b8b4..b55f02837 100644
--- a/kernel/driver.cc
+++ b/kernel/driver.cc
@@ -267,9 +267,11 @@ int main(int argc, char **argv)
printf("\n");
printf(" -s scriptfile\n");
printf(" execute the commands in the script file\n");
+#ifdef YOSYS_ENABLE_TCL
printf("\n");
printf(" -c tcl_scriptfile\n");
printf(" execute the commands in the tcl script file (see 'help tcl' for details)\n");
+#endif
printf("\n");
printf(" -p command\n");
printf(" execute the commands\n");
diff --git a/kernel/ff.h b/kernel/ff.h
new file mode 100644
index 000000000..0aecbaa2a
--- /dev/null
+++ b/kernel/ff.h
@@ -0,0 +1,486 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2020 Marcelina Kościelnicka <mwk@0x04.net>
+ *
+ * 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.
+ *
+ */
+
+#ifndef FF_H
+#define FF_H
+
+#include "kernel/yosys.h"
+#include "kernel/ffinit.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+struct FfData {
+ FfInitVals *initvals;
+ SigSpec sig_q;
+ SigSpec sig_d;
+ SigSpec sig_clk;
+ SigSpec sig_en;
+ SigSpec sig_arst;
+ SigSpec sig_srst;
+ SigSpec sig_clr;
+ SigSpec sig_set;
+ bool has_d;
+ bool has_clk;
+ bool has_en;
+ bool has_srst;
+ bool has_arst;
+ bool has_sr;
+ bool ce_over_srst;
+ bool is_fine;
+ bool pol_clk;
+ bool pol_en;
+ bool pol_arst;
+ bool pol_srst;
+ bool pol_clr;
+ bool pol_set;
+ Const val_arst;
+ Const val_srst;
+ Const val_init;
+ Const val_d;
+ bool d_is_const;
+ int width;
+ dict<IdString, Const> attributes;
+
+ FfData(FfInitVals *initvals, Cell *cell = nullptr) : initvals(initvals) {
+ width = 0;
+ has_d = true;
+ has_clk = false;
+ has_en = false;
+ has_srst = false;
+ has_arst = false;
+ has_sr = false;
+ ce_over_srst = false;
+ is_fine = false;
+ pol_clk = false;
+ pol_en = false;
+ pol_arst = false;
+ pol_srst = false;
+ pol_clr = false;
+ pol_set = false;
+ d_is_const = false;
+
+ if (!cell)
+ return;
+
+ sig_q = cell->getPort(ID::Q);
+ width = GetSize(sig_q);
+ attributes = cell->attributes;
+
+ if (initvals)
+ val_init = (*initvals)(sig_q);
+
+ std::string type_str = cell->type.str();
+
+ if (cell->type.in(ID($ff), ID($dff), ID($dffe), ID($dffsr), ID($dffsre), ID($adff), ID($adffe), ID($sdff), ID($sdffe), ID($sdffce), ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr))) {
+ if (cell->type == ID($sr)) {
+ has_d = false;
+ } else {
+ sig_d = cell->getPort(ID::D);
+ }
+ if (!cell->type.in(ID($ff), ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr))) {
+ has_clk = true;
+ sig_clk = cell->getPort(ID::CLK);
+ pol_clk = cell->getParam(ID::CLK_POLARITY).as_bool();
+ }
+ if (cell->type.in(ID($dffe), ID($dffsre), ID($adffe), ID($sdffe), ID($sdffce), ID($dlatch), ID($adlatch), ID($dlatchsr))) {
+ has_en = true;
+ sig_en = cell->getPort(ID::EN);
+ pol_en = cell->getParam(ID::EN_POLARITY).as_bool();
+ }
+ if (cell->type.in(ID($dffsr), ID($dffsre), ID($dlatchsr), ID($sr))) {
+ has_sr = true;
+ sig_clr = cell->getPort(ID::CLR);
+ sig_set = cell->getPort(ID::SET);
+ pol_clr = cell->getParam(ID::CLR_POLARITY).as_bool();
+ pol_set = cell->getParam(ID::SET_POLARITY).as_bool();
+ }
+ if (cell->type.in(ID($adff), ID($adffe), ID($adlatch))) {
+ has_arst = true;
+ sig_arst = cell->getPort(ID::ARST);
+ pol_arst = cell->getParam(ID::ARST_POLARITY).as_bool();
+ val_arst = cell->getParam(ID::ARST_VALUE);
+ }
+ if (cell->type.in(ID($sdff), ID($sdffe), ID($sdffce))) {
+ has_srst = true;
+ sig_srst = cell->getPort(ID::SRST);
+ pol_srst = cell->getParam(ID::SRST_POLARITY).as_bool();
+ val_srst = cell->getParam(ID::SRST_VALUE);
+ ce_over_srst = cell->type == ID($sdffce);
+ }
+ } else if (cell->type == ID($_FF_)) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ } else if (type_str.substr(0, 5) == "$_SR_") {
+ is_fine = true;
+ has_d = false;
+ has_sr = true;
+ pol_set = type_str[5] == 'P';
+ pol_clr = type_str[6] == 'P';
+ sig_set = cell->getPort(ID::S);
+ sig_clr = cell->getPort(ID::R);
+ } else if (type_str.substr(0, 6) == "$_DFF_" && type_str.size() == 8) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[6] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ } else if (type_str.substr(0, 7) == "$_DFFE_" && type_str.size() == 10) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[7] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_en = true;
+ pol_en = type_str[8] == 'P';
+ sig_en = cell->getPort(ID::E);
+ } else if (type_str.substr(0, 6) == "$_DFF_" && type_str.size() == 10) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[6] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_arst = true;
+ pol_arst = type_str[7] == 'P';
+ sig_arst = cell->getPort(ID::R);
+ val_arst = type_str[8] == '1' ? State::S1 : State::S0;
+ } else if (type_str.substr(0, 7) == "$_DFFE_" && type_str.size() == 12) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[7] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_arst = true;
+ pol_arst = type_str[8] == 'P';
+ sig_arst = cell->getPort(ID::R);
+ val_arst = type_str[9] == '1' ? State::S1 : State::S0;
+ has_en = true;
+ pol_en = type_str[10] == 'P';
+ sig_en = cell->getPort(ID::E);
+ } else if (type_str.substr(0, 8) == "$_DFFSR_" && type_str.size() == 12) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[8] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_sr = true;
+ pol_set = type_str[9] == 'P';
+ pol_clr = type_str[10] == 'P';
+ sig_set = cell->getPort(ID::S);
+ sig_clr = cell->getPort(ID::R);
+ } else if (type_str.substr(0, 9) == "$_DFFSRE_" && type_str.size() == 14) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[9] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_sr = true;
+ pol_set = type_str[10] == 'P';
+ pol_clr = type_str[11] == 'P';
+ sig_set = cell->getPort(ID::S);
+ sig_clr = cell->getPort(ID::R);
+ has_en = true;
+ pol_en = type_str[12] == 'P';
+ sig_en = cell->getPort(ID::E);
+ } else if (type_str.substr(0, 7) == "$_SDFF_" && type_str.size() == 11) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[7] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_srst = true;
+ pol_srst = type_str[8] == 'P';
+ sig_srst = cell->getPort(ID::R);
+ val_srst = type_str[9] == '1' ? State::S1 : State::S0;
+ } else if (type_str.substr(0, 8) == "$_SDFFE_" && type_str.size() == 13) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[8] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_srst = true;
+ pol_srst = type_str[9] == 'P';
+ sig_srst = cell->getPort(ID::R);
+ val_srst = type_str[10] == '1' ? State::S1 : State::S0;
+ has_en = true;
+ pol_en = type_str[11] == 'P';
+ sig_en = cell->getPort(ID::E);
+ } else if (type_str.substr(0, 9) == "$_SDFFCE_" && type_str.size() == 14) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[9] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_srst = true;
+ pol_srst = type_str[10] == 'P';
+ sig_srst = cell->getPort(ID::R);
+ val_srst = type_str[11] == '1' ? State::S1 : State::S0;
+ has_en = true;
+ pol_en = type_str[12] == 'P';
+ sig_en = cell->getPort(ID::E);
+ ce_over_srst = true;
+ } else if (type_str.substr(0, 9) == "$_DLATCH_" && type_str.size() == 11) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_en = true;
+ pol_en = type_str[9] == 'P';
+ sig_en = cell->getPort(ID::E);
+ } else if (type_str.substr(0, 9) == "$_DLATCH_" && type_str.size() == 13) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_en = true;
+ pol_en = type_str[9] == 'P';
+ sig_en = cell->getPort(ID::E);
+ has_arst = true;
+ pol_arst = type_str[10] == 'P';
+ sig_arst = cell->getPort(ID::R);
+ val_arst = type_str[11] == '1' ? State::S1 : State::S0;
+ } else if (type_str.substr(0, 11) == "$_DLATCHSR_" && type_str.size() == 15) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_en = true;
+ pol_en = type_str[11] == 'P';
+ sig_en = cell->getPort(ID::E);
+ has_sr = true;
+ pol_set = type_str[12] == 'P';
+ pol_clr = type_str[13] == 'P';
+ sig_set = cell->getPort(ID::S);
+ sig_clr = cell->getPort(ID::R);
+ } else {
+ log_assert(0);
+ }
+ if (has_d && sig_d.is_fully_const()) {
+ d_is_const = true;
+ val_d = sig_d.as_const();
+ if (has_en && !has_clk && !has_sr && !has_arst) {
+ // Plain D latches with const D treated specially.
+ has_en = has_d = false;
+ has_arst = true;
+ sig_arst = sig_en;
+ pol_arst = pol_en;
+ val_arst = val_d;
+ }
+ }
+ }
+
+ // Returns a FF identical to this one, but only keeping bit indices from the argument.
+ FfData slice(const std::vector<int> &bits) {
+ FfData res(initvals);
+ res.sig_clk = sig_clk;
+ res.sig_en = sig_en;
+ res.sig_arst = sig_arst;
+ res.sig_srst = sig_srst;
+ res.has_d = has_d;
+ res.has_clk = has_clk;
+ res.has_en = has_en;
+ res.has_arst = has_arst;
+ res.has_srst = has_srst;
+ res.has_sr = has_sr;
+ res.ce_over_srst = ce_over_srst;
+ res.is_fine = is_fine;
+ res.pol_clk = pol_clk;
+ res.pol_en = pol_en;
+ res.pol_arst = pol_arst;
+ res.pol_srst = pol_srst;
+ res.pol_clr = pol_clr;
+ res.pol_set = pol_set;
+ res.attributes = attributes;
+ for (int i : bits) {
+ res.sig_q.append(sig_q[i]);
+ if (has_d)
+ res.sig_d.append(sig_d[i]);
+ if (has_sr) {
+ res.sig_clr.append(sig_clr[i]);
+ res.sig_set.append(sig_set[i]);
+ }
+ if (has_arst)
+ res.val_arst.bits.push_back(val_arst[i]);
+ if (has_srst)
+ res.val_srst.bits.push_back(val_srst[i]);
+ res.val_init.bits.push_back(val_init[i]);
+ }
+ res.width = GetSize(res.sig_q);
+ // Slicing bits out may cause D to become const.
+ if (has_d && res.sig_d.is_fully_const()) {
+ res.d_is_const = true;
+ res.val_d = res.sig_d.as_const();
+ }
+ return res;
+ }
+
+ void unmap_ce(Module *module) {
+ if (!has_en)
+ return;
+ log_assert(has_clk);
+ if (has_srst && ce_over_srst)
+ unmap_srst(module);
+
+ if (!is_fine) {
+ if (pol_en)
+ sig_d = module->Mux(NEW_ID, sig_q, sig_d, sig_en);
+ else
+ sig_d = module->Mux(NEW_ID, sig_d, sig_q, sig_en);
+ } else {
+ if (pol_en)
+ sig_d = module->MuxGate(NEW_ID, sig_q, sig_d, sig_en);
+ else
+ sig_d = module->MuxGate(NEW_ID, sig_d, sig_q, sig_en);
+ }
+ has_en = false;
+ }
+
+ void unmap_srst(Module *module) {
+ if (!has_srst)
+ return;
+ if (has_en && !ce_over_srst)
+ unmap_ce(module);
+
+ if (!is_fine) {
+ if (pol_srst)
+ sig_d = module->Mux(NEW_ID, sig_d, val_srst, sig_srst);
+ else
+ sig_d = module->Mux(NEW_ID, val_srst, sig_d, sig_srst);
+ } else {
+ if (pol_srst)
+ sig_d = module->MuxGate(NEW_ID, sig_d, val_srst[0], sig_srst);
+ else
+ sig_d = module->MuxGate(NEW_ID, val_srst[0], sig_d, sig_srst);
+ }
+ has_srst = false;
+ }
+
+ void unmap_ce_srst(Module *module) {
+ unmap_ce(module);
+ unmap_srst(module);
+ }
+
+ Cell *emit(Module *module, IdString name) {
+ if (!width)
+ return nullptr;
+ if (!has_d && !has_sr) {
+ if (has_arst) {
+ // Convert this case to a D latch.
+ has_d = has_en = true;
+ has_arst = false;
+ sig_d = val_arst;
+ sig_en = sig_arst;
+ pol_en = pol_arst;
+ } else {
+ // No control inputs left. Turn into a const driver.
+ initvals->remove_init(sig_q);
+ module->connect(sig_q, val_init);
+ return nullptr;
+ }
+ }
+ initvals->set_init(sig_q, val_init);
+ Cell *cell;
+ if (!is_fine) {
+ if (!has_d) {
+ log_assert(has_sr);
+ cell = module->addSr(name, sig_set, sig_clr, sig_q, pol_set, pol_clr);
+ } else if (!has_clk && !has_en) {
+ log_assert(!has_arst);
+ log_assert(!has_srst);
+ log_assert(!has_sr);
+ cell = module->addFf(name, sig_d, sig_q);
+ } else if (!has_clk) {
+ log_assert(!has_srst);
+ if (has_sr)
+ cell = module->addDlatchsr(name, sig_en, sig_set, sig_clr, sig_d, sig_q, pol_en, pol_set, pol_clr);
+ else if (has_arst)
+ cell = module->addAdlatch(name, sig_en, sig_arst, sig_d, sig_q, val_arst, pol_en, pol_arst);
+ else
+ cell = module->addDlatch(name, sig_en, sig_d, sig_q, pol_en);
+ } else {
+ if (has_sr) {
+ if (has_en)
+ cell = module->addDffsre(name, sig_clk, sig_en, sig_set, sig_clr, sig_d, sig_q, pol_clk, pol_en, pol_set, pol_clr);
+ else
+ cell = module->addDffsr(name, sig_clk, sig_set, sig_clr, sig_d, sig_q, pol_clk, pol_set, pol_clr);
+ } else if (has_arst) {
+ if (has_en)
+ cell = module->addAdffe(name, sig_clk, sig_en, sig_arst, sig_d, sig_q, val_arst, pol_clk, pol_en, pol_arst);
+ else
+ cell = module->addAdff(name, sig_clk, sig_arst, sig_d, sig_q, val_arst, pol_clk, pol_arst);
+ } else if (has_srst) {
+ if (has_en)
+ if (ce_over_srst)
+ cell = module->addSdffce(name, sig_clk, sig_en, sig_srst, sig_d, sig_q, val_srst, pol_clk, pol_en, pol_srst);
+ else
+ cell = module->addSdffe(name, sig_clk, sig_en, sig_srst, sig_d, sig_q, val_srst, pol_clk, pol_en, pol_srst);
+ else
+ cell = module->addSdff(name, sig_clk, sig_srst, sig_d, sig_q, val_srst, pol_clk, pol_srst);
+ } else {
+ if (has_en)
+ cell = module->addDffe(name, sig_clk, sig_en, sig_d, sig_q, pol_clk, pol_en);
+ else
+ cell = module->addDff(name, sig_clk, sig_d, sig_q, pol_clk);
+ }
+ }
+ } else {
+ if (!has_d) {
+ log_assert(has_sr);
+ cell = module->addSrGate(name, sig_set, sig_clr, sig_q, pol_set, pol_clr);
+ } else if (!has_clk && !has_en) {
+ log_assert(!has_arst);
+ log_assert(!has_srst);
+ log_assert(!has_sr);
+ cell = module->addFfGate(name, sig_d, sig_q);
+ } else if (!has_clk) {
+ log_assert(!has_srst);
+ if (has_sr)
+ cell = module->addDlatchsrGate(name, sig_en, sig_set, sig_clr, sig_d, sig_q, pol_en, pol_set, pol_clr);
+ else if (has_arst)
+ cell = module->addAdlatchGate(name, sig_en, sig_arst, sig_d, sig_q, val_arst.as_bool(), pol_en, pol_arst);
+ else
+ cell = module->addDlatchGate(name, sig_en, sig_d, sig_q, pol_en);
+ } else {
+ if (has_sr) {
+ if (has_en)
+ cell = module->addDffsreGate(name, sig_clk, sig_en, sig_set, sig_clr, sig_d, sig_q, pol_clk, pol_en, pol_set, pol_clr);
+ else
+ cell = module->addDffsrGate(name, sig_clk, sig_set, sig_clr, sig_d, sig_q, pol_clk, pol_set, pol_clr);
+ } else if (has_arst) {
+ if (has_en)
+ cell = module->addAdffeGate(name, sig_clk, sig_en, sig_arst, sig_d, sig_q, val_arst.as_bool(), pol_clk, pol_en, pol_arst);
+ else
+ cell = module->addAdffGate(name, sig_clk, sig_arst, sig_d, sig_q, val_arst.as_bool(), pol_clk, pol_arst);
+ } else if (has_srst) {
+ if (has_en)
+ if (ce_over_srst)
+ cell = module->addSdffceGate(name, sig_clk, sig_en, sig_srst, sig_d, sig_q, val_srst.as_bool(), pol_clk, pol_en, pol_srst);
+ else
+ cell = module->addSdffeGate(name, sig_clk, sig_en, sig_srst, sig_d, sig_q, val_srst.as_bool(), pol_clk, pol_en, pol_srst);
+ else
+ cell = module->addSdffGate(name, sig_clk, sig_srst, sig_d, sig_q, val_srst.as_bool(), pol_clk, pol_srst);
+ } else {
+ if (has_en)
+ cell = module->addDffeGate(name, sig_clk, sig_en, sig_d, sig_q, pol_clk, pol_en);
+ else
+ cell = module->addDffGate(name, sig_clk, sig_d, sig_q, pol_clk);
+ }
+ }
+ }
+ cell->attributes = attributes;
+ return cell;
+ }
+};
+
+YOSYS_NAMESPACE_END
+
+#endif
diff --git a/kernel/ffinit.h b/kernel/ffinit.h
new file mode 100644
index 000000000..025b0c862
--- /dev/null
+++ b/kernel/ffinit.h
@@ -0,0 +1,141 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2020 Marcelina Kościelnicka <mwk@0x04.net>
+ *
+ * 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.
+ *
+ */
+
+#ifndef FFINIT_H
+#define FFINIT_H
+
+#include "kernel/yosys.h"
+#include "kernel/sigtools.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+struct FfInitVals
+{
+ const SigMap *sigmap;
+ RTLIL::Module *module;
+ dict<SigBit, std::pair<State,SigBit>> initbits;
+
+ void set(const SigMap *sigmap_, RTLIL::Module *module)
+ {
+ sigmap = sigmap_;
+ initbits.clear();
+ for (auto wire : module->wires())
+ {
+ if (wire->attributes.count(ID::init) == 0)
+ continue;
+
+ SigSpec wirebits = (*sigmap)(wire);
+ Const initval = wire->attributes.at(ID::init);
+
+ for (int i = 0; i < GetSize(wirebits) && i < GetSize(initval); i++)
+ {
+ SigBit bit = wirebits[i];
+ State val = initval[i];
+
+ if (val != State::S0 && val != State::S1 && bit.wire != nullptr)
+ continue;
+
+ if (initbits.count(bit)) {
+ if (initbits.at(bit).first != val)
+ log_error("Conflicting init values for signal %s (%s = %s != %s).\n",
+ log_signal(bit), log_signal(SigBit(wire, i)),
+ log_signal(val), log_signal(initbits.at(bit).first));
+ continue;
+ }
+
+ initbits[bit] = std::make_pair(val,SigBit(wire,i));
+ }
+ }
+ }
+
+ RTLIL::State operator()(RTLIL::SigBit bit) const
+ {
+ auto it = initbits.find((*sigmap)(bit));
+ if (it != initbits.end())
+ return it->second.first;
+ else
+ return State::Sx;
+ }
+
+ RTLIL::Const operator()(const RTLIL::SigSpec &sig) const
+ {
+ RTLIL::Const res;
+ for (auto bit : sig)
+ res.bits.push_back((*this)(bit));
+ return res;
+ }
+
+ void set_init(RTLIL::SigBit bit, RTLIL::State val)
+ {
+ SigBit mbit = (*sigmap)(bit);
+ SigBit abit = bit;
+ auto it = initbits.find(mbit);
+ if (it != initbits.end())
+ abit = it->second.second;
+ else if (val == State::Sx)
+ return;
+ log_assert(abit.wire);
+ initbits[mbit] = std::make_pair(val,abit);
+ auto it2 = abit.wire->attributes.find(ID::init);
+ if (it2 != abit.wire->attributes.end()) {
+ it2->second[abit.offset] = val;
+ if (it2->second.is_fully_undef())
+ abit.wire->attributes.erase(it2);
+ } else if (val != State::Sx) {
+ Const cval(State::Sx, GetSize(abit.wire));
+ cval[abit.offset] = val;
+ abit.wire->attributes[ID::init] = cval;
+ }
+ }
+
+ void set_init(const RTLIL::SigSpec &sig, RTLIL::Const val)
+ {
+ log_assert(GetSize(sig) == GetSize(val));
+ for (int i = 0; i < GetSize(sig); i++)
+ set_init(sig[i], val[i]);
+ }
+
+ void remove_init(RTLIL::SigBit bit)
+ {
+ set_init(bit, State::Sx);
+ }
+
+ void remove_init(const RTLIL::SigSpec &sig)
+ {
+ for (auto bit : sig)
+ remove_init(bit);
+ }
+
+ void clear()
+ {
+ initbits.clear();
+ }
+
+ FfInitVals (const SigMap *sigmap, RTLIL::Module *module)
+ {
+ set(sigmap, module);
+ }
+
+ FfInitVals () {}
+};
+
+
+YOSYS_NAMESPACE_END
+
+#endif
diff --git a/kernel/hashlib.h b/kernel/hashlib.h
index 5c87b55f5..a523afadd 100644
--- a/kernel/hashlib.h
+++ b/kernel/hashlib.h
@@ -363,6 +363,7 @@ public:
public:
const_iterator() { }
const_iterator operator++() { index--; return *this; }
+ const_iterator operator+=(int amt) { index -= amt; return *this; }
bool operator<(const const_iterator &other) const { return index > other.index; }
bool operator==(const const_iterator &other) const { return index == other.index; }
bool operator!=(const const_iterator &other) const { return index != other.index; }
@@ -380,6 +381,7 @@ public:
public:
iterator() { }
iterator operator++() { index--; return *this; }
+ iterator operator+=(int amt) { index -= amt; return *this; }
bool operator<(const iterator &other) const { return index > other.index; }
bool operator==(const iterator &other) const { return index == other.index; }
bool operator!=(const iterator &other) const { return index != other.index; }
diff --git a/kernel/log.cc b/kernel/log.cc
index 104bee078..c7ae873bc 100644
--- a/kernel/log.cc
+++ b/kernel/log.cc
@@ -19,7 +19,7 @@
#include "kernel/yosys.h"
#include "libs/sha1/sha1.h"
-#include "backends/ilang/ilang_backend.h"
+#include "backends/rtlil/rtlil_backend.h"
#if !defined(_WIN32) || defined(__MINGW32__)
# include <sys/time.h>
@@ -319,7 +319,7 @@ void log_file_info(const std::string &filename, int lineno,
va_end(ap);
}
-YS_ATTRIBUTE(noreturn)
+[[noreturn]]
static void logv_error_with_prefix(const char *prefix,
const char *format, va_list ap)
{
@@ -600,7 +600,7 @@ void log_dump_val_worker(RTLIL::State v) {
const char *log_signal(const RTLIL::SigSpec &sig, bool autoint)
{
std::stringstream buf;
- ILANG_BACKEND::dump_sigspec(buf, sig, autoint);
+ RTLIL_BACKEND::dump_sigspec(buf, sig, autoint);
if (string_buf.size() < 100) {
string_buf.push_back(buf.str());
@@ -647,21 +647,21 @@ const char *log_id(RTLIL::IdString str)
void log_module(RTLIL::Module *module, std::string indent)
{
std::stringstream buf;
- ILANG_BACKEND::dump_module(buf, indent, module, module->design, false);
+ RTLIL_BACKEND::dump_module(buf, indent, module, module->design, false);
log("%s", buf.str().c_str());
}
void log_cell(RTLIL::Cell *cell, std::string indent)
{
std::stringstream buf;
- ILANG_BACKEND::dump_cell(buf, indent, cell);
+ RTLIL_BACKEND::dump_cell(buf, indent, cell);
log("%s", buf.str().c_str());
}
void log_wire(RTLIL::Wire *wire, std::string indent)
{
std::stringstream buf;
- ILANG_BACKEND::dump_wire(buf, indent, wire);
+ RTLIL_BACKEND::dump_wire(buf, indent, wire);
log("%s", buf.str().c_str());
}
diff --git a/kernel/log.h b/kernel/log.h
index 516744b50..8981c4cde 100644
--- a/kernel/log.h
+++ b/kernel/log.h
@@ -55,7 +55,9 @@
#else
# include <sys/time.h>
# include <sys/resource.h>
-# include <signal.h>
+# if defined(__unix__) || (defined(__APPLE__) && defined(__MACH__))
+# include <signal.h>
+# endif
#endif
#if defined(_MSC_VER)
@@ -137,7 +139,7 @@ void logv(const char *format, va_list ap);
void logv_header(RTLIL::Design *design, const char *format, va_list ap);
void logv_warning(const char *format, va_list ap);
void logv_warning_noprefix(const char *format, va_list ap);
-YS_NORETURN void logv_error(const char *format, va_list ap) YS_ATTRIBUTE(noreturn);
+[[noreturn]] void logv_error(const char *format, va_list ap);
void log(const char *format, ...) YS_ATTRIBUTE(format(printf, 1, 2));
void log_header(RTLIL::Design *design, const char *format, ...) YS_ATTRIBUTE(format(printf, 2, 3));
@@ -149,17 +151,16 @@ void log_file_warning(const std::string &filename, int lineno, const char *forma
void log_file_info(const std::string &filename, int lineno, const char *format, ...) YS_ATTRIBUTE(format(printf, 3, 4));
void log_warning_noprefix(const char *format, ...) YS_ATTRIBUTE(format(printf, 1, 2));
-YS_NORETURN void log_error(const char *format, ...) YS_ATTRIBUTE(format(printf, 1, 2), noreturn);
-void log_file_error(const string &filename, int lineno, const char *format, ...) YS_ATTRIBUTE(format(printf, 3, 4), noreturn);
-YS_NORETURN void log_cmd_error(const char *format, ...) YS_ATTRIBUTE(format(printf, 1, 2), noreturn);
+[[noreturn]] void log_error(const char *format, ...) YS_ATTRIBUTE(format(printf, 1, 2));
+[[noreturn]] void log_file_error(const string &filename, int lineno, const char *format, ...) YS_ATTRIBUTE(format(printf, 3, 4));
+[[noreturn]] void log_cmd_error(const char *format, ...) YS_ATTRIBUTE(format(printf, 1, 2));
#ifndef NDEBUG
static inline bool ys_debug(int n = 0) { if (log_force_debug) return true; log_debug_suppressed += n; return false; }
-# define log_debug(...) do { if (ys_debug(1)) log(__VA_ARGS__); } while (0)
#else
static inline bool ys_debug(int = 0) { return false; }
-# define log_debug(_fmt, ...) do { } while (0)
#endif
+# define log_debug(...) do { if (ys_debug(1)) log(__VA_ARGS__); } while (0)
static inline void log_suppressed() {
if (log_debug_suppressed && !log_make_debug) {
@@ -234,7 +235,7 @@ static inline void log_assert_worker(bool cond, const char *expr, const char *fi
}
# define log_assert(_assert_expr_) YOSYS_NAMESPACE_PREFIX log_assert_worker(_assert_expr_, #_assert_expr_, __FILE__, __LINE__)
#else
-# define log_assert(_assert_expr_)
+# define log_assert(_assert_expr_) do { if (0) { (void)(_assert_expr_); } } while(0)
#endif
#define log_abort() YOSYS_NAMESPACE_PREFIX log_error("Abort in %s:%d.\n", __FILE__, __LINE__)
@@ -306,19 +307,17 @@ struct PerformanceTimer
static int64_t query() {
# ifdef _WIN32
return 0;
-# elif defined(_POSIX_TIMERS) && (_POSIX_TIMERS > 0)
- struct timespec ts;
- clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &ts);
- return int64_t(ts.tv_sec)*1000000000 + ts.tv_nsec;
# elif defined(RUSAGE_SELF)
struct rusage rusage;
- int64_t t;
- if (getrusage(RUSAGE_SELF, &rusage) == -1) {
- log_cmd_error("getrusage failed!\n");
- log_abort();
+ int64_t t = 0;
+ for (int who : {RUSAGE_SELF, RUSAGE_CHILDREN}) {
+ if (getrusage(who, &rusage) == -1) {
+ log_cmd_error("getrusage failed!\n");
+ log_abort();
+ }
+ t += 1000000000ULL * (int64_t) rusage.ru_utime.tv_sec + (int64_t) rusage.ru_utime.tv_usec * 1000ULL;
+ t += 1000000000ULL * (int64_t) rusage.ru_stime.tv_sec + (int64_t) rusage.ru_stime.tv_usec * 1000ULL;
}
- t = 1000000000ULL * (int64_t) rusage.ru_utime.tv_sec + (int64_t) rusage.ru_utime.tv_usec * 1000ULL;
- t += 1000000000ULL * (int64_t) rusage.ru_stime.tv_sec + (int64_t) rusage.ru_stime.tv_usec * 1000ULL;
return t;
# else
# error "Don't know how to measure per-process CPU time. Need alternative method (times()/clocks()/gettimeofday()?)."
@@ -369,7 +368,7 @@ static inline void log_dump_val_worker(char *v) { log("%s", v); }
static inline void log_dump_val_worker(const char *v) { log("%s", v); }
static inline void log_dump_val_worker(std::string v) { log("%s", v.c_str()); }
static inline void log_dump_val_worker(PerformanceTimer p) { log("%f seconds", p.sec()); }
-static inline void log_dump_args_worker(const char *p YS_ATTRIBUTE(unused)) { log_assert(*p == 0); }
+static inline void log_dump_args_worker(const char *p) { log_assert(*p == 0); }
void log_dump_val_worker(RTLIL::IdString v);
void log_dump_val_worker(RTLIL::SigSpec v);
void log_dump_val_worker(RTLIL::State v);
diff --git a/kernel/macc.h b/kernel/macc.h
index e9f6f05e9..d216e6772 100644
--- a/kernel/macc.h
+++ b/kernel/macc.h
@@ -107,10 +107,8 @@ struct Macc
std::vector<RTLIL::State> config_bits = cell->getParam(ID::CONFIG).bits;
int config_cursor = 0;
-#ifndef NDEBUG
int config_width = cell->getParam(ID::CONFIG_WIDTH).as_int();
log_assert(GetSize(config_bits) >= config_width);
-#endif
int num_bits = 0;
if (config_bits[config_cursor++] == State::S1) num_bits |= 1;
diff --git a/kernel/mem.cc b/kernel/mem.cc
new file mode 100644
index 000000000..0301a913c
--- /dev/null
+++ b/kernel/mem.cc
@@ -0,0 +1,436 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2020 Marcelina Kościelnicka <mwk@0x04.net>
+ *
+ * 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/mem.h"
+
+USING_YOSYS_NAMESPACE
+
+void Mem::remove() {
+ if (cell) {
+ module->remove(cell);
+ cell = nullptr;
+ }
+ if (mem) {
+ module->memories.erase(mem->name);
+ delete mem;
+ mem = nullptr;
+ }
+ for (auto &port : rd_ports) {
+ if (port.cell) {
+ module->remove(port.cell);
+ port.cell = nullptr;
+ }
+ }
+ for (auto &port : wr_ports) {
+ if (port.cell) {
+ module->remove(port.cell);
+ port.cell = nullptr;
+ }
+ }
+ for (auto &init : inits) {
+ if (init.cell) {
+ module->remove(init.cell);
+ init.cell = nullptr;
+ }
+ }
+}
+
+void Mem::emit() {
+ if (packed) {
+ if (mem) {
+ module->memories.erase(mem->name);
+ delete mem;
+ mem = nullptr;
+ }
+ if (!cell) {
+ if (memid.empty())
+ memid = NEW_ID;
+ cell = module->addCell(memid, ID($mem));
+ }
+ cell->attributes = attributes;
+ cell->parameters[ID::MEMID] = Const(memid.str());
+ cell->parameters[ID::WIDTH] = Const(width);
+ cell->parameters[ID::OFFSET] = Const(start_offset);
+ cell->parameters[ID::SIZE] = Const(size);
+ cell->parameters[ID::RD_PORTS] = Const(GetSize(rd_ports));
+ cell->parameters[ID::WR_PORTS] = Const(GetSize(wr_ports));
+ Const rd_clk_enable, rd_clk_polarity, rd_transparent;
+ Const wr_clk_enable, wr_clk_polarity;
+ SigSpec rd_clk, rd_en, rd_addr, rd_data;
+ SigSpec wr_clk, wr_en, wr_addr, wr_data;
+ int abits = 0;
+ for (auto &port : rd_ports)
+ abits = std::max(abits, GetSize(port.addr));
+ for (auto &port : wr_ports)
+ abits = std::max(abits, GetSize(port.addr));
+ cell->parameters[ID::ABITS] = Const(abits);
+ for (auto &port : rd_ports) {
+ if (port.cell) {
+ module->remove(port.cell);
+ port.cell = nullptr;
+ }
+ rd_clk_enable.bits.push_back(State(port.clk_enable));
+ rd_clk_polarity.bits.push_back(State(port.clk_polarity));
+ rd_transparent.bits.push_back(State(port.transparent));
+ rd_clk.append(port.clk);
+ log_assert(GetSize(port.clk) == 1);
+ rd_en.append(port.en);
+ log_assert(GetSize(port.en) == 1);
+ SigSpec addr = port.addr;
+ addr.extend_u0(abits, false);
+ rd_addr.append(addr);
+ log_assert(GetSize(addr) == abits);
+ rd_data.append(port.data);
+ log_assert(GetSize(port.data) == width);
+ }
+ if (rd_ports.empty()) {
+ rd_clk_enable = State::S0;
+ rd_clk_polarity = State::S0;
+ rd_transparent = State::S0;
+ }
+ cell->parameters[ID::RD_CLK_ENABLE] = rd_clk_enable;
+ cell->parameters[ID::RD_CLK_POLARITY] = rd_clk_polarity;
+ cell->parameters[ID::RD_TRANSPARENT] = rd_transparent;
+ cell->setPort(ID::RD_CLK, rd_clk);
+ cell->setPort(ID::RD_EN, rd_en);
+ cell->setPort(ID::RD_ADDR, rd_addr);
+ cell->setPort(ID::RD_DATA, rd_data);
+ for (auto &port : wr_ports) {
+ if (port.cell) {
+ module->remove(port.cell);
+ port.cell = nullptr;
+ }
+ wr_clk_enable.bits.push_back(State(port.clk_enable));
+ wr_clk_polarity.bits.push_back(State(port.clk_polarity));
+ wr_clk.append(port.clk);
+ log_assert(GetSize(port.clk) == 1);
+ wr_en.append(port.en);
+ log_assert(GetSize(port.en) == width);
+ SigSpec addr = port.addr;
+ addr.extend_u0(abits, false);
+ wr_addr.append(addr);
+ log_assert(GetSize(addr) == abits);
+ wr_data.append(port.data);
+ log_assert(GetSize(port.data) == width);
+ }
+ if (wr_ports.empty()) {
+ wr_clk_enable = State::S0;
+ wr_clk_polarity = State::S0;
+ }
+ cell->parameters[ID::WR_CLK_ENABLE] = wr_clk_enable;
+ cell->parameters[ID::WR_CLK_POLARITY] = wr_clk_polarity;
+ cell->setPort(ID::WR_CLK, wr_clk);
+ cell->setPort(ID::WR_EN, wr_en);
+ cell->setPort(ID::WR_ADDR, wr_addr);
+ cell->setPort(ID::WR_DATA, wr_data);
+ for (auto &init : inits) {
+ if (init.cell) {
+ module->remove(init.cell);
+ init.cell = nullptr;
+ }
+ }
+ cell->parameters[ID::INIT] = get_init_data();
+ } else {
+ if (cell) {
+ module->remove(cell);
+ cell = nullptr;
+ }
+ if (!mem) {
+ if (memid.empty())
+ memid = NEW_ID;
+ mem = new RTLIL::Memory;
+ mem->name = memid;
+ module->memories[memid] = mem;
+ }
+ mem->width = width;
+ mem->start_offset = start_offset;
+ mem->size = size;
+ for (auto &port : rd_ports) {
+ if (!port.cell)
+ port.cell = module->addCell(NEW_ID, ID($memrd));
+ port.cell->parameters[ID::MEMID] = memid.str();
+ port.cell->parameters[ID::ABITS] = GetSize(port.addr);
+ port.cell->parameters[ID::WIDTH] = width;
+ port.cell->parameters[ID::CLK_ENABLE] = port.clk_enable;
+ port.cell->parameters[ID::CLK_POLARITY] = port.clk_polarity;
+ port.cell->parameters[ID::TRANSPARENT] = port.transparent;
+ port.cell->setPort(ID::CLK, port.clk);
+ port.cell->setPort(ID::EN, port.en);
+ port.cell->setPort(ID::ADDR, port.addr);
+ port.cell->setPort(ID::DATA, port.data);
+ }
+ int idx = 0;
+ for (auto &port : wr_ports) {
+ if (!port.cell)
+ port.cell = module->addCell(NEW_ID, ID($memwr));
+ port.cell->parameters[ID::MEMID] = memid.str();
+ port.cell->parameters[ID::ABITS] = GetSize(port.addr);
+ port.cell->parameters[ID::WIDTH] = width;
+ port.cell->parameters[ID::CLK_ENABLE] = port.clk_enable;
+ port.cell->parameters[ID::CLK_POLARITY] = port.clk_polarity;
+ port.cell->parameters[ID::PRIORITY] = idx++;
+ port.cell->setPort(ID::CLK, port.clk);
+ port.cell->setPort(ID::EN, port.en);
+ port.cell->setPort(ID::ADDR, port.addr);
+ port.cell->setPort(ID::DATA, port.data);
+ }
+ idx = 0;
+ for (auto &init : inits) {
+ if (!init.cell)
+ init.cell = module->addCell(NEW_ID, ID($meminit));
+ init.cell->parameters[ID::MEMID] = memid.str();
+ init.cell->parameters[ID::ABITS] = GetSize(init.addr);
+ init.cell->parameters[ID::WIDTH] = width;
+ init.cell->parameters[ID::WORDS] = GetSize(init.data) / width;
+ init.cell->parameters[ID::PRIORITY] = idx++;
+ init.cell->setPort(ID::ADDR, init.addr);
+ init.cell->setPort(ID::DATA, init.data);
+ }
+ }
+}
+
+void Mem::remove_wr_port(int idx) {
+ if (wr_ports[idx].cell) {
+ module->remove(wr_ports[idx].cell);
+ }
+ wr_ports.erase(wr_ports.begin() + idx);
+}
+
+void Mem::remove_rd_port(int idx) {
+ if (rd_ports[idx].cell) {
+ module->remove(rd_ports[idx].cell);
+ }
+ rd_ports.erase(rd_ports.begin() + idx);
+}
+
+void Mem::clear_inits() {
+ for (auto &init : inits)
+ if (init.cell)
+ module->remove(init.cell);
+ inits.clear();
+}
+
+Const Mem::get_init_data() const {
+ Const init_data(State::Sx, width * size);
+ for (auto &init : inits) {
+ int offset = (init.addr.as_int() - start_offset) * width;
+ for (int i = 0; i < GetSize(init.data); i++)
+ if (0 <= i+offset && i+offset < GetSize(init_data))
+ init_data.bits[i+offset] = init.data.bits[i];
+ }
+ return init_data;
+}
+
+namespace {
+
+ struct MemIndex {
+ dict<IdString, pool<Cell *>> rd_ports;
+ dict<IdString, pool<Cell *>> wr_ports;
+ dict<IdString, pool<Cell *>> inits;
+ MemIndex (Module *module) {
+ for (auto cell: module->cells()) {
+ if (cell->type == ID($memwr))
+ wr_ports[cell->parameters.at(ID::MEMID).decode_string()].insert(cell);
+ else if (cell->type == ID($memrd))
+ rd_ports[cell->parameters.at(ID::MEMID).decode_string()].insert(cell);
+ else if (cell->type == ID($meminit))
+ inits[cell->parameters.at(ID::MEMID).decode_string()].insert(cell);
+ }
+ }
+ };
+
+ Mem mem_from_memory(Module *module, RTLIL::Memory *mem, const MemIndex &index) {
+ Mem res(module, mem->name, mem->width, mem->start_offset, mem->size);
+ res.packed = false;
+ res.mem = mem;
+ res.attributes = mem->attributes;
+ if (index.rd_ports.count(mem->name)) {
+ for (auto cell : index.rd_ports.at(mem->name)) {
+ MemRd mrd;
+ mrd.cell = cell;
+ mrd.attributes = cell->attributes;
+ mrd.clk_enable = cell->parameters.at(ID::CLK_ENABLE).as_bool();
+ mrd.clk_polarity = cell->parameters.at(ID::CLK_POLARITY).as_bool();
+ mrd.transparent = cell->parameters.at(ID::TRANSPARENT).as_bool();
+ mrd.clk = cell->getPort(ID::CLK);
+ mrd.en = cell->getPort(ID::EN);
+ mrd.addr = cell->getPort(ID::ADDR);
+ mrd.data = cell->getPort(ID::DATA);
+ res.rd_ports.push_back(mrd);
+ }
+ }
+ if (index.wr_ports.count(mem->name)) {
+ std::vector<std::pair<int, MemWr>> ports;
+ for (auto cell : index.wr_ports.at(mem->name)) {
+ MemWr mwr;
+ mwr.cell = cell;
+ mwr.attributes = cell->attributes;
+ mwr.clk_enable = cell->parameters.at(ID::CLK_ENABLE).as_bool();
+ mwr.clk_polarity = cell->parameters.at(ID::CLK_POLARITY).as_bool();
+ mwr.clk = cell->getPort(ID::CLK);
+ mwr.en = cell->getPort(ID::EN);
+ mwr.addr = cell->getPort(ID::ADDR);
+ mwr.data = cell->getPort(ID::DATA);
+ ports.push_back(std::make_pair(cell->parameters.at(ID::PRIORITY).as_int(), mwr));
+ }
+ std::sort(ports.begin(), ports.end(), [](const std::pair<int, MemWr> &a, const std::pair<int, MemWr> &b) { return a.first < b.first; });
+ for (auto &it : ports)
+ res.wr_ports.push_back(it.second);
+ }
+ if (index.inits.count(mem->name)) {
+ std::vector<std::pair<int, MemInit>> inits;
+ for (auto cell : index.inits.at(mem->name)) {
+ MemInit init;
+ init.cell = cell;
+ init.attributes = cell->attributes;
+ auto addr = cell->getPort(ID::ADDR);
+ auto data = cell->getPort(ID::DATA);
+ if (!addr.is_fully_const())
+ log_error("Non-constant address %s in memory initialization %s.\n", log_signal(addr), log_id(cell));
+ if (!data.is_fully_const())
+ log_error("Non-constant data %s in memory initialization %s.\n", log_signal(data), log_id(cell));
+ init.addr = addr.as_const();
+ init.data = data.as_const();
+ inits.push_back(std::make_pair(cell->parameters.at(ID::PRIORITY).as_int(), init));
+ }
+ std::sort(inits.begin(), inits.end(), [](const std::pair<int, MemInit> &a, const std::pair<int, MemInit> &b) { return a.first < b.first; });
+ for (auto &it : inits)
+ res.inits.push_back(it.second);
+ }
+ return res;
+ }
+
+ Mem mem_from_cell(Cell *cell) {
+ Mem res(cell->module, cell->parameters.at(ID::MEMID).decode_string(),
+ cell->parameters.at(ID::WIDTH).as_int(),
+ cell->parameters.at(ID::OFFSET).as_int(),
+ cell->parameters.at(ID::SIZE).as_int()
+ );
+ int abits = cell->parameters.at(ID::ABITS).as_int();
+ res.packed = true;
+ res.cell = cell;
+ res.attributes = cell->attributes;
+ Const &init = cell->parameters.at(ID::INIT);
+ if (!init.is_fully_undef()) {
+ int pos = 0;
+ while (pos < res.size) {
+ Const word = init.extract(pos * res.width, res.width, State::Sx);
+ if (word.is_fully_undef()) {
+ pos++;
+ } else {
+ int epos;
+ for (epos = pos; epos < res.size; epos++) {
+ Const eword = init.extract(epos * res.width, res.width, State::Sx);
+ if (eword.is_fully_undef())
+ break;
+ }
+ MemInit minit;
+ minit.addr = res.start_offset + pos;
+ minit.data = init.extract(pos * res.width, (epos - pos) * res.width, State::Sx);
+ res.inits.push_back(minit);
+ pos = epos;
+ }
+ }
+ }
+ for (int i = 0; i < cell->parameters.at(ID::RD_PORTS).as_int(); i++) {
+ MemRd mrd;
+ mrd.clk_enable = cell->parameters.at(ID::RD_CLK_ENABLE).extract(i, 1).as_bool();
+ mrd.clk_polarity = cell->parameters.at(ID::RD_CLK_POLARITY).extract(i, 1).as_bool();
+ mrd.transparent = cell->parameters.at(ID::RD_TRANSPARENT).extract(i, 1).as_bool();
+ mrd.clk = cell->getPort(ID::RD_CLK).extract(i, 1);
+ mrd.en = cell->getPort(ID::RD_EN).extract(i, 1);
+ mrd.addr = cell->getPort(ID::RD_ADDR).extract(i * abits, abits);
+ mrd.data = cell->getPort(ID::RD_DATA).extract(i * res.width, res.width);
+ res.rd_ports.push_back(mrd);
+ }
+ for (int i = 0; i < cell->parameters.at(ID::WR_PORTS).as_int(); i++) {
+ MemWr mwr;
+ mwr.clk_enable = cell->parameters.at(ID::WR_CLK_ENABLE).extract(i, 1).as_bool();
+ mwr.clk_polarity = cell->parameters.at(ID::WR_CLK_POLARITY).extract(i, 1).as_bool();
+ mwr.clk = cell->getPort(ID::WR_CLK).extract(i, 1);
+ mwr.en = cell->getPort(ID::WR_EN).extract(i * res.width, res.width);
+ mwr.addr = cell->getPort(ID::WR_ADDR).extract(i * abits, abits);
+ mwr.data = cell->getPort(ID::WR_DATA).extract(i * res.width, res.width);
+ res.wr_ports.push_back(mwr);
+ }
+ return res;
+ }
+
+}
+
+std::vector<Mem> Mem::get_all_memories(Module *module) {
+ std::vector<Mem> res;
+ MemIndex index(module);
+ for (auto it: module->memories) {
+ res.push_back(mem_from_memory(module, it.second, index));
+ }
+ for (auto cell: module->cells()) {
+ if (cell->type == ID($mem))
+ res.push_back(mem_from_cell(cell));
+ }
+ return res;
+}
+
+std::vector<Mem> Mem::get_selected_memories(Module *module) {
+ std::vector<Mem> res;
+ MemIndex index(module);
+ for (auto it: module->memories) {
+ if (module->design->selected(module, it.second))
+ res.push_back(mem_from_memory(module, it.second, index));
+ }
+ for (auto cell: module->selected_cells()) {
+ if (cell->type == ID($mem))
+ res.push_back(mem_from_cell(cell));
+ }
+ return res;
+}
+
+Cell *Mem::extract_rdff(int idx) {
+ MemRd &port = rd_ports[idx];
+
+ if (!port.clk_enable)
+ return nullptr;
+
+ Cell *c;
+
+ if (port.transparent)
+ {
+ SigSpec sig_q = module->addWire(stringf("%s$rdreg[%d]$q", memid.c_str(), idx), GetSize(port.addr));
+ SigSpec sig_d = port.addr;
+ port.addr = sig_q;
+ c = module->addDffe(stringf("%s$rdreg[%d]", memid.c_str(), idx), port.clk, port.en, sig_d, sig_q, port.clk_polarity, true);
+ }
+ else
+ {
+ SigSpec sig_d = module->addWire(stringf("%s$rdreg[%d]$d", memid.c_str(), idx), width);
+ SigSpec sig_q = port.data;
+ port.data = sig_d;
+ c = module->addDffe(stringf("%s$rdreg[%d]", memid.c_str(), idx), port.clk, port.en, sig_d, sig_q, port.clk_polarity, true);
+ }
+
+ log("Extracted %s FF from read port %d of %s.%s: %s\n", port.transparent ? "addr" : "data",
+ idx, log_id(module), log_id(memid), log_id(c));
+
+ port.en = State::S1;
+ port.clk = State::S0;
+ port.clk_enable = false;
+ port.clk_polarity = true;
+
+ return c;
+}
diff --git a/kernel/mem.h b/kernel/mem.h
new file mode 100644
index 000000000..6d727e71d
--- /dev/null
+++ b/kernel/mem.h
@@ -0,0 +1,78 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2020 Marcelina Kościelnicka <mwk@0x04.net>
+ *
+ * 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.
+ *
+ */
+
+#ifndef MEM_H
+#define MEM_H
+
+#include "kernel/yosys.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+struct MemRd {
+ dict<IdString, Const> attributes;
+ Cell *cell;
+ bool clk_enable, clk_polarity;
+ bool transparent;
+ SigSpec clk, en, addr, data;
+ MemRd() : cell(nullptr) {}
+};
+
+struct MemWr {
+ dict<IdString, Const> attributes;
+ Cell *cell;
+ bool clk_enable, clk_polarity;
+ SigSpec clk, en, addr, data;
+ MemWr() : cell(nullptr) {}
+};
+
+struct MemInit {
+ dict<IdString, Const> attributes;
+ Cell *cell;
+ Const addr;
+ Const data;
+ MemInit() : cell(nullptr) {}
+};
+
+struct Mem {
+ Module *module;
+ IdString memid;
+ dict<IdString, Const> attributes;
+ bool packed;
+ RTLIL::Memory *mem;
+ Cell *cell;
+ int width, start_offset, size;
+ std::vector<MemInit> inits;
+ std::vector<MemRd> rd_ports;
+ std::vector<MemWr> wr_ports;
+
+ void remove();
+ void emit();
+ void remove_wr_port(int idx);
+ void remove_rd_port(int idx);
+ void clear_inits();
+ Const get_init_data() const;
+ static std::vector<Mem> get_all_memories(Module *module);
+ static std::vector<Mem> get_selected_memories(Module *module);
+ Cell *extract_rdff(int idx);
+ Mem(Module *module, IdString memid, int width, int start_offset, int size) : module(module), memid(memid), packed(false), mem(nullptr), cell(nullptr), width(width), start_offset(start_offset), size(size) {}
+};
+
+YOSYS_NAMESPACE_END
+
+#endif
diff --git a/kernel/modtools.h b/kernel/modtools.h
index fbc5482ee..29c510059 100644
--- a/kernel/modtools.h
+++ b/kernel/modtools.h
@@ -158,7 +158,7 @@ struct ModIndex : public RTLIL::Monitor
#endif
}
- void notify_connect(RTLIL::Cell *cell, const RTLIL::IdString &port, const RTLIL::SigSpec &old_sig, const RTLIL::SigSpec &sig) YS_OVERRIDE
+ void notify_connect(RTLIL::Cell *cell, const RTLIL::IdString &port, const RTLIL::SigSpec &old_sig, const RTLIL::SigSpec &sig) override
{
log_assert(module == cell->module);
@@ -169,7 +169,7 @@ struct ModIndex : public RTLIL::Monitor
port_add(cell, port, sig);
}
- void notify_connect(RTLIL::Module *mod YS_ATTRIBUTE(unused), const RTLIL::SigSig &sigsig) YS_OVERRIDE
+ void notify_connect(RTLIL::Module *mod, const RTLIL::SigSig &sigsig) override
{
log_assert(module == mod);
@@ -214,13 +214,13 @@ struct ModIndex : public RTLIL::Monitor
}
}
- void notify_connect(RTLIL::Module *mod YS_ATTRIBUTE(unused), const std::vector<RTLIL::SigSig>&) YS_OVERRIDE
+ void notify_connect(RTLIL::Module *mod, const std::vector<RTLIL::SigSig>&) override
{
log_assert(module == mod);
auto_reload_module = true;
}
- void notify_blackout(RTLIL::Module *mod YS_ATTRIBUTE(unused)) YS_OVERRIDE
+ void notify_blackout(RTLIL::Module *mod) override
{
log_assert(module == mod);
auto_reload_module = true;
diff --git a/kernel/register.cc b/kernel/register.cc
index 02974e534..34735a608 100644
--- a/kernel/register.cc
+++ b/kernel/register.cc
@@ -753,7 +753,7 @@ static struct CellHelpMessages {
struct HelpPass : public Pass {
HelpPass() : Pass("help", "display help messages") { }
- void help() YS_OVERRIDE
+ void help() override
{
log("\n");
log(" help ................ list all commands\n");
@@ -822,7 +822,7 @@ struct HelpPass : public Pass {
fclose(f);
}
- void execute(std::vector<std::string> args, RTLIL::Design*) YS_OVERRIDE
+ void execute(std::vector<std::string> args, RTLIL::Design*) override
{
if (args.size() == 1) {
log("\n");
@@ -926,7 +926,7 @@ struct HelpPass : public Pass {
struct EchoPass : public Pass {
EchoPass() : Pass("echo", "turning echoing back of commands on and off") { }
- void help() YS_OVERRIDE
+ void help() override
{
log("\n");
log(" echo on\n");
@@ -939,7 +939,7 @@ struct EchoPass : public Pass {
log("Do not print all commands to log before executing them. (default)\n");
log("\n");
}
- void execute(std::vector<std::string> args, RTLIL::Design*) YS_OVERRIDE
+ void execute(std::vector<std::string> args, RTLIL::Design*) override
{
if (args.size() > 2)
cmd_error(args, 2, "Unexpected argument.");
@@ -964,7 +964,7 @@ struct MinisatSatSolver : public SatSolver {
MinisatSatSolver() : SatSolver("minisat") {
yosys_satsolver = this;
}
- ezSAT *create() YS_OVERRIDE {
+ ezSAT *create() override {
return new ezMiniSAT();
}
} MinisatSatSolver;
diff --git a/kernel/register.h b/kernel/register.h
index 7bbcd1727..5cd849082 100644
--- a/kernel/register.h
+++ b/kernel/register.h
@@ -97,9 +97,9 @@ struct Frontend : Pass
std::string frontend_name;
Frontend(std::string name, std::string short_help = "** document me **");
- void run_register() YS_OVERRIDE;
- ~Frontend() YS_OVERRIDE;
- void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE YS_FINAL;
+ void run_register() override;
+ ~Frontend() override;
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override final;
virtual void execute(std::istream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) = 0;
static std::vector<std::string> next_args;
@@ -113,9 +113,9 @@ struct Backend : Pass
{
std::string backend_name;
Backend(std::string name, std::string short_help = "** document me **");
- void run_register() YS_OVERRIDE;
- ~Backend() YS_OVERRIDE;
- void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE YS_FINAL;
+ void run_register() override;
+ ~Backend() override;
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override final;
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) = 0;
void extra_args(std::ostream *&f, std::string &filename, std::vector<std::string> args, size_t argidx, bool bin_output = false);
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index ef81cac01..a9f585616 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -22,7 +22,7 @@
#include "kernel/celltypes.h"
#include "frontends/verilog/verilog_frontend.h"
#include "frontends/verilog/preproc.h"
-#include "backends/ilang/ilang_backend.h"
+#include "backends/rtlil/rtlil_backend.h"
#include <string.h>
#include <algorithm>
@@ -54,8 +54,14 @@ const pool<IdString> &RTLIL::builtin_ff_cell_types() {
ID($dff),
ID($dffe),
ID($dffsr),
+ ID($dffsre),
ID($adff),
+ ID($adffe),
+ ID($sdff),
+ ID($sdffe),
+ ID($sdffce),
ID($dlatch),
+ ID($adlatch),
ID($dlatchsr),
ID($_DFFE_NN_),
ID($_DFFE_NP_),
@@ -69,16 +75,102 @@ const pool<IdString> &RTLIL::builtin_ff_cell_types() {
ID($_DFFSR_PNP_),
ID($_DFFSR_PPN_),
ID($_DFFSR_PPP_),
+ ID($_DFFSRE_NNNN_),
+ ID($_DFFSRE_NNNP_),
+ ID($_DFFSRE_NNPN_),
+ ID($_DFFSRE_NNPP_),
+ ID($_DFFSRE_NPNN_),
+ ID($_DFFSRE_NPNP_),
+ ID($_DFFSRE_NPPN_),
+ ID($_DFFSRE_NPPP_),
+ ID($_DFFSRE_PNNN_),
+ ID($_DFFSRE_PNNP_),
+ ID($_DFFSRE_PNPN_),
+ ID($_DFFSRE_PNPP_),
+ ID($_DFFSRE_PPNN_),
+ ID($_DFFSRE_PPNP_),
+ ID($_DFFSRE_PPPN_),
+ ID($_DFFSRE_PPPP_),
+ ID($_DFF_N_),
+ ID($_DFF_P_),
ID($_DFF_NN0_),
ID($_DFF_NN1_),
ID($_DFF_NP0_),
ID($_DFF_NP1_),
- ID($_DFF_N_),
ID($_DFF_PN0_),
ID($_DFF_PN1_),
ID($_DFF_PP0_),
ID($_DFF_PP1_),
- ID($_DFF_P_),
+ ID($_DFFE_NN0N_),
+ ID($_DFFE_NN0P_),
+ ID($_DFFE_NN1N_),
+ ID($_DFFE_NN1P_),
+ ID($_DFFE_NP0N_),
+ ID($_DFFE_NP0P_),
+ ID($_DFFE_NP1N_),
+ ID($_DFFE_NP1P_),
+ ID($_DFFE_PN0N_),
+ ID($_DFFE_PN0P_),
+ ID($_DFFE_PN1N_),
+ ID($_DFFE_PN1P_),
+ ID($_DFFE_PP0N_),
+ ID($_DFFE_PP0P_),
+ ID($_DFFE_PP1N_),
+ ID($_DFFE_PP1P_),
+ ID($_SDFF_NN0_),
+ ID($_SDFF_NN1_),
+ ID($_SDFF_NP0_),
+ ID($_SDFF_NP1_),
+ ID($_SDFF_PN0_),
+ ID($_SDFF_PN1_),
+ ID($_SDFF_PP0_),
+ ID($_SDFF_PP1_),
+ ID($_SDFFE_NN0N_),
+ ID($_SDFFE_NN0P_),
+ ID($_SDFFE_NN1N_),
+ ID($_SDFFE_NN1P_),
+ ID($_SDFFE_NP0N_),
+ ID($_SDFFE_NP0P_),
+ ID($_SDFFE_NP1N_),
+ ID($_SDFFE_NP1P_),
+ ID($_SDFFE_PN0N_),
+ ID($_SDFFE_PN0P_),
+ ID($_SDFFE_PN1N_),
+ ID($_SDFFE_PN1P_),
+ ID($_SDFFE_PP0N_),
+ ID($_SDFFE_PP0P_),
+ ID($_SDFFE_PP1N_),
+ ID($_SDFFE_PP1P_),
+ ID($_SDFFCE_NN0N_),
+ ID($_SDFFCE_NN0P_),
+ ID($_SDFFCE_NN1N_),
+ ID($_SDFFCE_NN1P_),
+ ID($_SDFFCE_NP0N_),
+ ID($_SDFFCE_NP0P_),
+ ID($_SDFFCE_NP1N_),
+ ID($_SDFFCE_NP1P_),
+ ID($_SDFFCE_PN0N_),
+ ID($_SDFFCE_PN0P_),
+ ID($_SDFFCE_PN1N_),
+ ID($_SDFFCE_PN1P_),
+ ID($_SDFFCE_PP0N_),
+ ID($_SDFFCE_PP0P_),
+ ID($_SDFFCE_PP1N_),
+ ID($_SDFFCE_PP1P_),
+ ID($_SR_NN_),
+ ID($_SR_NP_),
+ ID($_SR_PN_),
+ ID($_SR_PP_),
+ ID($_DLATCH_N_),
+ ID($_DLATCH_P_),
+ ID($_DLATCH_NN0_),
+ ID($_DLATCH_NN1_),
+ ID($_DLATCH_NP0_),
+ ID($_DLATCH_NP1_),
+ ID($_DLATCH_PN0_),
+ ID($_DLATCH_PN1_),
+ ID($_DLATCH_PP0_),
+ ID($_DLATCH_PP1_),
ID($_DLATCHSR_NNN_),
ID($_DLATCHSR_NNP_),
ID($_DLATCHSR_NPN_),
@@ -87,8 +179,6 @@ const pool<IdString> &RTLIL::builtin_ff_cell_types() {
ID($_DLATCHSR_PNP_),
ID($_DLATCHSR_PPN_),
ID($_DLATCHSR_PPP_),
- ID($_DLATCH_N_),
- ID($_DLATCH_P_),
ID($_FF_),
};
return res;
@@ -833,7 +923,7 @@ namespace {
void error(int linenr)
{
std::stringstream buf;
- ILANG_BACKEND::dump_cell(buf, " ", cell);
+ RTLIL_BACKEND::dump_cell(buf, " ", cell);
log_error("Found error in internal cell %s%s%s (%s) at %s:%d:\n%s",
module ? module->name.c_str() : "", module ? "." : "",
@@ -945,7 +1035,11 @@ namespace {
}
if (cell->type.in(ID($shift), ID($shiftx))) {
- param_bool(ID::A_SIGNED);
+ if (cell->type == ID($shiftx)) {
+ param_bool(ID::A_SIGNED, /*expected=*/false);
+ } else {
+ param_bool(ID::A_SIGNED);
+ }
param_bool(ID::B_SIGNED);
port(ID::A, param(ID::A_WIDTH));
port(ID::B, param(ID::B_WIDTH));
@@ -1139,6 +1233,21 @@ namespace {
return;
}
+ if (cell->type == ID($dffsre)) {
+ param_bool(ID::CLK_POLARITY);
+ param_bool(ID::SET_POLARITY);
+ param_bool(ID::CLR_POLARITY);
+ param_bool(ID::EN_POLARITY);
+ port(ID::CLK, 1);
+ port(ID::EN, 1);
+ port(ID::SET, param(ID::WIDTH));
+ port(ID::CLR, param(ID::WIDTH));
+ port(ID::D, param(ID::WIDTH));
+ port(ID::Q, param(ID::WIDTH));
+ check_expected();
+ return;
+ }
+
if (cell->type == ID($adff)) {
param_bool(ID::CLK_POLARITY);
param_bool(ID::ARST_POLARITY);
@@ -1151,6 +1260,46 @@ namespace {
return;
}
+ if (cell->type == ID($sdff)) {
+ param_bool(ID::CLK_POLARITY);
+ param_bool(ID::SRST_POLARITY);
+ param_bits(ID::SRST_VALUE, param(ID::WIDTH));
+ port(ID::CLK, 1);
+ port(ID::SRST, 1);
+ port(ID::D, param(ID::WIDTH));
+ port(ID::Q, param(ID::WIDTH));
+ check_expected();
+ return;
+ }
+
+ if (cell->type.in(ID($sdffe), ID($sdffce))) {
+ param_bool(ID::CLK_POLARITY);
+ param_bool(ID::EN_POLARITY);
+ param_bool(ID::SRST_POLARITY);
+ param_bits(ID::SRST_VALUE, param(ID::WIDTH));
+ port(ID::CLK, 1);
+ port(ID::EN, 1);
+ port(ID::SRST, 1);
+ port(ID::D, param(ID::WIDTH));
+ port(ID::Q, param(ID::WIDTH));
+ check_expected();
+ return;
+ }
+
+ if (cell->type == ID($adffe)) {
+ param_bool(ID::CLK_POLARITY);
+ param_bool(ID::EN_POLARITY);
+ param_bool(ID::ARST_POLARITY);
+ param_bits(ID::ARST_VALUE, param(ID::WIDTH));
+ port(ID::CLK, 1);
+ port(ID::EN, 1);
+ port(ID::ARST, 1);
+ port(ID::D, param(ID::WIDTH));
+ port(ID::Q, param(ID::WIDTH));
+ check_expected();
+ return;
+ }
+
if (cell->type == ID($dlatch)) {
param_bool(ID::EN_POLARITY);
port(ID::EN, 1);
@@ -1160,6 +1309,18 @@ namespace {
return;
}
+ if (cell->type == ID($adlatch)) {
+ param_bool(ID::EN_POLARITY);
+ param_bool(ID::ARST_POLARITY);
+ param_bits(ID::ARST_VALUE, param(ID::WIDTH));
+ port(ID::EN, 1);
+ port(ID::ARST, 1);
+ port(ID::D, param(ID::WIDTH));
+ port(ID::Q, param(ID::WIDTH));
+ check_expected();
+ return;
+ }
+
if (cell->type == ID($dlatchsr)) {
param_bool(ID::EN_POLARITY);
param_bool(ID::SET_POLARITY);
@@ -1351,49 +1512,69 @@ namespace {
if (cell->type == ID($_MUX8_)) { port(ID::A,1); port(ID::B,1); port(ID::C,1); port(ID::D,1); port(ID::E,1); port(ID::F,1); port(ID::G,1); port(ID::H,1); port(ID::S,1); port(ID::T,1); port(ID::U,1); port(ID::Y,1); check_expected(); return; }
if (cell->type == ID($_MUX16_)) { port(ID::A,1); port(ID::B,1); port(ID::C,1); port(ID::D,1); port(ID::E,1); port(ID::F,1); port(ID::G,1); port(ID::H,1); port(ID::I,1); port(ID::J,1); port(ID::K,1); port(ID::L,1); port(ID::M,1); port(ID::N,1); port(ID::O,1); port(ID::P,1); port(ID::S,1); port(ID::T,1); port(ID::U,1); port(ID::V,1); port(ID::Y,1); check_expected(); return; }
- if (cell->type == ID($_SR_NN_)) { port(ID::S,1); port(ID::R,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_SR_NP_)) { port(ID::S,1); port(ID::R,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_SR_PN_)) { port(ID::S,1); port(ID::R,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_SR_PP_)) { port(ID::S,1); port(ID::R,1); port(ID::Q,1); check_expected(); return; }
-
- if (cell->type == ID($_FF_)) { port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFF_N_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); check_expected(); return; }
- if (cell->type == ID($_DFF_P_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); check_expected(); return; }
-
- if (cell->type == ID($_DFFE_NN_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::E,1); check_expected(); return; }
- if (cell->type == ID($_DFFE_NP_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::E,1); check_expected(); return; }
- if (cell->type == ID($_DFFE_PN_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::E,1); check_expected(); return; }
- if (cell->type == ID($_DFFE_PP_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::E,1); check_expected(); return; }
-
- if (cell->type == ID($_DFF_NN0_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
- if (cell->type == ID($_DFF_NN1_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
- if (cell->type == ID($_DFF_NP0_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
- if (cell->type == ID($_DFF_NP1_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
- if (cell->type == ID($_DFF_PN0_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
- if (cell->type == ID($_DFF_PN1_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
- if (cell->type == ID($_DFF_PP0_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
- if (cell->type == ID($_DFF_PP1_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
-
- if (cell->type == ID($_DFFSR_NNN_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFFSR_NNP_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFFSR_NPN_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFFSR_NPP_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFFSR_PNN_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFFSR_PNP_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFFSR_PPN_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFFSR_PPP_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
-
- if (cell->type == ID($_DLATCH_N_)) { port(ID::E,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCH_P_)) { port(ID::E,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
-
- if (cell->type == ID($_DLATCHSR_NNN_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCHSR_NNP_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCHSR_NPN_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCHSR_NPP_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCHSR_PNN_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCHSR_PNP_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCHSR_PPN_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCHSR_PPP_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
+ if (cell->type.in(ID($_SR_NN_), ID($_SR_NP_), ID($_SR_PN_), ID($_SR_PP_)))
+ { port(ID::S,1); port(ID::R,1); port(ID::Q,1); check_expected(); return; }
+
+ if (cell->type == ID($_FF_)) { port(ID::D,1); port(ID::Q,1); check_expected(); return; }
+
+ if (cell->type.in(ID($_DFF_N_), ID($_DFF_P_)))
+ { port(ID::D,1); port(ID::Q,1); port(ID::C,1); check_expected(); return; }
+
+ if (cell->type.in(ID($_DFFE_NN_), ID($_DFFE_NP_), ID($_DFFE_PN_), ID($_DFFE_PP_)))
+ { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::E,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_),
+ ID($_DFF_PN0_), ID($_DFF_PN1_), ID($_DFF_PP0_), ID($_DFF_PP1_)))
+ { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_DFFE_NN0N_), ID($_DFFE_NN0P_), ID($_DFFE_NN1N_), ID($_DFFE_NN1P_),
+ ID($_DFFE_NP0N_), ID($_DFFE_NP0P_), ID($_DFFE_NP1N_), ID($_DFFE_NP1P_),
+ ID($_DFFE_PN0N_), ID($_DFFE_PN0P_), ID($_DFFE_PN1N_), ID($_DFFE_PN1P_),
+ ID($_DFFE_PP0N_), ID($_DFFE_PP0P_), ID($_DFFE_PP1N_), ID($_DFFE_PP1P_)))
+ { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); port(ID::E,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_),
+ ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_)))
+ { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_DFFSRE_NNNN_), ID($_DFFSRE_NNNP_), ID($_DFFSRE_NNPN_), ID($_DFFSRE_NNPP_),
+ ID($_DFFSRE_NPNN_), ID($_DFFSRE_NPNP_), ID($_DFFSRE_NPPN_), ID($_DFFSRE_NPPP_),
+ ID($_DFFSRE_PNNN_), ID($_DFFSRE_PNNP_), ID($_DFFSRE_PNPN_), ID($_DFFSRE_PNPP_),
+ ID($_DFFSRE_PPNN_), ID($_DFFSRE_PPNP_), ID($_DFFSRE_PPPN_), ID($_DFFSRE_PPPP_)))
+ { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::E,1); port(ID::Q,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_SDFF_NN0_), ID($_SDFF_NN1_), ID($_SDFF_NP0_), ID($_SDFF_NP1_),
+ ID($_SDFF_PN0_), ID($_SDFF_PN1_), ID($_SDFF_PP0_), ID($_SDFF_PP1_)))
+ { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_SDFFE_NN0N_), ID($_SDFFE_NN0P_), ID($_SDFFE_NN1N_), ID($_SDFFE_NN1P_),
+ ID($_SDFFE_NP0N_), ID($_SDFFE_NP0P_), ID($_SDFFE_NP1N_), ID($_SDFFE_NP1P_),
+ ID($_SDFFE_PN0N_), ID($_SDFFE_PN0P_), ID($_SDFFE_PN1N_), ID($_SDFFE_PN1P_),
+ ID($_SDFFE_PP0N_), ID($_SDFFE_PP0P_), ID($_SDFFE_PP1N_), ID($_SDFFE_PP1P_),
+ ID($_SDFFCE_NN0N_), ID($_SDFFCE_NN0P_), ID($_SDFFCE_NN1N_), ID($_SDFFCE_NN1P_),
+ ID($_SDFFCE_NP0N_), ID($_SDFFCE_NP0P_), ID($_SDFFCE_NP1N_), ID($_SDFFCE_NP1P_),
+ ID($_SDFFCE_PN0N_), ID($_SDFFCE_PN0P_), ID($_SDFFCE_PN1N_), ID($_SDFFCE_PN1P_),
+ ID($_SDFFCE_PP0N_), ID($_SDFFCE_PP0P_), ID($_SDFFCE_PP1N_), ID($_SDFFCE_PP1P_)))
+ { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); port(ID::E,1); check_expected(); return; }
+
+ if (cell->type.in(ID($_DLATCH_N_), ID($_DLATCH_P_)))
+ { port(ID::E,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_DLATCH_NN0_), ID($_DLATCH_NN1_), ID($_DLATCH_NP0_), ID($_DLATCH_NP1_),
+ ID($_DLATCH_PN0_), ID($_DLATCH_PN1_), ID($_DLATCH_PP0_), ID($_DLATCH_PP1_)))
+ { port(ID::E,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_DLATCHSR_NNN_), ID($_DLATCHSR_NNP_), ID($_DLATCHSR_NPN_), ID($_DLATCHSR_NPP_),
+ ID($_DLATCHSR_PNN_), ID($_DLATCHSR_PNP_), ID($_DLATCHSR_PPN_), ID($_DLATCHSR_PPP_)))
+ { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
error(__LINE__);
}
@@ -2299,6 +2480,25 @@ RTLIL::Cell* RTLIL::Module::addDffsr(RTLIL::IdString name, const RTLIL::SigSpec
return cell;
}
+RTLIL::Cell* RTLIL::Module::addDffsre(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
+ RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity, bool en_polarity, bool set_polarity, bool clr_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, ID($dffsre));
+ cell->parameters[ID::CLK_POLARITY] = clk_polarity;
+ cell->parameters[ID::EN_POLARITY] = en_polarity;
+ cell->parameters[ID::SET_POLARITY] = set_polarity;
+ cell->parameters[ID::CLR_POLARITY] = clr_polarity;
+ cell->parameters[ID::WIDTH] = sig_q.size();
+ cell->setPort(ID::CLK, sig_clk);
+ cell->setPort(ID::EN, sig_en);
+ cell->setPort(ID::SET, sig_set);
+ cell->setPort(ID::CLR, sig_clr);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addAdff(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
RTLIL::Const arst_value, bool clk_polarity, bool arst_polarity, const std::string &src)
{
@@ -2315,6 +2515,76 @@ RTLIL::Cell* RTLIL::Module::addAdff(RTLIL::IdString name, const RTLIL::SigSpec &
return cell;
}
+RTLIL::Cell* RTLIL::Module::addAdffe(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ RTLIL::Const arst_value, bool clk_polarity, bool en_polarity, bool arst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, ID($adffe));
+ cell->parameters[ID::CLK_POLARITY] = clk_polarity;
+ cell->parameters[ID::EN_POLARITY] = en_polarity;
+ cell->parameters[ID::ARST_POLARITY] = arst_polarity;
+ cell->parameters[ID::ARST_VALUE] = arst_value;
+ cell->parameters[ID::WIDTH] = sig_q.size();
+ cell->setPort(ID::CLK, sig_clk);
+ cell->setPort(ID::EN, sig_en);
+ cell->setPort(ID::ARST, sig_arst);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
+RTLIL::Cell* RTLIL::Module::addSdff(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ RTLIL::Const srst_value, bool clk_polarity, bool srst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, ID($sdff));
+ cell->parameters[ID::CLK_POLARITY] = clk_polarity;
+ cell->parameters[ID::SRST_POLARITY] = srst_polarity;
+ cell->parameters[ID::SRST_VALUE] = srst_value;
+ cell->parameters[ID::WIDTH] = sig_q.size();
+ cell->setPort(ID::CLK, sig_clk);
+ cell->setPort(ID::SRST, sig_srst);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
+RTLIL::Cell* RTLIL::Module::addSdffe(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ RTLIL::Const srst_value, bool clk_polarity, bool en_polarity, bool srst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, ID($sdffe));
+ cell->parameters[ID::CLK_POLARITY] = clk_polarity;
+ cell->parameters[ID::EN_POLARITY] = en_polarity;
+ cell->parameters[ID::SRST_POLARITY] = srst_polarity;
+ cell->parameters[ID::SRST_VALUE] = srst_value;
+ cell->parameters[ID::WIDTH] = sig_q.size();
+ cell->setPort(ID::CLK, sig_clk);
+ cell->setPort(ID::EN, sig_en);
+ cell->setPort(ID::SRST, sig_srst);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
+RTLIL::Cell* RTLIL::Module::addSdffce(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ RTLIL::Const srst_value, bool clk_polarity, bool en_polarity, bool srst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, ID($sdffce));
+ cell->parameters[ID::CLK_POLARITY] = clk_polarity;
+ cell->parameters[ID::EN_POLARITY] = en_polarity;
+ cell->parameters[ID::SRST_POLARITY] = srst_polarity;
+ cell->parameters[ID::SRST_VALUE] = srst_value;
+ cell->parameters[ID::WIDTH] = sig_q.size();
+ cell->setPort(ID::CLK, sig_clk);
+ cell->setPort(ID::EN, sig_en);
+ cell->setPort(ID::SRST, sig_srst);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addDlatch(RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity, const std::string &src)
{
RTLIL::Cell *cell = addCell(name, ID($dlatch));
@@ -2327,6 +2597,22 @@ RTLIL::Cell* RTLIL::Module::addDlatch(RTLIL::IdString name, const RTLIL::SigSpec
return cell;
}
+RTLIL::Cell* RTLIL::Module::addAdlatch(RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ RTLIL::Const arst_value, bool en_polarity, bool arst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, ID($adlatch));
+ cell->parameters[ID::EN_POLARITY] = en_polarity;
+ cell->parameters[ID::ARST_POLARITY] = arst_polarity;
+ cell->parameters[ID::ARST_VALUE] = arst_value;
+ cell->parameters[ID::WIDTH] = sig_q.size();
+ cell->setPort(ID::EN, sig_en);
+ cell->setPort(ID::ARST, sig_arst);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addDlatchsr(RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity, bool set_polarity, bool clr_polarity, const std::string &src)
{
@@ -2344,6 +2630,17 @@ RTLIL::Cell* RTLIL::Module::addDlatchsr(RTLIL::IdString name, const RTLIL::SigSp
return cell;
}
+RTLIL::Cell* RTLIL::Module::addSrGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
+ const RTLIL::SigSpec &sig_q, bool set_polarity, bool clr_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, stringf("$_SR_%c%c_", set_polarity ? 'P' : 'N', clr_polarity ? 'P' : 'N'));
+ cell->setPort(ID::S, sig_set);
+ cell->setPort(ID::R, sig_clr);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addFfGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, const std::string &src)
{
RTLIL::Cell *cell = addCell(name, ID($_FF_));
@@ -2387,6 +2684,20 @@ RTLIL::Cell* RTLIL::Module::addDffsrGate(RTLIL::IdString name, const RTLIL::SigS
return cell;
}
+RTLIL::Cell* RTLIL::Module::addDffsreGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
+ RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity, bool en_polarity, bool set_polarity, bool clr_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, stringf("$_DFFSRE_%c%c%c%c_", clk_polarity ? 'P' : 'N', set_polarity ? 'P' : 'N', clr_polarity ? 'P' : 'N', en_polarity ? 'P' : 'N'));
+ cell->setPort(ID::C, sig_clk);
+ cell->setPort(ID::S, sig_set);
+ cell->setPort(ID::R, sig_clr);
+ cell->setPort(ID::E, sig_en);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addAdffGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
bool arst_value, bool clk_polarity, bool arst_polarity, const std::string &src)
{
@@ -2399,6 +2710,57 @@ RTLIL::Cell* RTLIL::Module::addAdffGate(RTLIL::IdString name, const RTLIL::SigSp
return cell;
}
+RTLIL::Cell* RTLIL::Module::addAdffeGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool arst_value, bool clk_polarity, bool en_polarity, bool arst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, stringf("$_DFFE_%c%c%c%c_", clk_polarity ? 'P' : 'N', arst_polarity ? 'P' : 'N', arst_value ? '1' : '0', en_polarity ? 'P' : 'N'));
+ cell->setPort(ID::C, sig_clk);
+ cell->setPort(ID::R, sig_arst);
+ cell->setPort(ID::E, sig_en);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
+RTLIL::Cell* RTLIL::Module::addSdffGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool srst_value, bool clk_polarity, bool srst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, stringf("$_SDFF_%c%c%c_", clk_polarity ? 'P' : 'N', srst_polarity ? 'P' : 'N', srst_value ? '1' : '0'));
+ cell->setPort(ID::C, sig_clk);
+ cell->setPort(ID::R, sig_srst);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
+RTLIL::Cell* RTLIL::Module::addSdffeGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool srst_value, bool clk_polarity, bool en_polarity, bool srst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, stringf("$_SDFFE_%c%c%c%c_", clk_polarity ? 'P' : 'N', srst_polarity ? 'P' : 'N', srst_value ? '1' : '0', en_polarity ? 'P' : 'N'));
+ cell->setPort(ID::C, sig_clk);
+ cell->setPort(ID::R, sig_srst);
+ cell->setPort(ID::E, sig_en);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
+RTLIL::Cell* RTLIL::Module::addSdffceGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool srst_value, bool clk_polarity, bool en_polarity, bool srst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, stringf("$_SDFFCE_%c%c%c%c_", clk_polarity ? 'P' : 'N', srst_polarity ? 'P' : 'N', srst_value ? '1' : '0', en_polarity ? 'P' : 'N'));
+ cell->setPort(ID::C, sig_clk);
+ cell->setPort(ID::R, sig_srst);
+ cell->setPort(ID::E, sig_en);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addDlatchGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity, const std::string &src)
{
RTLIL::Cell *cell = addCell(name, stringf("$_DLATCH_%c_", en_polarity ? 'P' : 'N'));
@@ -2409,6 +2771,18 @@ RTLIL::Cell* RTLIL::Module::addDlatchGate(RTLIL::IdString name, const RTLIL::Sig
return cell;
}
+RTLIL::Cell* RTLIL::Module::addAdlatchGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool arst_value, bool en_polarity, bool arst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, stringf("$_DLATCH_%c%c%c_", en_polarity ? 'P' : 'N', arst_polarity ? 'P' : 'N', arst_value ? '1' : '0'));
+ cell->setPort(ID::E, sig_en);
+ cell->setPort(ID::R, sig_arst);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addDlatchsrGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity, bool set_polarity, bool clr_polarity, const std::string &src)
{
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index f3dc3af68..a03e8933c 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -375,6 +375,8 @@ namespace RTLIL
bool in(const char *rhs) const { return *this == rhs; }
bool in(const std::string &rhs) const { return *this == rhs; }
bool in(const pool<IdString> &rhs) const { return rhs.count(*this) != 0; }
+
+ bool isPublic() { return begins_with("\\"); }
};
namespace ID {
@@ -554,6 +556,29 @@ namespace RTLIL
return *this;
}
+ inline ObjIterator<T>& operator+=(int amt) {
+ log_assert(list_p != nullptr);
+ it += amt;
+ if (it == list_p->end()) {
+ (*refcount_p)--;
+ list_p = nullptr;
+ refcount_p = nullptr;
+ }
+ return *this;
+ }
+
+ inline ObjIterator<T> operator+(int amt) {
+ log_assert(list_p != nullptr);
+ ObjIterator<T> new_obj(*this);
+ new_obj.it += amt;
+ if (new_obj.it == list_p->end()) {
+ (*(new_obj.refcount_p))--;
+ new_obj.list_p = nullptr;
+ new_obj.refcount_p = nullptr;
+ }
+ return new_obj;
+ }
+
inline const ObjIterator<T> operator++(int) {
ObjIterator<T> result(*this);
++(*this);
@@ -1061,6 +1086,13 @@ struct RTLIL::Design
return selected_member(module->name, member->name);
}
+ template<typename T1> void select(T1 *module) {
+ if (selection_stack.size() > 0) {
+ RTLIL::Selection &sel = selection_stack.back();
+ sel.select(module);
+ }
+ }
+
template<typename T1, typename T2> void select(T1 *module, T2 *member) {
if (selection_stack.size() > 0) {
RTLIL::Selection &sel = selection_stack.back();
@@ -1244,8 +1276,14 @@ public:
RTLIL::Cell* addDff (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, const std::string &src = "");
RTLIL::Cell* addDffe (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, bool en_polarity = true, const std::string &src = "");
RTLIL::Cell* addDffsr (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr, RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, bool set_polarity = true, bool clr_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addDffsre (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr, RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, bool en_polarity = true, bool set_polarity = true, bool clr_polarity = true, const std::string &src = "");
RTLIL::Cell* addAdff (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, RTLIL::Const arst_value, bool clk_polarity = true, bool arst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addAdffe (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, RTLIL::Const arst_value, bool clk_polarity = true, bool en_polarity = true, bool arst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addSdff (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, RTLIL::Const srst_value, bool clk_polarity = true, bool srst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addSdffe (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, RTLIL::Const srst_value, bool clk_polarity = true, bool en_polarity = true, bool srst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addSdffce (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, RTLIL::Const srst_value, bool clk_polarity = true, bool en_polarity = true, bool srst_polarity = true, const std::string &src = "");
RTLIL::Cell* addDlatch (RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addAdlatch (RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, RTLIL::Const arst_value, bool en_polarity = true, bool arst_polarity = true, const std::string &src = "");
RTLIL::Cell* addDlatchsr (RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr, RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity = true, bool set_polarity = true, bool clr_polarity = true, const std::string &src = "");
RTLIL::Cell* addBufGate (RTLIL::IdString name, const RTLIL::SigBit &sig_a, const RTLIL::SigBit &sig_y, const std::string &src = "");
@@ -1265,14 +1303,28 @@ public:
RTLIL::Cell* addAoi4Gate (RTLIL::IdString name, const RTLIL::SigBit &sig_a, const RTLIL::SigBit &sig_b, const RTLIL::SigBit &sig_c, const RTLIL::SigBit &sig_d, const RTLIL::SigBit &sig_y, const std::string &src = "");
RTLIL::Cell* addOai4Gate (RTLIL::IdString name, const RTLIL::SigBit &sig_a, const RTLIL::SigBit &sig_b, const RTLIL::SigBit &sig_c, const RTLIL::SigBit &sig_d, const RTLIL::SigBit &sig_y, const std::string &src = "");
+ RTLIL::Cell* addSrGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
+ const RTLIL::SigSpec &sig_q, bool set_polarity = true, bool clr_polarity = true, const std::string &src = "");
RTLIL::Cell* addFfGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, const std::string &src = "");
RTLIL::Cell* addDffGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, const std::string &src = "");
RTLIL::Cell* addDffeGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, bool en_polarity = true, const std::string &src = "");
RTLIL::Cell* addDffsrGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, bool set_polarity = true, bool clr_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addDffsreGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
+ RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, bool en_polarity = true, bool set_polarity = true, bool clr_polarity = true, const std::string &src = "");
RTLIL::Cell* addAdffGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
bool arst_value = false, bool clk_polarity = true, bool arst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addAdffeGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool arst_value = false, bool clk_polarity = true, bool en_polarity = true, bool arst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addSdffGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool srst_value = false, bool clk_polarity = true, bool srst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addSdffeGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool srst_value = false, bool clk_polarity = true, bool en_polarity = true, bool srst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addSdffceGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool srst_value = false, bool clk_polarity = true, bool en_polarity = true, bool srst_polarity = true, const std::string &src = "");
RTLIL::Cell* addDlatchGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addAdlatchGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool arst_value = false, bool en_polarity = true, bool arst_polarity = true, const std::string &src = "");
RTLIL::Cell* addDlatchsrGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity = true, bool set_polarity = true, bool clr_polarity = true, const std::string &src = "");
diff --git a/kernel/satgen.cc b/kernel/satgen.cc
new file mode 100644
index 000000000..2a54e78ec
--- /dev/null
+++ b/kernel/satgen.cc
@@ -0,0 +1,1239 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/satgen.h"
+#include "kernel/ff.h"
+
+USING_YOSYS_NAMESPACE
+
+bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
+{
+ bool arith_undef_handled = false;
+ bool is_arith_compare = cell->type.in(ID($lt), ID($le), ID($ge), ID($gt));
+
+ if (model_undef && (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor)) || is_arith_compare))
+ {
+ 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);
+ if (is_arith_compare)
+ extendSignalWidth(undef_a, undef_b, cell, true);
+ else
+ extendSignalWidth(undef_a, undef_b, undef_y, cell, true);
+
+ int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
+ int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
+ int undef_y_bit = ez->OR(undef_any_a, undef_any_b);
+
+ if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor))) {
+ std::vector<int> b = importSigSpec(cell->getPort(ID::B), timestep);
+ undef_y_bit = ez->OR(undef_y_bit, ez->NOT(ez->expression(ezSAT::OpOr, b)));
+ }
+
+ if (is_arith_compare) {
+ for (size_t i = 1; i < undef_y.size(); i++)
+ ez->SET(ez->CONST_FALSE, undef_y.at(i));
+ ez->SET(undef_y_bit, undef_y.at(0));
+ } else {
+ std::vector<int> undef_y_bits(undef_y.size(), undef_y_bit);
+ ez->assume(ez->vec_eq(undef_y_bits, undef_y));
+ }
+
+ arith_undef_handled = true;
+ }
+
+ if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_),
+ ID($and), ID($or), ID($xor), ID($xnor), ID($add), ID($sub)))
+ {
+ 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);
+ extendSignalWidth(a, b, y, cell);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ if (cell->type.in(ID($and), ID($_AND_)))
+ ez->assume(ez->vec_eq(ez->vec_and(a, b), yy));
+ if (cell->type == ID($_NAND_))
+ ez->assume(ez->vec_eq(ez->vec_not(ez->vec_and(a, b)), yy));
+ if (cell->type.in(ID($or), ID($_OR_)))
+ ez->assume(ez->vec_eq(ez->vec_or(a, b), yy));
+ if (cell->type == ID($_NOR_))
+ ez->assume(ez->vec_eq(ez->vec_not(ez->vec_or(a, b)), yy));
+ if (cell->type.in(ID($xor), ID($_XOR_)))
+ ez->assume(ez->vec_eq(ez->vec_xor(a, b), yy));
+ if (cell->type.in(ID($xnor), ID($_XNOR_)))
+ ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(a, b)), yy));
+ if (cell->type == ID($_ANDNOT_))
+ ez->assume(ez->vec_eq(ez->vec_and(a, ez->vec_not(b)), yy));
+ if (cell->type == ID($_ORNOT_))
+ ez->assume(ez->vec_eq(ez->vec_or(a, ez->vec_not(b)), yy));
+ if (cell->type == ID($add))
+ ez->assume(ez->vec_eq(ez->vec_add(a, b), yy));
+ if (cell->type == ID($sub))
+ ez->assume(ez->vec_eq(ez->vec_sub(a, b), yy));
+
+ if (model_undef && !arith_undef_handled)
+ {
+ 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);
+ extendSignalWidth(undef_a, undef_b, undef_y, cell, false);
+
+ if (cell->type.in(ID($and), ID($_AND_), ID($_NAND_))) {
+ std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
+ std::vector<int> b0 = ez->vec_and(ez->vec_not(b), ez->vec_not(undef_b));
+ std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a0, b0)));
+ ez->assume(ez->vec_eq(yX, undef_y));
+ }
+ else if (cell->type.in(ID($or), ID($_OR_), ID($_NOR_))) {
+ std::vector<int> a1 = ez->vec_and(a, ez->vec_not(undef_a));
+ std::vector<int> b1 = ez->vec_and(b, ez->vec_not(undef_b));
+ std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a1, b1)));
+ ez->assume(ez->vec_eq(yX, undef_y));
+ }
+ else if (cell->type.in(ID($xor), ID($xnor), ID($_XOR_), ID($_XNOR_))) {
+ std::vector<int> yX = ez->vec_or(undef_a, undef_b);
+ ez->assume(ez->vec_eq(yX, undef_y));
+ }
+ else if (cell->type == ID($_ANDNOT_)) {
+ std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
+ std::vector<int> b1 = ez->vec_and(b, ez->vec_not(undef_b));
+ std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a0, b1)));
+ ez->assume(ez->vec_eq(yX, undef_y));
+ }
+
+ else if (cell->type == ID($_ORNOT_)) {
+ std::vector<int> a1 = ez->vec_and(a, ez->vec_not(undef_a));
+ std::vector<int> b0 = ez->vec_and(ez->vec_not(b), ez->vec_not(undef_b));
+ std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a1, b0)));
+ ez->assume(ez->vec_eq(yX, undef_y));
+ }
+ else
+ log_abort();
+
+ undefGating(y, yy, undef_y);
+ }
+ else if (model_undef)
+ {
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type.in(ID($_AOI3_), ID($_OAI3_), ID($_AOI4_), ID($_OAI4_)))
+ {
+ bool aoi_mode = cell->type.in(ID($_AOI3_), ID($_AOI4_));
+ bool three_mode = cell->type.in(ID($_AOI3_), ID($_OAI3_));
+
+ int a = importDefSigSpec(cell->getPort(ID::A), timestep).at(0);
+ int b = importDefSigSpec(cell->getPort(ID::B), timestep).at(0);
+ int c = importDefSigSpec(cell->getPort(ID::C), timestep).at(0);
+ int d = three_mode ? (aoi_mode ? ez->CONST_TRUE : ez->CONST_FALSE) : importDefSigSpec(cell->getPort(ID::D), timestep).at(0);
+ int y = importDefSigSpec(cell->getPort(ID::Y), timestep).at(0);
+ int yy = model_undef ? ez->literal() : y;
+
+ if (cell->type.in(ID($_AOI3_), ID($_AOI4_)))
+ ez->assume(ez->IFF(ez->NOT(ez->OR(ez->AND(a, b), ez->AND(c, d))), yy));
+ else
+ ez->assume(ez->IFF(ez->NOT(ez->AND(ez->OR(a, b), ez->OR(c, d))), yy));
+
+ if (model_undef)
+ {
+ int undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep).at(0);
+ int undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep).at(0);
+ int undef_c = importUndefSigSpec(cell->getPort(ID::C), timestep).at(0);
+ int undef_d = three_mode ? ez->CONST_FALSE : importUndefSigSpec(cell->getPort(ID::D), timestep).at(0);
+ int undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep).at(0);
+
+ if (aoi_mode)
+ {
+ int a0 = ez->AND(ez->NOT(a), ez->NOT(undef_a));
+ int b0 = ez->AND(ez->NOT(b), ez->NOT(undef_b));
+ int c0 = ez->AND(ez->NOT(c), ez->NOT(undef_c));
+ int d0 = ez->AND(ez->NOT(d), ez->NOT(undef_d));
+
+ int ab = ez->AND(a, b), cd = ez->AND(c, d);
+ int undef_ab = ez->AND(ez->OR(undef_a, undef_b), ez->NOT(ez->OR(a0, b0)));
+ int undef_cd = ez->AND(ez->OR(undef_c, undef_d), ez->NOT(ez->OR(c0, d0)));
+
+ int ab1 = ez->AND(ab, ez->NOT(undef_ab));
+ int cd1 = ez->AND(cd, ez->NOT(undef_cd));
+ int yX = ez->AND(ez->OR(undef_ab, undef_cd), ez->NOT(ez->OR(ab1, cd1)));
+
+ ez->assume(ez->IFF(yX, undef_y));
+ }
+ else
+ {
+ int a1 = ez->AND(a, ez->NOT(undef_a));
+ int b1 = ez->AND(b, ez->NOT(undef_b));
+ int c1 = ez->AND(c, ez->NOT(undef_c));
+ int d1 = ez->AND(d, ez->NOT(undef_d));
+
+ int ab = ez->OR(a, b), cd = ez->OR(c, d);
+ int undef_ab = ez->AND(ez->OR(undef_a, undef_b), ez->NOT(ez->OR(a1, b1)));
+ int undef_cd = ez->AND(ez->OR(undef_c, undef_d), ez->NOT(ez->OR(c1, d1)));
+
+ int ab0 = ez->AND(ez->NOT(ab), ez->NOT(undef_ab));
+ int cd0 = ez->AND(ez->NOT(cd), ez->NOT(undef_cd));
+ int yX = ez->AND(ez->OR(undef_ab, undef_cd), ez->NOT(ez->OR(ab0, cd0)));
+
+ ez->assume(ez->IFF(yX, undef_y));
+ }
+
+ undefGating(y, yy, undef_y);
+ }
+
+ return true;
+ }
+
+ if (cell->type.in(ID($_NOT_), ID($not)))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidthUnary(a, y, cell);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+ ez->assume(ez->vec_eq(ez->vec_not(a), yy));
+
+ if (model_undef) {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidthUnary(undef_a, undef_y, cell, false);
+ ez->assume(ez->vec_eq(undef_a, undef_y));
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type.in(ID($_MUX_), ID($mux), ID($_NMUX_)))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), 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
+ ez->assume(ez->vec_eq(ez->vec_ite(s.at(0), b, a), yy));
+
+ 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_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), 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));
+ ez->assume(ez->vec_eq(yX, undef_y));
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($pmux))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ std::vector<int> tmp = 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());
+ tmp = ez->vec_ite(s.at(i), part_of_b, tmp);
+ }
+ ez->assume(ez->vec_eq(tmp, yy));
+
+ 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_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+
+ int maybe_a = ez->CONST_TRUE;
+
+ 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);
+
+ 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);
+ }
+
+ 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);
+
+ ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(bits_set, bits_clr)), undef_y));
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type.in(ID($pos), ID($neg)))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidthUnary(a, y, cell);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ if (cell->type == ID($pos)) {
+ ez->assume(ez->vec_eq(a, yy));
+ } else {
+ std::vector<int> zero(a.size(), ez->CONST_FALSE);
+ ez->assume(ez->vec_eq(ez->vec_sub(zero, a), yy));
+ }
+
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidthUnary(undef_a, undef_y, cell);
+
+ if (cell->type == ID($pos)) {
+ ez->assume(ez->vec_eq(undef_a, undef_y));
+ } else {
+ int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
+ std::vector<int> undef_y_bits(undef_y.size(), undef_any_a);
+ ez->assume(ez->vec_eq(undef_y_bits, undef_y));
+ }
+
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_xnor), ID($reduce_bool), ID($logic_not)))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ if (cell->type == ID($reduce_and))
+ ez->SET(ez->expression(ez->OpAnd, a), yy.at(0));
+ if (cell->type.in(ID($reduce_or), ID($reduce_bool)))
+ ez->SET(ez->expression(ez->OpOr, a), yy.at(0));
+ if (cell->type == ID($reduce_xor))
+ ez->SET(ez->expression(ez->OpXor, a), yy.at(0));
+ if (cell->type == ID($reduce_xnor))
+ ez->SET(ez->NOT(ez->expression(ez->OpXor, a)), yy.at(0));
+ if (cell->type == ID($logic_not))
+ ez->SET(ez->NOT(ez->expression(ez->OpOr, a)), yy.at(0));
+ for (size_t i = 1; i < y.size(); i++)
+ ez->SET(ez->CONST_FALSE, yy.at(i));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ int aX = ez->expression(ezSAT::OpOr, undef_a);
+
+ if (cell->type == ID($reduce_and)) {
+ int a0 = ez->expression(ezSAT::OpOr, ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a)));
+ ez->assume(ez->IFF(ez->AND(ez->NOT(a0), aX), undef_y.at(0)));
+ }
+ else if (cell->type.in(ID($reduce_or), ID($reduce_bool), ID($logic_not))) {
+ int a1 = ez->expression(ezSAT::OpOr, ez->vec_and(a, ez->vec_not(undef_a)));
+ ez->assume(ez->IFF(ez->AND(ez->NOT(a1), aX), undef_y.at(0)));
+ }
+ else if (cell->type.in(ID($reduce_xor), ID($reduce_xnor))) {
+ ez->assume(ez->IFF(aX, undef_y.at(0)));
+ } else
+ log_abort();
+
+ for (size_t i = 1; i < undef_y.size(); i++)
+ ez->SET(ez->CONST_FALSE, undef_y.at(i));
+
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type.in(ID($logic_and), ID($logic_or)))
+ {
+ std::vector<int> vec_a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> vec_b = importDefSigSpec(cell->getPort(ID::B), timestep);
+
+ int a = ez->expression(ez->OpOr, vec_a);
+ int b = ez->expression(ez->OpOr, vec_b);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ if (cell->type == ID($logic_and))
+ ez->SET(ez->expression(ez->OpAnd, a, b), yy.at(0));
+ else
+ ez->SET(ez->expression(ez->OpOr, a, b), yy.at(0));
+ for (size_t i = 1; i < y.size(); i++)
+ ez->SET(ez->CONST_FALSE, yy.at(i));
+
+ 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);
+
+ int a0 = ez->NOT(ez->OR(ez->expression(ezSAT::OpOr, vec_a), ez->expression(ezSAT::OpOr, undef_a)));
+ int b0 = ez->NOT(ez->OR(ez->expression(ezSAT::OpOr, vec_b), ez->expression(ezSAT::OpOr, undef_b)));
+ int a1 = ez->expression(ezSAT::OpOr, ez->vec_and(vec_a, ez->vec_not(undef_a)));
+ int b1 = ez->expression(ezSAT::OpOr, ez->vec_and(vec_b, ez->vec_not(undef_b)));
+ int aX = ez->expression(ezSAT::OpOr, undef_a);
+ int bX = ez->expression(ezSAT::OpOr, undef_b);
+
+ if (cell->type == ID($logic_and))
+ ez->SET(ez->AND(ez->OR(aX, bX), ez->NOT(ez->AND(a1, b1)), ez->NOT(a0), ez->NOT(b0)), undef_y.at(0));
+ else if (cell->type == ID($logic_or))
+ ez->SET(ez->AND(ez->OR(aX, bX), ez->NOT(ez->AND(a0, b0)), ez->NOT(a1), ez->NOT(b1)), undef_y.at(0));
+ else
+ log_abort();
+
+ for (size_t i = 1; i < undef_y.size(); i++)
+ ez->SET(ez->CONST_FALSE, undef_y.at(i));
+
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type.in(ID($lt), ID($le), ID($eq), ID($ne), ID($eqx), ID($nex), ID($ge), ID($gt)))
+ {
+ bool is_signed = cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool();
+ 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);
+ extendSignalWidth(a, b, cell);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ if (model_undef && cell->type.in(ID($eqx), ID($nex))) {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
+ extendSignalWidth(undef_a, undef_b, cell, true);
+ a = ez->vec_or(a, undef_a);
+ b = ez->vec_or(b, undef_b);
+ }
+
+ if (cell->type == ID($lt))
+ ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), yy.at(0));
+ if (cell->type == ID($le))
+ ez->SET(is_signed ? ez->vec_le_signed(a, b) : ez->vec_le_unsigned(a, b), yy.at(0));
+ if (cell->type.in(ID($eq), ID($eqx)))
+ ez->SET(ez->vec_eq(a, b), yy.at(0));
+ if (cell->type.in(ID($ne), ID($nex)))
+ ez->SET(ez->vec_ne(a, b), yy.at(0));
+ if (cell->type == ID($ge))
+ ez->SET(is_signed ? ez->vec_ge_signed(a, b) : ez->vec_ge_unsigned(a, b), yy.at(0));
+ if (cell->type == ID($gt))
+ ez->SET(is_signed ? ez->vec_gt_signed(a, b) : ez->vec_gt_unsigned(a, b), yy.at(0));
+ for (size_t i = 1; i < y.size(); i++)
+ ez->SET(ez->CONST_FALSE, yy.at(i));
+
+ if (model_undef && cell->type.in(ID($eqx), ID($nex)))
+ {
+ 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);
+ extendSignalWidth(undef_a, undef_b, cell, true);
+
+ if (cell->type == ID($eqx))
+ yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
+ else
+ yy.at(0) = ez->OR(yy.at(0), ez->vec_ne(undef_a, undef_b));
+
+ for (size_t i = 0; i < y.size(); i++)
+ ez->SET(ez->CONST_FALSE, undef_y.at(i));
+
+ ez->assume(ez->vec_eq(y, yy));
+ }
+ else if (model_undef && cell->type.in(ID($eq), ID($ne)))
+ {
+ 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);
+ extendSignalWidth(undef_a, undef_b, cell, true);
+
+ int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
+ int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
+ int undef_any = ez->OR(undef_any_a, undef_any_b);
+
+ std::vector<int> masked_a_bits = ez->vec_or(a, ez->vec_or(undef_a, undef_b));
+ std::vector<int> masked_b_bits = ez->vec_or(b, ez->vec_or(undef_a, undef_b));
+
+ int masked_ne = ez->vec_ne(masked_a_bits, masked_b_bits);
+ int undef_y_bit = ez->AND(undef_any, ez->NOT(masked_ne));
+
+ for (size_t i = 1; i < undef_y.size(); i++)
+ ez->SET(ez->CONST_FALSE, undef_y.at(i));
+ ez->SET(undef_y_bit, undef_y.at(0));
+
+ undefGating(y, yy, undef_y);
+ }
+ else
+ {
+ if (model_undef) {
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ undefGating(y, yy, undef_y);
+ }
+ log_assert(!model_undef || arith_undef_handled);
+ }
+ return true;
+ }
+
+ if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)))
+ {
+ 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);
+
+ int extend_bit = ez->CONST_FALSE;
+
+ if (cell->parameters[ID::A_SIGNED].as_bool())
+ extend_bit = a.back();
+
+ while (y.size() < a.size())
+ y.push_back(ez->literal());
+ while (y.size() > a.size())
+ a.push_back(extend_bit);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+ std::vector<int> shifted_a;
+
+ if (cell->type.in( ID($shl), ID($sshl)))
+ shifted_a = ez->vec_shift_left(a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
+
+ if (cell->type == ID($shr))
+ shifted_a = ez->vec_shift_right(a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
+
+ if (cell->type == ID($sshr))
+ shifted_a = ez->vec_shift_right(a, b, false, cell->parameters[ID::A_SIGNED].as_bool() ? a.back() : ez->CONST_FALSE, ez->CONST_FALSE);
+
+ if (cell->type.in(ID($shift), ID($shiftx)))
+ shifted_a = ez->vec_shift_right(a, b, cell->parameters[ID::B_SIGNED].as_bool(), ez->CONST_FALSE, ez->CONST_FALSE);
+
+ ez->assume(ez->vec_eq(shifted_a, yy));
+
+ 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> undef_a_shifted;
+
+ extend_bit = cell->type == ID($shiftx) ? ez->CONST_TRUE : ez->CONST_FALSE;
+ if (cell->parameters[ID::A_SIGNED].as_bool())
+ extend_bit = undef_a.back();
+
+ while (undef_y.size() < undef_a.size())
+ undef_y.push_back(ez->literal());
+ while (undef_y.size() > undef_a.size())
+ undef_a.push_back(extend_bit);
+
+ if (cell->type.in(ID($shl), ID($sshl)))
+ undef_a_shifted = ez->vec_shift_left(undef_a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
+
+ if (cell->type == ID($shr))
+ undef_a_shifted = ez->vec_shift_right(undef_a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
+
+ if (cell->type == ID($sshr))
+ undef_a_shifted = ez->vec_shift_right(undef_a, b, false, cell->parameters[ID::A_SIGNED].as_bool() ? undef_a.back() : ez->CONST_FALSE, ez->CONST_FALSE);
+
+ if (cell->type == ID($shift))
+ undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters[ID::B_SIGNED].as_bool(), ez->CONST_FALSE, ez->CONST_FALSE);
+
+ if (cell->type == ID($shiftx))
+ undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters[ID::B_SIGNED].as_bool(), ez->CONST_TRUE, ez->CONST_TRUE);
+
+ int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
+ std::vector<int> undef_all_y_bits(undef_y.size(), undef_any_b);
+ ez->assume(ez->vec_eq(ez->vec_or(undef_a_shifted, undef_all_y_bits), undef_y));
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($mul))
+ {
+ 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);
+ extendSignalWidth(a, b, y, cell);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ std::vector<int> tmp(a.size(), ez->CONST_FALSE);
+ for (int i = 0; i < int(a.size()); i++)
+ {
+ std::vector<int> shifted_a(a.size(), ez->CONST_FALSE);
+ for (int j = i; j < int(a.size()); j++)
+ shifted_a.at(j) = a.at(j-i);
+ tmp = ez->vec_ite(b.at(i), ez->vec_add(tmp, shifted_a), tmp);
+ }
+ ez->assume(ez->vec_eq(tmp, yy));
+
+ if (model_undef) {
+ log_assert(arith_undef_handled);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($macc))
+ {
+ 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);
+
+ Macc macc;
+ macc.from_cell(cell);
+
+ std::vector<int> tmp(GetSize(y), ez->CONST_FALSE);
+
+ for (auto &port : macc.ports)
+ {
+ std::vector<int> in_a = importDefSigSpec(port.in_a, timestep);
+ std::vector<int> in_b = importDefSigSpec(port.in_b, timestep);
+
+ while (GetSize(in_a) < GetSize(y))
+ in_a.push_back(port.is_signed && !in_a.empty() ? in_a.back() : ez->CONST_FALSE);
+ in_a.resize(GetSize(y));
+
+ if (GetSize(in_b))
+ {
+ while (GetSize(in_b) < GetSize(y))
+ in_b.push_back(port.is_signed && !in_b.empty() ? in_b.back() : ez->CONST_FALSE);
+ in_b.resize(GetSize(y));
+
+ for (int i = 0; i < GetSize(in_b); i++) {
+ std::vector<int> shifted_a(in_a.size(), ez->CONST_FALSE);
+ for (int j = i; j < int(in_a.size()); j++)
+ shifted_a.at(j) = in_a.at(j-i);
+ if (port.do_subtract)
+ tmp = ez->vec_ite(in_b.at(i), ez->vec_sub(tmp, shifted_a), tmp);
+ else
+ tmp = ez->vec_ite(in_b.at(i), ez->vec_add(tmp, shifted_a), tmp);
+ }
+ }
+ else
+ {
+ if (port.do_subtract)
+ tmp = ez->vec_sub(tmp, in_a);
+ else
+ tmp = ez->vec_add(tmp, in_a);
+ }
+ }
+
+ for (int i = 0; i < GetSize(b); i++) {
+ std::vector<int> val(GetSize(y), ez->CONST_FALSE);
+ val.at(0) = b.at(i);
+ tmp = ez->vec_add(tmp, val);
+ }
+
+ 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);
+
+ int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
+ int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
+
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ ez->assume(ez->vec_eq(undef_y, std::vector<int>(GetSize(y), ez->OR(undef_any_a, undef_any_b))));
+
+ undefGating(y, tmp, undef_y);
+ }
+ else
+ ez->assume(ez->vec_eq(y, tmp));
+
+ return true;
+ }
+
+ if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor)))
+ {
+ 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);
+ extendSignalWidth(a, b, y, cell);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ std::vector<int> a_u, b_u;
+ if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
+ a_u = ez->vec_ite(a.back(), ez->vec_neg(a), a);
+ b_u = ez->vec_ite(b.back(), ez->vec_neg(b), b);
+ } else {
+ a_u = a;
+ b_u = b;
+ }
+
+ std::vector<int> chain_buf = a_u;
+ std::vector<int> y_u(a_u.size(), ez->CONST_FALSE);
+ for (int i = int(a.size())-1; i >= 0; i--)
+ {
+ chain_buf.insert(chain_buf.end(), chain_buf.size(), ez->CONST_FALSE);
+
+ std::vector<int> b_shl(i, ez->CONST_FALSE);
+ b_shl.insert(b_shl.end(), b_u.begin(), b_u.end());
+ b_shl.insert(b_shl.end(), chain_buf.size()-b_shl.size(), ez->CONST_FALSE);
+
+ y_u.at(i) = ez->vec_ge_unsigned(chain_buf, b_shl);
+ chain_buf = ez->vec_ite(y_u.at(i), ez->vec_sub(chain_buf, b_shl), chain_buf);
+
+ chain_buf.erase(chain_buf.begin() + a_u.size(), chain_buf.end());
+ }
+
+ std::vector<int> y_tmp = ignore_div_by_zero ? yy : ez->vec_var(y.size());
+
+ // modulo calculation
+ std::vector<int> modulo_trunc;
+ int floored_eq_trunc;
+ if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
+ modulo_trunc = ez->vec_ite(a.back(), ez->vec_neg(chain_buf), chain_buf);
+ // floor == trunc when sgn(a) == sgn(b) or trunc == 0
+ floored_eq_trunc = ez->OR(ez->IFF(a.back(), b.back()), ez->NOT(ez->expression(ezSAT::OpOr, modulo_trunc)));
+ } else {
+ modulo_trunc = chain_buf;
+ floored_eq_trunc = ez->CONST_TRUE;
+ }
+
+ if (cell->type == ID($div)) {
+ if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
+ ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(ez->XOR(a.back(), b.back()), ez->vec_neg(y_u), y_u)));
+ else
+ ez->assume(ez->vec_eq(y_tmp, y_u));
+ } else if (cell->type == ID($mod)) {
+ ez->assume(ez->vec_eq(y_tmp, modulo_trunc));
+ } else if (cell->type == ID($divfloor)) {
+ if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
+ ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(
+ ez->XOR(a.back(), b.back()),
+ ez->vec_neg(ez->vec_ite(
+ ez->vec_reduce_or(modulo_trunc),
+ ez->vec_add(y_u, ez->vec_const_unsigned(1, y_u.size())),
+ y_u
+ )),
+ y_u
+ )));
+ else
+ ez->assume(ez->vec_eq(y_tmp, y_u));
+ } else if (cell->type == ID($modfloor)) {
+ ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(floored_eq_trunc, modulo_trunc, ez->vec_add(modulo_trunc, b))));
+ }
+
+ if (ignore_div_by_zero) {
+ ez->assume(ez->expression(ezSAT::OpOr, b));
+ } else {
+ std::vector<int> div_zero_result;
+ if (cell->type.in(ID($div), ID($divfloor))) {
+ if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
+ std::vector<int> all_ones(y.size(), ez->CONST_TRUE);
+ std::vector<int> only_first_one(y.size(), ez->CONST_FALSE);
+ only_first_one.at(0) = ez->CONST_TRUE;
+ div_zero_result = ez->vec_ite(a.back(), only_first_one, all_ones);
+ } else {
+ div_zero_result.insert(div_zero_result.end(), cell->getPort(ID::A).size(), ez->CONST_TRUE);
+ div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
+ }
+ } else if (cell->type.in(ID($mod), ID($modfloor))) {
+ // a mod 0 = a
+ int copy_a_bits = min(cell->getPort(ID::A).size(), cell->getPort(ID::B).size());
+ div_zero_result.insert(div_zero_result.end(), a.begin(), a.begin() + copy_a_bits);
+ if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
+ div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), div_zero_result.back());
+ else
+ div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
+ }
+ ez->assume(ez->vec_eq(yy, ez->vec_ite(ez->expression(ezSAT::OpOr, b), y_tmp, div_zero_result)));
+ }
+
+ if (model_undef) {
+ log_assert(arith_undef_handled);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($lut))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+
+ std::vector<int> lut;
+ for (auto bit : cell->getParam(ID::LUT).bits)
+ lut.push_back(bit == State::S1 ? ez->CONST_TRUE : ez->CONST_FALSE);
+ while (GetSize(lut) < (1 << GetSize(a)))
+ lut.push_back(ez->CONST_FALSE);
+ lut.resize(1 << GetSize(a));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> t(lut), u(GetSize(t), ez->CONST_FALSE);
+
+ for (int i = GetSize(a)-1; i >= 0; i--)
+ {
+ std::vector<int> t0(t.begin(), t.begin() + GetSize(t)/2);
+ std::vector<int> t1(t.begin() + GetSize(t)/2, t.end());
+
+ std::vector<int> u0(u.begin(), u.begin() + GetSize(u)/2);
+ std::vector<int> u1(u.begin() + GetSize(u)/2, u.end());
+
+ t = ez->vec_ite(a[i], t1, t0);
+ u = ez->vec_ite(undef_a[i], ez->vec_or(ez->vec_xor(t0, t1), ez->vec_or(u0, u1)), ez->vec_ite(a[i], u1, u0));
+ }
+
+ log_assert(GetSize(t) == 1);
+ log_assert(GetSize(u) == 1);
+ undefGating(y, t, u);
+ ez->assume(ez->vec_eq(importUndefSigSpec(cell->getPort(ID::Y), timestep), u));
+ }
+ else
+ {
+ std::vector<int> t = lut;
+ for (int i = GetSize(a)-1; i >= 0; i--)
+ {
+ std::vector<int> t0(t.begin(), t.begin() + GetSize(t)/2);
+ std::vector<int> t1(t.begin() + GetSize(t)/2, t.end());
+ t = ez->vec_ite(a[i], t1, t0);
+ }
+
+ log_assert(GetSize(t) == 1);
+ ez->assume(ez->vec_eq(y, t));
+ }
+ return true;
+ }
+
+ if (cell->type == ID($sop))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ int y = importDefSigSpec(cell->getPort(ID::Y), timestep).at(0);
+
+ int width = cell->getParam(ID::WIDTH).as_int();
+ int depth = cell->getParam(ID::DEPTH).as_int();
+
+ vector<State> table_raw = cell->getParam(ID::TABLE).bits;
+ while (GetSize(table_raw) < 2*width*depth)
+ table_raw.push_back(State::S0);
+
+ vector<vector<int>> table(depth);
+
+ for (int i = 0; i < depth; i++)
+ for (int j = 0; j < width; j++)
+ {
+ bool pat0 = (table_raw[2*width*i + 2*j + 0] == State::S1);
+ bool pat1 = (table_raw[2*width*i + 2*j + 1] == State::S1);
+
+ if (pat0 && !pat1)
+ table.at(i).push_back(0);
+ else if (!pat0 && pat1)
+ table.at(i).push_back(1);
+ else
+ table.at(i).push_back(-1);
+ }
+
+ if (model_undef)
+ {
+ std::vector<int> products, undef_products;
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ int undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep).at(0);
+
+ for (int i = 0; i < depth; i++)
+ {
+ std::vector<int> cmp_a, cmp_ua, cmp_b;
+
+ for (int j = 0; j < width; j++)
+ if (table.at(i).at(j) >= 0) {
+ cmp_a.push_back(a.at(j));
+ cmp_ua.push_back(undef_a.at(j));
+ cmp_b.push_back(table.at(i).at(j) ? ez->CONST_TRUE : ez->CONST_FALSE);
+ }
+
+ std::vector<int> masked_a = ez->vec_or(cmp_a, cmp_ua);
+ std::vector<int> masked_b = ez->vec_or(cmp_b, cmp_ua);
+
+ int masked_eq = ez->vec_eq(masked_a, masked_b);
+ int any_undef = ez->expression(ezSAT::OpOr, cmp_ua);
+
+ undef_products.push_back(ez->AND(any_undef, masked_eq));
+ products.push_back(ez->AND(ez->NOT(any_undef), masked_eq));
+ }
+
+ int yy = ez->expression(ezSAT::OpOr, products);
+ ez->SET(undef_y, ez->AND(ez->NOT(yy), ez->expression(ezSAT::OpOr, undef_products)));
+ undefGating(y, yy, undef_y);
+ }
+ else
+ {
+ std::vector<int> products;
+
+ for (int i = 0; i < depth; i++)
+ {
+ std::vector<int> cmp_a, cmp_b;
+
+ for (int j = 0; j < width; j++)
+ if (table.at(i).at(j) >= 0) {
+ cmp_a.push_back(a.at(j));
+ cmp_b.push_back(table.at(i).at(j) ? ez->CONST_TRUE : ez->CONST_FALSE);
+ }
+
+ products.push_back(ez->vec_eq(cmp_a, cmp_b));
+ }
+
+ ez->SET(y, ez->expression(ezSAT::OpOr, products));
+ }
+
+ return true;
+ }
+
+ if (cell->type == ID($fa))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> c = importDefSigSpec(cell->getPort(ID::C), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ std::vector<int> x = importDefSigSpec(cell->getPort(ID::X), timestep);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+ std::vector<int> xx = model_undef ? ez->vec_var(x.size()) : x;
+
+ std::vector<int> t1 = ez->vec_xor(a, b);
+ ez->assume(ez->vec_eq(yy, ez->vec_xor(t1, c)));
+
+ std::vector<int> t2 = ez->vec_and(a, b);
+ std::vector<int> t3 = ez->vec_and(c, t1);
+ ez->assume(ez->vec_eq(xx, ez->vec_or(t2, t3)));
+
+ 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_c = importUndefSigSpec(cell->getPort(ID::C), timestep);
+
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ std::vector<int> undef_x = importUndefSigSpec(cell->getPort(ID::X), timestep);
+
+ ez->assume(ez->vec_eq(undef_y, ez->vec_or(ez->vec_or(undef_a, undef_b), undef_c)));
+ ez->assume(ez->vec_eq(undef_x, undef_y));
+
+ undefGating(y, yy, undef_y);
+ undefGating(x, xx, undef_x);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($lcu))
+ {
+ std::vector<int> p = importDefSigSpec(cell->getPort(ID::P), timestep);
+ std::vector<int> g = importDefSigSpec(cell->getPort(ID::G), timestep);
+ std::vector<int> ci = importDefSigSpec(cell->getPort(ID::CI), timestep);
+ std::vector<int> co = importDefSigSpec(cell->getPort(ID::CO), timestep);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(co.size()) : co;
+
+ for (int i = 0; i < GetSize(co); i++)
+ ez->SET(yy[i], ez->OR(g[i], ez->AND(p[i], i ? yy[i-1] : ci[0])));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_p = importUndefSigSpec(cell->getPort(ID::P), timestep);
+ std::vector<int> undef_g = importUndefSigSpec(cell->getPort(ID::G), timestep);
+ std::vector<int> undef_ci = importUndefSigSpec(cell->getPort(ID::CI), timestep);
+ std::vector<int> undef_co = importUndefSigSpec(cell->getPort(ID::CO), timestep);
+
+ int undef_any_p = ez->expression(ezSAT::OpOr, undef_p);
+ int undef_any_g = ez->expression(ezSAT::OpOr, undef_g);
+ int undef_any_ci = ez->expression(ezSAT::OpOr, undef_ci);
+ int undef_co_bit = ez->OR(undef_any_p, undef_any_g, undef_any_ci);
+
+ std::vector<int> undef_co_bits(undef_co.size(), undef_co_bit);
+ ez->assume(ez->vec_eq(undef_co_bits, undef_co));
+
+ undefGating(co, yy, undef_co);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($alu))
+ {
+ 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> x = importDefSigSpec(cell->getPort(ID::X), timestep);
+ std::vector<int> ci = importDefSigSpec(cell->getPort(ID::CI), timestep);
+ std::vector<int> bi = importDefSigSpec(cell->getPort(ID::BI), timestep);
+ std::vector<int> co = importDefSigSpec(cell->getPort(ID::CO), timestep);
+
+ extendSignalWidth(a, b, y, cell);
+ extendSignalWidth(a, b, x, cell);
+ extendSignalWidth(a, b, co, cell);
+
+ std::vector<int> def_y = model_undef ? ez->vec_var(y.size()) : y;
+ std::vector<int> def_x = model_undef ? ez->vec_var(x.size()) : x;
+ std::vector<int> def_co = model_undef ? ez->vec_var(co.size()) : co;
+
+ log_assert(GetSize(y) == GetSize(x));
+ log_assert(GetSize(y) == GetSize(co));
+ log_assert(GetSize(ci) == 1);
+ log_assert(GetSize(bi) == 1);
+
+ for (int i = 0; i < GetSize(y); i++)
+ {
+ int s1 = a.at(i), s2 = ez->XOR(b.at(i), bi.at(0)), s3 = i ? co.at(i-1) : ci.at(0);
+ ez->SET(def_x.at(i), ez->XOR(s1, s2));
+ ez->SET(def_y.at(i), ez->XOR(def_x.at(i), s3));
+ ez->SET(def_co.at(i), ez->OR(ez->AND(s1, s2), ez->AND(s1, s3), ez->AND(s2, s3)));
+ }
+
+ 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_ci = importUndefSigSpec(cell->getPort(ID::CI), timestep);
+ std::vector<int> undef_bi = importUndefSigSpec(cell->getPort(ID::BI), timestep);
+
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ std::vector<int> undef_x = importUndefSigSpec(cell->getPort(ID::X), timestep);
+ std::vector<int> undef_co = importUndefSigSpec(cell->getPort(ID::CO), timestep);
+
+ extendSignalWidth(undef_a, undef_b, undef_y, cell);
+ extendSignalWidth(undef_a, undef_b, undef_x, cell);
+ extendSignalWidth(undef_a, undef_b, undef_co, cell);
+
+ std::vector<int> all_inputs_undef;
+ all_inputs_undef.insert(all_inputs_undef.end(), undef_a.begin(), undef_a.end());
+ all_inputs_undef.insert(all_inputs_undef.end(), undef_b.begin(), undef_b.end());
+ all_inputs_undef.insert(all_inputs_undef.end(), undef_ci.begin(), undef_ci.end());
+ all_inputs_undef.insert(all_inputs_undef.end(), undef_bi.begin(), undef_bi.end());
+ int undef_any = ez->expression(ezSAT::OpOr, all_inputs_undef);
+
+ for (int i = 0; i < GetSize(undef_y); i++) {
+ ez->SET(undef_y.at(i), undef_any);
+ ez->SET(undef_x.at(i), ez->OR(undef_a.at(i), undef_b.at(i), undef_bi.at(0)));
+ ez->SET(undef_co.at(i), undef_any);
+ }
+
+ undefGating(y, def_y, undef_y);
+ undefGating(x, def_x, undef_x);
+ undefGating(co, def_co, undef_co);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($slice))
+ {
+ RTLIL::SigSpec a = cell->getPort(ID::A);
+ RTLIL::SigSpec y = cell->getPort(ID::Y);
+ ez->assume(signals_eq(a.extract(cell->parameters.at(ID::OFFSET).as_int(), y.size()), y, timestep));
+ return true;
+ }
+
+ if (cell->type == ID($concat))
+ {
+ RTLIL::SigSpec a = cell->getPort(ID::A);
+ RTLIL::SigSpec b = cell->getPort(ID::B);
+ RTLIL::SigSpec y = cell->getPort(ID::Y);
+
+ RTLIL::SigSpec ab = a;
+ ab.append(b);
+
+ ez->assume(signals_eq(ab, y, timestep));
+ return true;
+ }
+
+ if (timestep > 0 && RTLIL::builtin_ff_cell_types().count(cell->type))
+ {
+ FfData ff(nullptr, cell);
+
+ // Latches and FFs with async inputs are not supported — use clk2fflogic or async2sync first.
+ if (!ff.has_d || ff.has_arst || ff.has_sr || (ff.has_en && !ff.has_clk))
+ return false;
+
+ if (timestep == 1)
+ {
+ initial_state.add((*sigmap)(cell->getPort(ID::Q)));
+ }
+ else
+ {
+ std::vector<int> d = importDefSigSpec(cell->getPort(ID::D), timestep-1);
+ std::vector<int> undef_d;
+ if (model_undef)
+ undef_d = importUndefSigSpec(cell->getPort(ID::D), timestep-1);
+ if (ff.has_srst && ff.has_en && ff.ce_over_srst) {
+ int srst = importDefSigSpec(ff.sig_srst, timestep-1).at(0);
+ std::vector<int> rval = importDefSigSpec(ff.val_srst, timestep-1);
+ int undef_srst;
+ std::vector<int> undef_rval;
+ if (model_undef) {
+ undef_srst = importUndefSigSpec(ff.sig_srst, timestep-1).at(0);
+ undef_rval = importUndefSigSpec(ff.val_srst, timestep-1);
+ }
+ if (ff.pol_srst)
+ std::tie(d, undef_d) = mux(srst, undef_srst, d, undef_d, rval, undef_rval);
+ else
+ std::tie(d, undef_d) = mux(srst, undef_srst, rval, undef_rval, d, undef_d);
+ }
+ if (ff.has_en) {
+ int en = importDefSigSpec(ff.sig_en, timestep-1).at(0);
+ std::vector<int> old_q = importDefSigSpec(ff.sig_q, timestep-1);
+ int undef_en;
+ std::vector<int> undef_old_q;
+ if (model_undef) {
+ undef_en = importUndefSigSpec(ff.sig_en, timestep-1).at(0);
+ undef_old_q = importUndefSigSpec(ff.sig_q, timestep-1);
+ }
+ if (ff.pol_en)
+ std::tie(d, undef_d) = mux(en, undef_en, old_q, undef_old_q, d, undef_d);
+ else
+ std::tie(d, undef_d) = mux(en, undef_en, d, undef_d, old_q, undef_old_q);
+ }
+ if (ff.has_srst && !(ff.has_en && ff.ce_over_srst)) {
+ int srst = importDefSigSpec(ff.sig_srst, timestep-1).at(0);
+ std::vector<int> rval = importDefSigSpec(ff.val_srst, timestep-1);
+ int undef_srst;
+ std::vector<int> undef_rval;
+ if (model_undef) {
+ undef_srst = importUndefSigSpec(ff.sig_srst, timestep-1).at(0);
+ undef_rval = importUndefSigSpec(ff.val_srst, timestep-1);
+ }
+ if (ff.pol_srst)
+ std::tie(d, undef_d) = mux(srst, undef_srst, d, undef_d, rval, undef_rval);
+ else
+ std::tie(d, undef_d) = mux(srst, undef_srst, rval, undef_rval, d, undef_d);
+ }
+ std::vector<int> q = importDefSigSpec(cell->getPort(ID::Q), timestep);
+
+ std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
+ ez->assume(ez->vec_eq(d, qq));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Q), timestep);
+
+ ez->assume(ez->vec_eq(undef_d, undef_q));
+ undefGating(q, qq, undef_q);
+ }
+ }
+ return true;
+ }
+
+ if (cell->type == ID($anyconst))
+ {
+ if (timestep < 2)
+ return true;
+
+ std::vector<int> d = importDefSigSpec(cell->getPort(ID::Y), timestep-1);
+ std::vector<int> q = importDefSigSpec(cell->getPort(ID::Y), timestep);
+
+ std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
+ ez->assume(ez->vec_eq(d, qq));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_d = importUndefSigSpec(cell->getPort(ID::Y), timestep-1);
+ std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+
+ ez->assume(ez->vec_eq(undef_d, undef_q));
+ undefGating(q, qq, undef_q);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($anyseq))
+ {
+ return true;
+ }
+
+ if (cell->type.in(ID($_BUF_), ID($equiv)))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidthUnary(a, y, cell);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+ ez->assume(ez->vec_eq(a, yy));
+
+ if (model_undef) {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidthUnary(undef_a, undef_y, cell, false);
+ ez->assume(ez->vec_eq(undef_a, undef_y));
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($initstate))
+ {
+ auto key = make_pair(prefix, timestep);
+ if (initstates.count(key) == 0)
+ initstates[key] = false;
+
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ log_assert(GetSize(y) == 1);
+ ez->SET(y[0], initstates[key] ? ez->CONST_TRUE : ez->CONST_FALSE);
+
+ if (model_undef) {
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ log_assert(GetSize(undef_y) == 1);
+ ez->SET(undef_y[0], ez->CONST_FALSE);
+ }
+
+ return true;
+ }
+
+ if (cell->type == ID($assert))
+ {
+ std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
+ asserts_a[pf].append((*sigmap)(cell->getPort(ID::A)));
+ asserts_en[pf].append((*sigmap)(cell->getPort(ID::EN)));
+ return true;
+ }
+
+ if (cell->type == ID($assume))
+ {
+ std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
+ assumes_a[pf].append((*sigmap)(cell->getPort(ID::A)));
+ assumes_en[pf].append((*sigmap)(cell->getPort(ID::EN)));
+ return true;
+ }
+
+ // Unsupported internal cell types: $pow $fsm $mem*
+ // .. and all sequential cells with asynchronous inputs
+ return false;
+}
diff --git a/kernel/satgen.h b/kernel/satgen.h
index 3929a8708..cf2db733f 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -262,6 +262,18 @@ struct SatGen
}
}
+ std::pair<std::vector<int>, std::vector<int>> mux(int s, int undef_s, const std::vector<int> &a, const std::vector<int> &undef_a, const std::vector<int> &b, const std::vector<int> &undef_b) {
+ std::vector<int> res;
+ std::vector<int> undef_res;
+ res = ez->vec_ite(s, b, a);
+ if (model_undef) {
+ 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));
+ undef_res = ez->vec_ite(undef_s, undef_ab, ez->vec_ite(s, undef_b, undef_a));
+ }
+ return std::make_pair(res, undef_res);
+ }
+
void undefGating(int y, int yy, int undef)
{
ez->assume(ez->OR(undef, ez->IFF(y, yy)));
@@ -274,1171 +286,7 @@ struct SatGen
initstates[key] = true;
}
- bool importCell(RTLIL::Cell *cell, int timestep = -1)
- {
- bool arith_undef_handled = false;
- bool is_arith_compare = cell->type.in(ID($lt), ID($le), ID($ge), ID($gt));
-
- if (model_undef && (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor)) || is_arith_compare))
- {
- 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);
- if (is_arith_compare)
- extendSignalWidth(undef_a, undef_b, cell, true);
- else
- extendSignalWidth(undef_a, undef_b, undef_y, cell, true);
-
- int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
- int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
- int undef_y_bit = ez->OR(undef_any_a, undef_any_b);
-
- if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor))) {
- std::vector<int> b = importSigSpec(cell->getPort(ID::B), timestep);
- undef_y_bit = ez->OR(undef_y_bit, ez->NOT(ez->expression(ezSAT::OpOr, b)));
- }
-
- if (is_arith_compare) {
- for (size_t i = 1; i < undef_y.size(); i++)
- ez->SET(ez->CONST_FALSE, undef_y.at(i));
- ez->SET(undef_y_bit, undef_y.at(0));
- } else {
- std::vector<int> undef_y_bits(undef_y.size(), undef_y_bit);
- ez->assume(ez->vec_eq(undef_y_bits, undef_y));
- }
-
- arith_undef_handled = true;
- }
-
- if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_),
- ID($and), ID($or), ID($xor), ID($xnor), ID($add), ID($sub)))
- {
- 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);
- extendSignalWidth(a, b, y, cell);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- if (cell->type.in(ID($and), ID($_AND_)))
- ez->assume(ez->vec_eq(ez->vec_and(a, b), yy));
- if (cell->type == ID($_NAND_))
- ez->assume(ez->vec_eq(ez->vec_not(ez->vec_and(a, b)), yy));
- if (cell->type.in(ID($or), ID($_OR_)))
- ez->assume(ez->vec_eq(ez->vec_or(a, b), yy));
- if (cell->type == ID($_NOR_))
- ez->assume(ez->vec_eq(ez->vec_not(ez->vec_or(a, b)), yy));
- if (cell->type.in(ID($xor), ID($_XOR_)))
- ez->assume(ez->vec_eq(ez->vec_xor(a, b), yy));
- if (cell->type.in(ID($xnor), ID($_XNOR_)))
- ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(a, b)), yy));
- if (cell->type == ID($_ANDNOT_))
- ez->assume(ez->vec_eq(ez->vec_and(a, ez->vec_not(b)), yy));
- if (cell->type == ID($_ORNOT_))
- ez->assume(ez->vec_eq(ez->vec_or(a, ez->vec_not(b)), yy));
- if (cell->type == ID($add))
- ez->assume(ez->vec_eq(ez->vec_add(a, b), yy));
- if (cell->type == ID($sub))
- ez->assume(ez->vec_eq(ez->vec_sub(a, b), yy));
-
- if (model_undef && !arith_undef_handled)
- {
- 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);
- extendSignalWidth(undef_a, undef_b, undef_y, cell, false);
-
- if (cell->type.in(ID($and), ID($_AND_), ID($_NAND_))) {
- std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
- std::vector<int> b0 = ez->vec_and(ez->vec_not(b), ez->vec_not(undef_b));
- std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a0, b0)));
- ez->assume(ez->vec_eq(yX, undef_y));
- }
- else if (cell->type.in(ID($or), ID($_OR_), ID($_NOR_))) {
- std::vector<int> a1 = ez->vec_and(a, ez->vec_not(undef_a));
- std::vector<int> b1 = ez->vec_and(b, ez->vec_not(undef_b));
- std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a1, b1)));
- ez->assume(ez->vec_eq(yX, undef_y));
- }
- else if (cell->type.in(ID($xor), ID($xnor), ID($_XOR_), ID($_XNOR_))) {
- std::vector<int> yX = ez->vec_or(undef_a, undef_b);
- ez->assume(ez->vec_eq(yX, undef_y));
- }
- else if (cell->type == ID($_ANDNOT_)) {
- std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
- std::vector<int> b1 = ez->vec_and(b, ez->vec_not(undef_b));
- std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a0, b1)));
- ez->assume(ez->vec_eq(yX, undef_y));
- }
-
- else if (cell->type == ID($_ORNOT_)) {
- std::vector<int> a1 = ez->vec_and(a, ez->vec_not(undef_a));
- std::vector<int> b0 = ez->vec_and(ez->vec_not(b), ez->vec_not(undef_b));
- std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a1, b0)));
- ez->assume(ez->vec_eq(yX, undef_y));
- }
- else
- log_abort();
-
- undefGating(y, yy, undef_y);
- }
- else if (model_undef)
- {
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type.in(ID($_AOI3_), ID($_OAI3_), ID($_AOI4_), ID($_OAI4_)))
- {
- bool aoi_mode = cell->type.in(ID($_AOI3_), ID($_AOI4_));
- bool three_mode = cell->type.in(ID($_AOI3_), ID($_OAI3_));
-
- int a = importDefSigSpec(cell->getPort(ID::A), timestep).at(0);
- int b = importDefSigSpec(cell->getPort(ID::B), timestep).at(0);
- int c = importDefSigSpec(cell->getPort(ID::C), timestep).at(0);
- int d = three_mode ? (aoi_mode ? ez->CONST_TRUE : ez->CONST_FALSE) : importDefSigSpec(cell->getPort(ID::D), timestep).at(0);
- int y = importDefSigSpec(cell->getPort(ID::Y), timestep).at(0);
- int yy = model_undef ? ez->literal() : y;
-
- if (cell->type.in(ID($_AOI3_), ID($_AOI4_)))
- ez->assume(ez->IFF(ez->NOT(ez->OR(ez->AND(a, b), ez->AND(c, d))), yy));
- else
- ez->assume(ez->IFF(ez->NOT(ez->AND(ez->OR(a, b), ez->OR(c, d))), yy));
-
- if (model_undef)
- {
- int undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep).at(0);
- int undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep).at(0);
- int undef_c = importUndefSigSpec(cell->getPort(ID::C), timestep).at(0);
- int undef_d = three_mode ? ez->CONST_FALSE : importUndefSigSpec(cell->getPort(ID::D), timestep).at(0);
- int undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep).at(0);
-
- if (aoi_mode)
- {
- int a0 = ez->AND(ez->NOT(a), ez->NOT(undef_a));
- int b0 = ez->AND(ez->NOT(b), ez->NOT(undef_b));
- int c0 = ez->AND(ez->NOT(c), ez->NOT(undef_c));
- int d0 = ez->AND(ez->NOT(d), ez->NOT(undef_d));
-
- int ab = ez->AND(a, b), cd = ez->AND(c, d);
- int undef_ab = ez->AND(ez->OR(undef_a, undef_b), ez->NOT(ez->OR(a0, b0)));
- int undef_cd = ez->AND(ez->OR(undef_c, undef_d), ez->NOT(ez->OR(c0, d0)));
-
- int ab1 = ez->AND(ab, ez->NOT(undef_ab));
- int cd1 = ez->AND(cd, ez->NOT(undef_cd));
- int yX = ez->AND(ez->OR(undef_ab, undef_cd), ez->NOT(ez->OR(ab1, cd1)));
-
- ez->assume(ez->IFF(yX, undef_y));
- }
- else
- {
- int a1 = ez->AND(a, ez->NOT(undef_a));
- int b1 = ez->AND(b, ez->NOT(undef_b));
- int c1 = ez->AND(c, ez->NOT(undef_c));
- int d1 = ez->AND(d, ez->NOT(undef_d));
-
- int ab = ez->OR(a, b), cd = ez->OR(c, d);
- int undef_ab = ez->AND(ez->OR(undef_a, undef_b), ez->NOT(ez->OR(a1, b1)));
- int undef_cd = ez->AND(ez->OR(undef_c, undef_d), ez->NOT(ez->OR(c1, d1)));
-
- int ab0 = ez->AND(ez->NOT(ab), ez->NOT(undef_ab));
- int cd0 = ez->AND(ez->NOT(cd), ez->NOT(undef_cd));
- int yX = ez->AND(ez->OR(undef_ab, undef_cd), ez->NOT(ez->OR(ab0, cd0)));
-
- ez->assume(ez->IFF(yX, undef_y));
- }
-
- undefGating(y, yy, undef_y);
- }
-
- return true;
- }
-
- if (cell->type.in(ID($_NOT_), ID($not)))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidthUnary(a, y, cell);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
- ez->assume(ez->vec_eq(ez->vec_not(a), yy));
-
- if (model_undef) {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidthUnary(undef_a, undef_y, cell, false);
- ez->assume(ez->vec_eq(undef_a, undef_y));
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type.in(ID($_MUX_), ID($mux), ID($_NMUX_)))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), 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
- ez->assume(ez->vec_eq(ez->vec_ite(s.at(0), b, a), yy));
-
- 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_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), 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));
- ez->assume(ez->vec_eq(yX, undef_y));
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type == ID($pmux))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- std::vector<int> tmp = 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());
- tmp = ez->vec_ite(s.at(i), part_of_b, tmp);
- }
- ez->assume(ez->vec_eq(tmp, yy));
-
- 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_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
-
- int maybe_a = ez->CONST_TRUE;
-
- 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);
-
- 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);
- }
-
- 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);
-
- ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(bits_set, bits_clr)), undef_y));
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type.in(ID($pos), ID($neg)))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidthUnary(a, y, cell);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- if (cell->type == ID($pos)) {
- ez->assume(ez->vec_eq(a, yy));
- } else {
- std::vector<int> zero(a.size(), ez->CONST_FALSE);
- ez->assume(ez->vec_eq(ez->vec_sub(zero, a), yy));
- }
-
- if (model_undef)
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidthUnary(undef_a, undef_y, cell);
-
- if (cell->type == ID($pos)) {
- ez->assume(ez->vec_eq(undef_a, undef_y));
- } else {
- int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
- std::vector<int> undef_y_bits(undef_y.size(), undef_any_a);
- ez->assume(ez->vec_eq(undef_y_bits, undef_y));
- }
-
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_xnor), ID($reduce_bool), ID($logic_not)))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- if (cell->type == ID($reduce_and))
- ez->SET(ez->expression(ez->OpAnd, a), yy.at(0));
- if (cell->type.in(ID($reduce_or), ID($reduce_bool)))
- ez->SET(ez->expression(ez->OpOr, a), yy.at(0));
- if (cell->type == ID($reduce_xor))
- ez->SET(ez->expression(ez->OpXor, a), yy.at(0));
- if (cell->type == ID($reduce_xnor))
- ez->SET(ez->NOT(ez->expression(ez->OpXor, a)), yy.at(0));
- if (cell->type == ID($logic_not))
- ez->SET(ez->NOT(ez->expression(ez->OpOr, a)), yy.at(0));
- for (size_t i = 1; i < y.size(); i++)
- ez->SET(ez->CONST_FALSE, yy.at(i));
-
- if (model_undef)
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- int aX = ez->expression(ezSAT::OpOr, undef_a);
-
- if (cell->type == ID($reduce_and)) {
- int a0 = ez->expression(ezSAT::OpOr, ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a)));
- ez->assume(ez->IFF(ez->AND(ez->NOT(a0), aX), undef_y.at(0)));
- }
- else if (cell->type.in(ID($reduce_or), ID($reduce_bool), ID($logic_not))) {
- int a1 = ez->expression(ezSAT::OpOr, ez->vec_and(a, ez->vec_not(undef_a)));
- ez->assume(ez->IFF(ez->AND(ez->NOT(a1), aX), undef_y.at(0)));
- }
- else if (cell->type.in(ID($reduce_xor), ID($reduce_xnor))) {
- ez->assume(ez->IFF(aX, undef_y.at(0)));
- } else
- log_abort();
-
- for (size_t i = 1; i < undef_y.size(); i++)
- ez->SET(ez->CONST_FALSE, undef_y.at(i));
-
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type.in(ID($logic_and), ID($logic_or)))
- {
- std::vector<int> vec_a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> vec_b = importDefSigSpec(cell->getPort(ID::B), timestep);
-
- int a = ez->expression(ez->OpOr, vec_a);
- int b = ez->expression(ez->OpOr, vec_b);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- if (cell->type == ID($logic_and))
- ez->SET(ez->expression(ez->OpAnd, a, b), yy.at(0));
- else
- ez->SET(ez->expression(ez->OpOr, a, b), yy.at(0));
- for (size_t i = 1; i < y.size(); i++)
- ez->SET(ez->CONST_FALSE, yy.at(i));
-
- 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);
-
- int a0 = ez->NOT(ez->OR(ez->expression(ezSAT::OpOr, vec_a), ez->expression(ezSAT::OpOr, undef_a)));
- int b0 = ez->NOT(ez->OR(ez->expression(ezSAT::OpOr, vec_b), ez->expression(ezSAT::OpOr, undef_b)));
- int a1 = ez->expression(ezSAT::OpOr, ez->vec_and(vec_a, ez->vec_not(undef_a)));
- int b1 = ez->expression(ezSAT::OpOr, ez->vec_and(vec_b, ez->vec_not(undef_b)));
- int aX = ez->expression(ezSAT::OpOr, undef_a);
- int bX = ez->expression(ezSAT::OpOr, undef_b);
-
- if (cell->type == ID($logic_and))
- ez->SET(ez->AND(ez->OR(aX, bX), ez->NOT(ez->AND(a1, b1)), ez->NOT(a0), ez->NOT(b0)), undef_y.at(0));
- else if (cell->type == ID($logic_or))
- ez->SET(ez->AND(ez->OR(aX, bX), ez->NOT(ez->AND(a0, b0)), ez->NOT(a1), ez->NOT(b1)), undef_y.at(0));
- else
- log_abort();
-
- for (size_t i = 1; i < undef_y.size(); i++)
- ez->SET(ez->CONST_FALSE, undef_y.at(i));
-
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type.in(ID($lt), ID($le), ID($eq), ID($ne), ID($eqx), ID($nex), ID($ge), ID($gt)))
- {
- bool is_signed = cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool();
- 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);
- extendSignalWidth(a, b, cell);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- if (model_undef && cell->type.in(ID($eqx), ID($nex))) {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
- extendSignalWidth(undef_a, undef_b, cell, true);
- a = ez->vec_or(a, undef_a);
- b = ez->vec_or(b, undef_b);
- }
-
- if (cell->type == ID($lt))
- ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), yy.at(0));
- if (cell->type == ID($le))
- ez->SET(is_signed ? ez->vec_le_signed(a, b) : ez->vec_le_unsigned(a, b), yy.at(0));
- if (cell->type.in(ID($eq), ID($eqx)))
- ez->SET(ez->vec_eq(a, b), yy.at(0));
- if (cell->type.in(ID($ne), ID($nex)))
- ez->SET(ez->vec_ne(a, b), yy.at(0));
- if (cell->type == ID($ge))
- ez->SET(is_signed ? ez->vec_ge_signed(a, b) : ez->vec_ge_unsigned(a, b), yy.at(0));
- if (cell->type == ID($gt))
- ez->SET(is_signed ? ez->vec_gt_signed(a, b) : ez->vec_gt_unsigned(a, b), yy.at(0));
- for (size_t i = 1; i < y.size(); i++)
- ez->SET(ez->CONST_FALSE, yy.at(i));
-
- if (model_undef && cell->type.in(ID($eqx), ID($nex)))
- {
- 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);
- extendSignalWidth(undef_a, undef_b, cell, true);
-
- if (cell->type == ID($eqx))
- yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
- else
- yy.at(0) = ez->OR(yy.at(0), ez->vec_ne(undef_a, undef_b));
-
- for (size_t i = 0; i < y.size(); i++)
- ez->SET(ez->CONST_FALSE, undef_y.at(i));
-
- ez->assume(ez->vec_eq(y, yy));
- }
- else if (model_undef && cell->type.in(ID($eq), ID($ne)))
- {
- 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);
- extendSignalWidth(undef_a, undef_b, cell, true);
-
- int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
- int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
- int undef_any = ez->OR(undef_any_a, undef_any_b);
-
- std::vector<int> masked_a_bits = ez->vec_or(a, ez->vec_or(undef_a, undef_b));
- std::vector<int> masked_b_bits = ez->vec_or(b, ez->vec_or(undef_a, undef_b));
-
- int masked_ne = ez->vec_ne(masked_a_bits, masked_b_bits);
- int undef_y_bit = ez->AND(undef_any, ez->NOT(masked_ne));
-
- for (size_t i = 1; i < undef_y.size(); i++)
- ez->SET(ez->CONST_FALSE, undef_y.at(i));
- ez->SET(undef_y_bit, undef_y.at(0));
-
- undefGating(y, yy, undef_y);
- }
- else
- {
- if (model_undef) {
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- undefGating(y, yy, undef_y);
- }
- log_assert(!model_undef || arith_undef_handled);
- }
- return true;
- }
-
- if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)))
- {
- 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);
-
- int extend_bit = ez->CONST_FALSE;
-
- if (!cell->type.in(ID($shift), ID($shiftx)) && cell->parameters[ID::A_SIGNED].as_bool())
- extend_bit = a.back();
-
- while (y.size() < a.size())
- y.push_back(ez->literal());
- while (y.size() > a.size())
- a.push_back(extend_bit);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
- std::vector<int> shifted_a;
-
- if (cell->type.in( ID($shl), ID($sshl)))
- shifted_a = ez->vec_shift_left(a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
-
- if (cell->type == ID($shr))
- shifted_a = ez->vec_shift_right(a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
-
- if (cell->type == ID($sshr))
- shifted_a = ez->vec_shift_right(a, b, false, cell->parameters[ID::A_SIGNED].as_bool() ? a.back() : ez->CONST_FALSE, ez->CONST_FALSE);
-
- if (cell->type.in(ID($shift), ID($shiftx)))
- shifted_a = ez->vec_shift_right(a, b, cell->parameters[ID::B_SIGNED].as_bool(), ez->CONST_FALSE, ez->CONST_FALSE);
-
- ez->assume(ez->vec_eq(shifted_a, yy));
-
- 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> undef_a_shifted;
-
- extend_bit = cell->type == ID($shiftx) ? ez->CONST_TRUE : ez->CONST_FALSE;
- if (!cell->type.in(ID($shift), ID($shiftx)) && cell->parameters[ID::A_SIGNED].as_bool())
- extend_bit = undef_a.back();
-
- while (undef_y.size() < undef_a.size())
- undef_y.push_back(ez->literal());
- while (undef_y.size() > undef_a.size())
- undef_a.push_back(extend_bit);
-
- if (cell->type.in(ID($shl), ID($sshl)))
- undef_a_shifted = ez->vec_shift_left(undef_a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
-
- if (cell->type == ID($shr))
- undef_a_shifted = ez->vec_shift_right(undef_a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
-
- if (cell->type == ID($sshr))
- undef_a_shifted = ez->vec_shift_right(undef_a, b, false, cell->parameters[ID::A_SIGNED].as_bool() ? undef_a.back() : ez->CONST_FALSE, ez->CONST_FALSE);
-
- if (cell->type == ID($shift))
- undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters[ID::B_SIGNED].as_bool(), ez->CONST_FALSE, ez->CONST_FALSE);
-
- if (cell->type == ID($shiftx))
- undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters[ID::B_SIGNED].as_bool(), ez->CONST_TRUE, ez->CONST_TRUE);
-
- int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
- std::vector<int> undef_all_y_bits(undef_y.size(), undef_any_b);
- ez->assume(ez->vec_eq(ez->vec_or(undef_a_shifted, undef_all_y_bits), undef_y));
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type == ID($mul))
- {
- 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);
- extendSignalWidth(a, b, y, cell);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- std::vector<int> tmp(a.size(), ez->CONST_FALSE);
- for (int i = 0; i < int(a.size()); i++)
- {
- std::vector<int> shifted_a(a.size(), ez->CONST_FALSE);
- for (int j = i; j < int(a.size()); j++)
- shifted_a.at(j) = a.at(j-i);
- tmp = ez->vec_ite(b.at(i), ez->vec_add(tmp, shifted_a), tmp);
- }
- ez->assume(ez->vec_eq(tmp, yy));
-
- if (model_undef) {
- log_assert(arith_undef_handled);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type == ID($macc))
- {
- 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);
-
- Macc macc;
- macc.from_cell(cell);
-
- std::vector<int> tmp(GetSize(y), ez->CONST_FALSE);
-
- for (auto &port : macc.ports)
- {
- std::vector<int> in_a = importDefSigSpec(port.in_a, timestep);
- std::vector<int> in_b = importDefSigSpec(port.in_b, timestep);
-
- while (GetSize(in_a) < GetSize(y))
- in_a.push_back(port.is_signed && !in_a.empty() ? in_a.back() : ez->CONST_FALSE);
- in_a.resize(GetSize(y));
-
- if (GetSize(in_b))
- {
- while (GetSize(in_b) < GetSize(y))
- in_b.push_back(port.is_signed && !in_b.empty() ? in_b.back() : ez->CONST_FALSE);
- in_b.resize(GetSize(y));
-
- for (int i = 0; i < GetSize(in_b); i++) {
- std::vector<int> shifted_a(in_a.size(), ez->CONST_FALSE);
- for (int j = i; j < int(in_a.size()); j++)
- shifted_a.at(j) = in_a.at(j-i);
- if (port.do_subtract)
- tmp = ez->vec_ite(in_b.at(i), ez->vec_sub(tmp, shifted_a), tmp);
- else
- tmp = ez->vec_ite(in_b.at(i), ez->vec_add(tmp, shifted_a), tmp);
- }
- }
- else
- {
- if (port.do_subtract)
- tmp = ez->vec_sub(tmp, in_a);
- else
- tmp = ez->vec_add(tmp, in_a);
- }
- }
-
- for (int i = 0; i < GetSize(b); i++) {
- std::vector<int> val(GetSize(y), ez->CONST_FALSE);
- val.at(0) = b.at(i);
- tmp = ez->vec_add(tmp, val);
- }
-
- 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);
-
- int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
- int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
-
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- ez->assume(ez->vec_eq(undef_y, std::vector<int>(GetSize(y), ez->OR(undef_any_a, undef_any_b))));
-
- undefGating(y, tmp, undef_y);
- }
- else
- ez->assume(ez->vec_eq(y, tmp));
-
- return true;
- }
-
- if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor)))
- {
- 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);
- extendSignalWidth(a, b, y, cell);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- std::vector<int> a_u, b_u;
- if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
- a_u = ez->vec_ite(a.back(), ez->vec_neg(a), a);
- b_u = ez->vec_ite(b.back(), ez->vec_neg(b), b);
- } else {
- a_u = a;
- b_u = b;
- }
-
- std::vector<int> chain_buf = a_u;
- std::vector<int> y_u(a_u.size(), ez->CONST_FALSE);
- for (int i = int(a.size())-1; i >= 0; i--)
- {
- chain_buf.insert(chain_buf.end(), chain_buf.size(), ez->CONST_FALSE);
-
- std::vector<int> b_shl(i, ez->CONST_FALSE);
- b_shl.insert(b_shl.end(), b_u.begin(), b_u.end());
- b_shl.insert(b_shl.end(), chain_buf.size()-b_shl.size(), ez->CONST_FALSE);
-
- y_u.at(i) = ez->vec_ge_unsigned(chain_buf, b_shl);
- chain_buf = ez->vec_ite(y_u.at(i), ez->vec_sub(chain_buf, b_shl), chain_buf);
-
- chain_buf.erase(chain_buf.begin() + a_u.size(), chain_buf.end());
- }
-
- std::vector<int> y_tmp = ignore_div_by_zero ? yy : ez->vec_var(y.size());
-
- // modulo calculation
- std::vector<int> modulo_trunc;
- int floored_eq_trunc;
- if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
- modulo_trunc = ez->vec_ite(a.back(), ez->vec_neg(chain_buf), chain_buf);
- // floor == trunc when sgn(a) == sgn(b) or trunc == 0
- floored_eq_trunc = ez->OR(ez->IFF(a.back(), b.back()), ez->NOT(ez->expression(ezSAT::OpOr, modulo_trunc)));
- } else {
- modulo_trunc = chain_buf;
- floored_eq_trunc = ez->CONST_TRUE;
- }
-
- if (cell->type == ID($div)) {
- if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
- ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(ez->XOR(a.back(), b.back()), ez->vec_neg(y_u), y_u)));
- else
- ez->assume(ez->vec_eq(y_tmp, y_u));
- } else if (cell->type == ID($mod)) {
- ez->assume(ez->vec_eq(y_tmp, modulo_trunc));
- } else if (cell->type == ID($divfloor)) {
- if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
- ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(
- ez->XOR(a.back(), b.back()),
- ez->vec_neg(ez->vec_ite(
- ez->vec_reduce_or(modulo_trunc),
- ez->vec_add(y_u, ez->vec_const_unsigned(1, y_u.size())),
- y_u
- )),
- y_u
- )));
- else
- ez->assume(ez->vec_eq(y_tmp, y_u));
- } else if (cell->type == ID($modfloor)) {
- ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(floored_eq_trunc, modulo_trunc, ez->vec_add(modulo_trunc, b))));
- }
-
- if (ignore_div_by_zero) {
- ez->assume(ez->expression(ezSAT::OpOr, b));
- } else {
- std::vector<int> div_zero_result;
- if (cell->type.in(ID($div), ID($divfloor))) {
- if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
- std::vector<int> all_ones(y.size(), ez->CONST_TRUE);
- std::vector<int> only_first_one(y.size(), ez->CONST_FALSE);
- only_first_one.at(0) = ez->CONST_TRUE;
- div_zero_result = ez->vec_ite(a.back(), only_first_one, all_ones);
- } else {
- div_zero_result.insert(div_zero_result.end(), cell->getPort(ID::A).size(), ez->CONST_TRUE);
- div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
- }
- } else if (cell->type.in(ID($mod), ID($modfloor))) {
- // a mod 0 = a
- int copy_a_bits = min(cell->getPort(ID::A).size(), cell->getPort(ID::B).size());
- div_zero_result.insert(div_zero_result.end(), a.begin(), a.begin() + copy_a_bits);
- if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
- div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), div_zero_result.back());
- else
- div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
- }
- ez->assume(ez->vec_eq(yy, ez->vec_ite(ez->expression(ezSAT::OpOr, b), y_tmp, div_zero_result)));
- }
-
- if (model_undef) {
- log_assert(arith_undef_handled);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type == ID($lut))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
-
- std::vector<int> lut;
- for (auto bit : cell->getParam(ID::LUT).bits)
- lut.push_back(bit == State::S1 ? ez->CONST_TRUE : ez->CONST_FALSE);
- while (GetSize(lut) < (1 << GetSize(a)))
- lut.push_back(ez->CONST_FALSE);
- lut.resize(1 << GetSize(a));
-
- if (model_undef)
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> t(lut), u(GetSize(t), ez->CONST_FALSE);
-
- for (int i = GetSize(a)-1; i >= 0; i--)
- {
- std::vector<int> t0(t.begin(), t.begin() + GetSize(t)/2);
- std::vector<int> t1(t.begin() + GetSize(t)/2, t.end());
-
- std::vector<int> u0(u.begin(), u.begin() + GetSize(u)/2);
- std::vector<int> u1(u.begin() + GetSize(u)/2, u.end());
-
- t = ez->vec_ite(a[i], t1, t0);
- u = ez->vec_ite(undef_a[i], ez->vec_or(ez->vec_xor(t0, t1), ez->vec_or(u0, u1)), ez->vec_ite(a[i], u1, u0));
- }
-
- log_assert(GetSize(t) == 1);
- log_assert(GetSize(u) == 1);
- undefGating(y, t, u);
- ez->assume(ez->vec_eq(importUndefSigSpec(cell->getPort(ID::Y), timestep), u));
- }
- else
- {
- std::vector<int> t = lut;
- for (int i = GetSize(a)-1; i >= 0; i--)
- {
- std::vector<int> t0(t.begin(), t.begin() + GetSize(t)/2);
- std::vector<int> t1(t.begin() + GetSize(t)/2, t.end());
- t = ez->vec_ite(a[i], t1, t0);
- }
-
- log_assert(GetSize(t) == 1);
- ez->assume(ez->vec_eq(y, t));
- }
- return true;
- }
-
- if (cell->type == ID($sop))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- int y = importDefSigSpec(cell->getPort(ID::Y), timestep).at(0);
-
- int width = cell->getParam(ID::WIDTH).as_int();
- int depth = cell->getParam(ID::DEPTH).as_int();
-
- vector<State> table_raw = cell->getParam(ID::TABLE).bits;
- while (GetSize(table_raw) < 2*width*depth)
- table_raw.push_back(State::S0);
-
- vector<vector<int>> table(depth);
-
- for (int i = 0; i < depth; i++)
- for (int j = 0; j < width; j++)
- {
- bool pat0 = (table_raw[2*width*i + 2*j + 0] == State::S1);
- bool pat1 = (table_raw[2*width*i + 2*j + 1] == State::S1);
-
- if (pat0 && !pat1)
- table.at(i).push_back(0);
- else if (!pat0 && pat1)
- table.at(i).push_back(1);
- else
- table.at(i).push_back(-1);
- }
-
- if (model_undef)
- {
- std::vector<int> products, undef_products;
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- int undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep).at(0);
-
- for (int i = 0; i < depth; i++)
- {
- std::vector<int> cmp_a, cmp_ua, cmp_b;
-
- for (int j = 0; j < width; j++)
- if (table.at(i).at(j) >= 0) {
- cmp_a.push_back(a.at(j));
- cmp_ua.push_back(undef_a.at(j));
- cmp_b.push_back(table.at(i).at(j) ? ez->CONST_TRUE : ez->CONST_FALSE);
- }
-
- std::vector<int> masked_a = ez->vec_or(cmp_a, cmp_ua);
- std::vector<int> masked_b = ez->vec_or(cmp_b, cmp_ua);
-
- int masked_eq = ez->vec_eq(masked_a, masked_b);
- int any_undef = ez->expression(ezSAT::OpOr, cmp_ua);
-
- undef_products.push_back(ez->AND(any_undef, masked_eq));
- products.push_back(ez->AND(ez->NOT(any_undef), masked_eq));
- }
-
- int yy = ez->expression(ezSAT::OpOr, products);
- ez->SET(undef_y, ez->AND(ez->NOT(yy), ez->expression(ezSAT::OpOr, undef_products)));
- undefGating(y, yy, undef_y);
- }
- else
- {
- std::vector<int> products;
-
- for (int i = 0; i < depth; i++)
- {
- std::vector<int> cmp_a, cmp_b;
-
- for (int j = 0; j < width; j++)
- if (table.at(i).at(j) >= 0) {
- cmp_a.push_back(a.at(j));
- cmp_b.push_back(table.at(i).at(j) ? ez->CONST_TRUE : ez->CONST_FALSE);
- }
-
- products.push_back(ez->vec_eq(cmp_a, cmp_b));
- }
-
- ez->SET(y, ez->expression(ezSAT::OpOr, products));
- }
-
- return true;
- }
-
- if (cell->type == ID($fa))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> c = importDefSigSpec(cell->getPort(ID::C), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
- std::vector<int> x = importDefSigSpec(cell->getPort(ID::X), timestep);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
- std::vector<int> xx = model_undef ? ez->vec_var(x.size()) : x;
-
- std::vector<int> t1 = ez->vec_xor(a, b);
- ez->assume(ez->vec_eq(yy, ez->vec_xor(t1, c)));
-
- std::vector<int> t2 = ez->vec_and(a, b);
- std::vector<int> t3 = ez->vec_and(c, t1);
- ez->assume(ez->vec_eq(xx, ez->vec_or(t2, t3)));
-
- 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_c = importUndefSigSpec(cell->getPort(ID::C), timestep);
-
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- std::vector<int> undef_x = importUndefSigSpec(cell->getPort(ID::X), timestep);
-
- ez->assume(ez->vec_eq(undef_y, ez->vec_or(ez->vec_or(undef_a, undef_b), undef_c)));
- ez->assume(ez->vec_eq(undef_x, undef_y));
-
- undefGating(y, yy, undef_y);
- undefGating(x, xx, undef_x);
- }
- return true;
- }
-
- if (cell->type == ID($lcu))
- {
- std::vector<int> p = importDefSigSpec(cell->getPort(ID::P), timestep);
- std::vector<int> g = importDefSigSpec(cell->getPort(ID::G), timestep);
- std::vector<int> ci = importDefSigSpec(cell->getPort(ID::CI), timestep);
- std::vector<int> co = importDefSigSpec(cell->getPort(ID::CO), timestep);
-
- std::vector<int> yy = model_undef ? ez->vec_var(co.size()) : co;
-
- for (int i = 0; i < GetSize(co); i++)
- ez->SET(yy[i], ez->OR(g[i], ez->AND(p[i], i ? yy[i-1] : ci[0])));
-
- if (model_undef)
- {
- std::vector<int> undef_p = importUndefSigSpec(cell->getPort(ID::P), timestep);
- std::vector<int> undef_g = importUndefSigSpec(cell->getPort(ID::G), timestep);
- std::vector<int> undef_ci = importUndefSigSpec(cell->getPort(ID::CI), timestep);
- std::vector<int> undef_co = importUndefSigSpec(cell->getPort(ID::CO), timestep);
-
- int undef_any_p = ez->expression(ezSAT::OpOr, undef_p);
- int undef_any_g = ez->expression(ezSAT::OpOr, undef_g);
- int undef_any_ci = ez->expression(ezSAT::OpOr, undef_ci);
- int undef_co_bit = ez->OR(undef_any_p, undef_any_g, undef_any_ci);
-
- std::vector<int> undef_co_bits(undef_co.size(), undef_co_bit);
- ez->assume(ez->vec_eq(undef_co_bits, undef_co));
-
- undefGating(co, yy, undef_co);
- }
- return true;
- }
-
- if (cell->type == ID($alu))
- {
- 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> x = importDefSigSpec(cell->getPort(ID::X), timestep);
- std::vector<int> ci = importDefSigSpec(cell->getPort(ID::CI), timestep);
- std::vector<int> bi = importDefSigSpec(cell->getPort(ID::BI), timestep);
- std::vector<int> co = importDefSigSpec(cell->getPort(ID::CO), timestep);
-
- extendSignalWidth(a, b, y, cell);
- extendSignalWidth(a, b, x, cell);
- extendSignalWidth(a, b, co, cell);
-
- std::vector<int> def_y = model_undef ? ez->vec_var(y.size()) : y;
- std::vector<int> def_x = model_undef ? ez->vec_var(x.size()) : x;
- std::vector<int> def_co = model_undef ? ez->vec_var(co.size()) : co;
-
- log_assert(GetSize(y) == GetSize(x));
- log_assert(GetSize(y) == GetSize(co));
- log_assert(GetSize(ci) == 1);
- log_assert(GetSize(bi) == 1);
-
- for (int i = 0; i < GetSize(y); i++)
- {
- int s1 = a.at(i), s2 = ez->XOR(b.at(i), bi.at(0)), s3 = i ? co.at(i-1) : ci.at(0);
- ez->SET(def_x.at(i), ez->XOR(s1, s2));
- ez->SET(def_y.at(i), ez->XOR(def_x.at(i), s3));
- ez->SET(def_co.at(i), ez->OR(ez->AND(s1, s2), ez->AND(s1, s3), ez->AND(s2, s3)));
- }
-
- 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_ci = importUndefSigSpec(cell->getPort(ID::CI), timestep);
- std::vector<int> undef_bi = importUndefSigSpec(cell->getPort(ID::BI), timestep);
-
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- std::vector<int> undef_x = importUndefSigSpec(cell->getPort(ID::X), timestep);
- std::vector<int> undef_co = importUndefSigSpec(cell->getPort(ID::CO), timestep);
-
- extendSignalWidth(undef_a, undef_b, undef_y, cell);
- extendSignalWidth(undef_a, undef_b, undef_x, cell);
- extendSignalWidth(undef_a, undef_b, undef_co, cell);
-
- std::vector<int> all_inputs_undef;
- all_inputs_undef.insert(all_inputs_undef.end(), undef_a.begin(), undef_a.end());
- all_inputs_undef.insert(all_inputs_undef.end(), undef_b.begin(), undef_b.end());
- all_inputs_undef.insert(all_inputs_undef.end(), undef_ci.begin(), undef_ci.end());
- all_inputs_undef.insert(all_inputs_undef.end(), undef_bi.begin(), undef_bi.end());
- int undef_any = ez->expression(ezSAT::OpOr, all_inputs_undef);
-
- for (int i = 0; i < GetSize(undef_y); i++) {
- ez->SET(undef_y.at(i), undef_any);
- ez->SET(undef_x.at(i), ez->OR(undef_a.at(i), undef_b.at(i), undef_bi.at(0)));
- ez->SET(undef_co.at(i), undef_any);
- }
-
- undefGating(y, def_y, undef_y);
- undefGating(x, def_x, undef_x);
- undefGating(co, def_co, undef_co);
- }
- return true;
- }
-
- if (cell->type == ID($slice))
- {
- RTLIL::SigSpec a = cell->getPort(ID::A);
- RTLIL::SigSpec y = cell->getPort(ID::Y);
- ez->assume(signals_eq(a.extract(cell->parameters.at(ID::OFFSET).as_int(), y.size()), y, timestep));
- return true;
- }
-
- if (cell->type == ID($concat))
- {
- RTLIL::SigSpec a = cell->getPort(ID::A);
- RTLIL::SigSpec b = cell->getPort(ID::B);
- RTLIL::SigSpec y = cell->getPort(ID::Y);
-
- RTLIL::SigSpec ab = a;
- ab.append(b);
-
- ez->assume(signals_eq(ab, y, timestep));
- return true;
- }
-
- if (timestep > 0 && cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_N_), ID($_DFF_P_)))
- {
- if (timestep == 1)
- {
- initial_state.add((*sigmap)(cell->getPort(ID::Q)));
- }
- else
- {
- std::vector<int> d = importDefSigSpec(cell->getPort(ID::D), timestep-1);
- std::vector<int> q = importDefSigSpec(cell->getPort(ID::Q), timestep);
-
- std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
- ez->assume(ez->vec_eq(d, qq));
-
- if (model_undef)
- {
- std::vector<int> undef_d = importUndefSigSpec(cell->getPort(ID::D), timestep-1);
- std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Q), timestep);
-
- ez->assume(ez->vec_eq(undef_d, undef_q));
- undefGating(q, qq, undef_q);
- }
- }
- return true;
- }
-
- if (cell->type == ID($anyconst))
- {
- if (timestep < 2)
- return true;
-
- std::vector<int> d = importDefSigSpec(cell->getPort(ID::Y), timestep-1);
- std::vector<int> q = importDefSigSpec(cell->getPort(ID::Y), timestep);
-
- std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
- ez->assume(ez->vec_eq(d, qq));
-
- if (model_undef)
- {
- std::vector<int> undef_d = importUndefSigSpec(cell->getPort(ID::Y), timestep-1);
- std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Y), timestep);
-
- ez->assume(ez->vec_eq(undef_d, undef_q));
- undefGating(q, qq, undef_q);
- }
- return true;
- }
-
- if (cell->type == ID($anyseq))
- {
- return true;
- }
-
- if (cell->type.in(ID($_BUF_), ID($equiv)))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidthUnary(a, y, cell);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
- ez->assume(ez->vec_eq(a, yy));
-
- if (model_undef) {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidthUnary(undef_a, undef_y, cell, false);
- ez->assume(ez->vec_eq(undef_a, undef_y));
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type == ID($initstate))
- {
- auto key = make_pair(prefix, timestep);
- if (initstates.count(key) == 0)
- initstates[key] = false;
-
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
- log_assert(GetSize(y) == 1);
- ez->SET(y[0], initstates[key] ? ez->CONST_TRUE : ez->CONST_FALSE);
-
- if (model_undef) {
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- log_assert(GetSize(undef_y) == 1);
- ez->SET(undef_y[0], ez->CONST_FALSE);
- }
-
- return true;
- }
-
- if (cell->type == ID($assert))
- {
- std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
- asserts_a[pf].append((*sigmap)(cell->getPort(ID::A)));
- asserts_en[pf].append((*sigmap)(cell->getPort(ID::EN)));
- return true;
- }
-
- if (cell->type == ID($assume))
- {
- std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
- assumes_a[pf].append((*sigmap)(cell->getPort(ID::A)));
- assumes_en[pf].append((*sigmap)(cell->getPort(ID::EN)));
- return true;
- }
-
- // Unsupported internal cell types: $pow $lut
- // .. and all sequential cells except $dff and $_DFF_[NP]_
- return false;
- }
+ bool importCell(RTLIL::Cell *cell, int timestep = -1);
};
YOSYS_NAMESPACE_END
diff --git a/kernel/yosys.cc b/kernel/yosys.cc
index 2ec3dca0c..dcaf364e9 100644
--- a/kernel/yosys.cc
+++ b/kernel/yosys.cc
@@ -89,6 +89,12 @@ bool memhasher_active = false;
uint32_t memhasher_rng = 123456;
std::vector<void*> memhasher_store;
+std::string yosys_share_dirname;
+std::string yosys_abc_executable;
+
+void init_share_dirname();
+void init_abc_executable_name();
+
void memhasher_on()
{
#if defined(__linux__) || defined(__FreeBSD__)
@@ -523,6 +529,8 @@ void yosys_setup()
if(already_setup)
return;
already_setup = true;
+ init_share_dirname();
+ init_abc_executable_name();
#define X(_id) RTLIL::ID::_id = "\\" # _id;
#include "kernel/constids.inc"
@@ -713,7 +721,7 @@ extern Tcl_Interp *yosys_get_tcl_interp()
struct TclPass : public Pass {
TclPass() : Pass("tcl", "execute a TCL script file") { }
- void help() YS_OVERRIDE {
+ void help() override {
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
log(" tcl <filename> [args]\n");
@@ -730,7 +738,7 @@ struct TclPass : public Pass {
log("the standard $argc and $argv variables.\n");
log("\n");
}
- void execute(std::vector<std::string> args, RTLIL::Design *) YS_OVERRIDE {
+ void execute(std::vector<std::string> args, RTLIL::Design *) override {
if (args.size() < 2)
log_cmd_error("Missing script file.\n");
@@ -825,38 +833,74 @@ std::string proc_self_dirname()
#endif
#if defined(EMSCRIPTEN) || defined(__wasm)
-std::string proc_share_dirname()
+void init_share_dirname()
{
- return "/share/";
+ yosys_share_dirname = "/share/";
}
#else
-std::string proc_share_dirname()
+void init_share_dirname()
{
std::string proc_self_path = proc_self_dirname();
# if defined(_WIN32) && !defined(YOSYS_WIN32_UNIX_DIR)
std::string proc_share_path = proc_self_path + "share\\";
- if (check_file_exists(proc_share_path, true))
- return proc_share_path;
+ if (check_file_exists(proc_share_path, true)) {
+ yosys_share_dirname = proc_share_path;
+ return;
+ }
proc_share_path = proc_self_path + "..\\share\\";
- if (check_file_exists(proc_share_path, true))
- return proc_share_path;
+ if (check_file_exists(proc_share_path, true)) {
+ yosys_share_dirname = proc_share_path;
+ return;
+ }
# else
std::string proc_share_path = proc_self_path + "share/";
- if (check_file_exists(proc_share_path, true))
- return proc_share_path;
+ if (check_file_exists(proc_share_path, true)) {
+ yosys_share_dirname = proc_share_path;
+ return;
+ }
proc_share_path = proc_self_path + "../share/" + proc_program_prefix()+ "yosys/";
- if (check_file_exists(proc_share_path, true))
- return proc_share_path;
+ if (check_file_exists(proc_share_path, true)) {
+ yosys_share_dirname = proc_share_path;
+ return;
+ }
# ifdef YOSYS_DATDIR
proc_share_path = YOSYS_DATDIR "/";
- if (check_file_exists(proc_share_path, true))
- return proc_share_path;
+ if (check_file_exists(proc_share_path, true)) {
+ yosys_share_dirname = proc_share_path;
+ return;
+ }
# endif
# endif
- log_error("proc_share_dirname: unable to determine share/ directory!\n");
}
#endif
+void init_abc_executable_name()
+{
+#ifdef ABCEXTERNAL
+ std::string exe_file;
+ if (std::getenv("ABC")) {
+ yosys_abc_executable = std::getenv("ABC");
+ } else {
+ yosys_abc_executable = ABCEXTERNAL;
+ }
+#else
+ yosys_abc_executable = proc_self_dirname() + proc_program_prefix()+ "yosys-abc";
+#endif
+#ifdef _WIN32
+#ifndef ABCEXTERNAL
+ if (!check_file_exists(yosys_abc_executable + ".exe") && check_file_exists(proc_self_dirname() + "..\\" + proc_program_prefix() + "yosys-abc.exe"))
+ yosys_abc_executable = proc_self_dirname() + "..\\" + proc_program_prefix() + "yosys-abc";
+#endif
+#endif
+}
+
+std::string proc_share_dirname()
+{
+ if (yosys_share_dirname.empty())
+ log_error("init_share_dirname: unable to determine share/ directory!\n");
+ return yosys_share_dirname;
+}
+
std::string proc_program_prefix()
{
std::string program_prefix;
@@ -930,7 +974,7 @@ void run_frontend(std::string filename, std::string command, std::string *backen
else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-5, std::string::npos, ".json") == 0)
command = "json";
else if (filename_trim.size() > 3 && filename_trim.compare(filename_trim.size()-3, std::string::npos, ".il") == 0)
- command = "ilang";
+ command = "rtlil";
else if (filename_trim.size() > 3 && filename_trim.compare(filename_trim.size()-3, std::string::npos, ".ys") == 0)
command = "script";
else if (filename_trim.size() > 3 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".tcl") == 0)
@@ -1050,8 +1094,10 @@ void run_backend(std::string filename, std::string command, RTLIL::Design *desig
if (command == "auto") {
if (filename.size() > 2 && filename.compare(filename.size()-2, std::string::npos, ".v") == 0)
command = "verilog";
+ else if (filename.size() > 3 && filename.compare(filename.size()-3, std::string::npos, ".sv") == 0)
+ command = "verilog -sv";
else if (filename.size() > 3 && filename.compare(filename.size()-3, std::string::npos, ".il") == 0)
- command = "ilang";
+ command = "rtlil";
else if (filename.size() > 3 && filename.compare(filename.size()-3, std::string::npos, ".cc") == 0)
command = "cxxrtl";
else if (filename.size() > 4 && filename.compare(filename.size()-4, std::string::npos, ".aig") == 0)
@@ -1063,7 +1109,7 @@ void run_backend(std::string filename, std::string command, RTLIL::Design *desig
else if (filename.size() > 5 && filename.compare(filename.size()-5, std::string::npos, ".json") == 0)
command = "json";
else if (filename == "-")
- command = "ilang";
+ command = "rtlil";
else if (filename.empty())
return;
else
@@ -1220,7 +1266,7 @@ void shell(RTLIL::Design *design)
struct ShellPass : public Pass {
ShellPass() : Pass("shell", "enter interactive command mode") { }
- void help() YS_OVERRIDE {
+ void help() override {
log("\n");
log(" shell\n");
log("\n");
@@ -1252,7 +1298,7 @@ struct ShellPass : public Pass {
log("Press Ctrl-D or type 'exit' to leave the interactive shell.\n");
log("\n");
}
- void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE {
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override {
extra_args(args, 1, design, false);
shell(design);
}
@@ -1261,7 +1307,7 @@ struct ShellPass : public Pass {
#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
struct HistoryPass : public Pass {
HistoryPass() : Pass("history", "show last interactive commands") { }
- void help() YS_OVERRIDE {
+ void help() override {
log("\n");
log(" history\n");
log("\n");
@@ -1270,7 +1316,7 @@ struct HistoryPass : public Pass {
log("from executed scripts.\n");
log("\n");
}
- void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE {
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override {
extra_args(args, 1, design, false);
#ifdef YOSYS_ENABLE_READLINE
for(HIST_ENTRY **list = history_list(); *list != NULL; list++)
@@ -1285,7 +1331,7 @@ struct HistoryPass : public Pass {
struct ScriptCmdPass : public Pass {
ScriptCmdPass() : Pass("script", "execute commands from file or wire") { }
- void help() YS_OVERRIDE {
+ void help() override {
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
log(" script <filename> [<from_label>:<to_label>]\n");
@@ -1308,7 +1354,7 @@ struct ScriptCmdPass : public Pass {
log("'-module' mode can be exited by using the 'cd' command.\n");
log("\n");
}
- void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
bool scriptwire = false;
diff --git a/kernel/yosys.h b/kernel/yosys.h
index c922faf26..ab6eb5f8c 100644
--- a/kernel/yosys.h
+++ b/kernel/yosys.h
@@ -117,11 +117,11 @@ extern Tcl_Obj *Tcl_ObjSetVar2(Tcl_Interp *interp, Tcl_Obj *part1Ptr, Tcl_Obj *p
# define PATH_MAX MAX_PATH
# define isatty _isatty
# define fileno _fileno
-# else
-// mingw includes `wingdi.h` which defines a TRANSPARENT macro
-// that conflicts with X(TRANSPARENT) entry in kernel/constids.inc
-# undef TRANSPARENT
# endif
+
+// mingw and msvc include `wingdi.h` which defines a TRANSPARENT macro
+// that conflicts with X(TRANSPARENT) entry in kernel/constids.inc
+# undef TRANSPARENT
#endif
#ifndef PATH_MAX
@@ -136,23 +136,20 @@ extern Tcl_Obj *Tcl_ObjSetVar2(Tcl_Interp *interp, Tcl_Obj *part1Ptr, Tcl_Obj *p
#define YOSYS_NAMESPACE_PREFIX Yosys::
#define USING_YOSYS_NAMESPACE using namespace Yosys;
-#if __cplusplus >= 201103L
-# define YS_OVERRIDE override
-# define YS_FINAL final
-#else
-# define YS_OVERRIDE
-# define YS_FINAL
-#endif
-
#if defined(__GNUC__) || defined(__clang__)
# define YS_ATTRIBUTE(...) __attribute__((__VA_ARGS__))
-# define YS_NORETURN
#elif defined(_MSC_VER)
# define YS_ATTRIBUTE(...)
-# define YS_NORETURN __declspec(noreturn)
#else
# define YS_ATTRIBUTE(...)
-# define YS_NORETURN
+#endif
+
+#if __cplusplus >= 201703L
+# define YS_MAYBE_UNUSED [[maybe_unused]];
+#elif defined(__GNUC__) || defined(__clang__)
+# define YS_MAYBE_UNUSED __attribute__((__unused__))
+#else
+# define YS_MAYBE_UNUSED
#endif
#if __cplusplus >= 201703L
@@ -369,6 +366,9 @@ extern std::map<std::string, void*> loaded_python_plugins;
extern std::map<std::string, std::string> loaded_plugin_aliases;
void load_plugin(std::string filename, std::vector<std::string> aliases);
+extern std::string yosys_share_dirname;
+extern std::string yosys_abc_executable;
+
YOSYS_NAMESPACE_END
#endif
generated by cgit v1.2.3 (git 2.25.1) at 2025-06-10 09:32:53 +0000